metamath  

Messages by Thread

• • Re: [Metamath] GPT-f paper savask
  • Re: [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
• [Metamath] Going from AM-GM to AM-GM 3 'Stanislas Polu' via Metamath
  • Re: [Metamath] Going from AM-GM to AM-GM 3 Mario Carneiro
  • Re: [Metamath] Going from AM-GM to AM-GM 3 'Stanislas Polu' via Metamath
• Re: [Metamath] Re: Resources for newbies Thierry Arnoux
  • Re: [Metamath] Re: Resources for newbies David A. Wheeler
  • Re: [Metamath] Re: Resources for newbies [email protected]
  • Re: [Metamath] Re: Resources for newbies Jim Kingdon
  • Re: [Metamath] Re: Resources for newbies ginx
  • Re: [Metamath] Re: Resources for newbies Norman Megill
  • Re: [Metamath] Re: Resources for newbies Mario Carneiro
  • Re: [Metamath] Re: Resources for newbies ginx
  • Re: [Metamath] Re: Resources for newbies Mario Carneiro
  • Re: [Metamath] Re: Resources for newbies ginx
  • Re: [Metamath] Re: Resources for newbies [email protected]
• [Metamath] Resources for newbies ginx
  • [Metamath] Re: Resources for newbies Norman Megill
  • Re: [Metamath] Re: Resources for newbies 'Stanislas Polu' via Metamath
  • [Metamath] Re: Resources for newbies Norman Megill
  • Re: [Metamath] Re: Resources for newbies David A. Wheeler
  • Re: [Metamath] Re: Resources for newbies David A. Wheeler
• [Metamath] metamath.exe - added "/extract" to "write source" Norman Megill
  • [Metamath] Re: metamath.exe - added "/extract" to "write source" 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: metamath.exe - added "/extract" to "write source" Norman Megill
  • Re: [Metamath] Re: metamath.exe - added "/extract" to "write source" Mario Carneiro
  • Re: [Metamath] Re: metamath.exe - added "/extract" to "write source" Norman Megill
  • [Metamath] Re: metamath.exe - added "/extract" to "write source" 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: metamath.exe - added "/extract" to "write source" Glauco
  • [Metamath] Re: metamath.exe - added "/extract" to "write source" Glauco
  • [Metamath] Re: metamath.exe - added "/extract" to "write source" Glauco
• [Metamath] Fwd: New metamath game on Android Norman Megill
  • Re: [Metamath] Fwd: New metamath game on Android Thierry Arnoux
  • [Metamath] Re: New metamath game on Android Norman Megill
• [Metamath] Overloading symbol names 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Overloading symbol names Steve Rodriguez
  • Re: [Metamath] Overloading symbol names David A. Wheeler
  • [Metamath] Re: Overloading symbol names Norman Megill
  • [Metamath] Re: Overloading symbol names Norman Megill
  • Re: [Metamath] Re: Overloading symbol names Mario Carneiro
  • Re: [Metamath] Re: Overloading symbol names 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Overloading symbol names David A. Wheeler
  • [Metamath] Re: Overloading symbol names Norman Megill
• [Metamath] Matrix indexing start Thierry Arnoux
  • [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Matrix indexing start Benoit
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start Norman Megill
  • Re: [Metamath] Re: Matrix indexing start David A. Wheeler
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start savask
  • Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
  • Re: [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
  • Re: [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Benoit
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start Jim Kingdon
  • [Metamath] Re: Matrix indexing start Norman Megill
  • [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start Norman Megill
  • Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start David A. Wheeler
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
  • Re: [Metamath] Re: Matrix indexing start Norman Megill
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
  • Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• Re: [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs Thierry Arnoux
• [Metamath] The version date of set.mm is less recent than the contribution date for imadifss Glauco
  • [Metamath] Re: The version date of set.mm is less recent than the contribution date for imadifss Norman Megill
  • [Metamath] Re: The version date of set.mm is less recent than the contribution date for imadifss Glauco
• [Metamath] Travis tests are not reliably showing on GitHub David A. Wheeler
  • [Metamath] Re: Travis tests are not reliably showing on GitHub Benoit
  • Re: [Metamath] Re: Travis tests are not reliably showing on GitHub David A. Wheeler
• [Metamath] Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise? Anarcocap-socdem
  • [Metamath] Re: Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise? vvs
  • Re: [Metamath] Re: Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise? David A. Wheeler
• [Metamath] bianir 'roger witte' via Metamath
  • [Metamath] Re: bianir Norman Megill
• [Metamath] Promoting to the main body ad4ant* , ad5ant* and a couple more Glauco
  • [Metamath] Re: Promoting to the main body ad4ant* , ad5ant* and a couple more Norman Megill
  • Re: [Metamath] Promoting to the main body ad4ant* , ad5ant* and a couple more Jim Kingdon
• [Metamath] A < B -> A and B are real and it's use in theorem statements. Jon P
  • [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Jon P
  • Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Mario Carneiro
  • Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Mario Carneiro
  • Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Jon P
  • Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Steve Rodriguez
  • Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Stef O'Rear
  • Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. David A. Wheeler
• [Metamath] Goldbach's conjecture(s) - a challange for (open)AI? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Goldbach's conjecture(s) - a challange for (open)AI? 'Stanislas Polu' via Metamath
  • Re: [Metamath] Goldbach's conjecture(s) - a challange for (open)AI? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? savask
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Mario Carneiro
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Abhishek Chugh
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Mario Carneiro
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Thierry Arnoux
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Jon P
  • [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? savask
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Thierry Arnoux
  • Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? savask
• [Metamath] CICM 2020: Metamath Zero talk Mario Carneiro
  • Re: [Metamath] CICM 2020: Metamath Zero talk Raph Levien
  • Re: [Metamath] CICM 2020: Metamath Zero talk Mario Carneiro
  • Re: [Metamath] CICM 2020: Metamath Zero talk David A. Wheeler
  • [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
  • Re: [Metamath] Re: CICM 2020: Metamath Zero talk Mario Carneiro
  • Re: [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
  • Re: [Metamath] Re: CICM 2020: Metamath Zero talk Mario Carneiro
  • Re: [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
  • Re: [Metamath] Re: CICM 2020: Metamath Zero talk Mario Carneiro
  • Re: [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
• [Metamath] Reworking recursion Scott Fenton
  • [Metamath] Re: Reworking recursion Norman Megill
  • Re: [Metamath] Re: Reworking recursion David A. Wheeler
  • Re: [Metamath] Re: Reworking recursion Scott Fenton
  • Re: [Metamath] Re: Reworking recursion Norman Megill
  • Re: [Metamath] Re: Reworking recursion Jim Kingdon
  • Re: [Metamath] Re: Reworking recursion Benoit
  • Re: [Metamath] Re: Reworking recursion Scott Fenton
  • [Metamath] Re: Reworking recursion 'fl' via Metamath
  • [Metamath] Re: Reworking recursion 'fl' via Metamath
• [Metamath] Graphics in set.mm comments Richard Penner
  • Re: [Metamath] Graphics in set.mm comments David A. Wheeler
  • Re: [Metamath] Graphics in set.mm comments Thierry Arnoux
  • Re: [Metamath] Graphics in set.mm comments Richard Penner
• [Metamath] Now public: Video on proving Schwabhäuser 4.6 David A. Wheeler
  • Re: [Metamath] Now public: Video on proving Schwabhäuser 4.6 David A. Wheeler
• [Metamath] Building Metamath Automation Framework Abhishek Chugh
  • [Metamath] Building Metamath Automation Framework Abhishek Chugh
  • [Metamath] Re: Building Metamath Automation Framework Abhishek Chugh
  • [Metamath] Re: Building Metamath Automation Framework Abhishek Chugh
  • [Metamath] Re: Building Metamath Automation Framework Jon P
  • [Metamath] Re: Building Metamath Automation Framework Abhishek Chugh
• [Metamath] New unlisted video available: "Formalizing Geometric Proof Schwabhäuser 4.6 in the Metamath Proof Explorer" David A. Wheeler
• [Metamath] Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
  • Re: [Metamath] Any comments on my draft presentation Schwabhauser4.6.pptx? Thierry Arnoux
  • [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
  • Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
  • Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? Marnix Klooster
  • Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
  • [Metamath] Any comments on version #3 of my presentation Schwabhauser4.6.pptx? David A. Wheeler
  • Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? Marnix Klooster
• [Metamath] Reminder: We'd love to see more Metamath 100 proofs David A. Wheeler
  • [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs Thomas Brendan Leahy
  • Re: [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs David A. Wheeler
  • [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs 'fl' via Metamath
• [Metamath] Introduction to Sophize Abhishek Chugh
  • Re: [Metamath] Introduction to Sophize Jim Kingdon
  • Re: [Metamath] Introduction to Sophize Abhishek Chugh
  • Re: [Metamath] Introduction to Sophize Mario Carneiro
  • Re: [Metamath] Introduction to Sophize Abhishek Chugh
  • Re: [Metamath] Introduction to Sophize Mario Carneiro
  • Re: [Metamath] Introduction to Sophize Abhishek Chugh
  • Re: [Metamath] Introduction to Sophize David A. Wheeler
  • Re: [Metamath] Introduction to Sophize Abhishek Chugh
• [Metamath] Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
  • [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'ookami' via Metamath
  • Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
  • [Metamath] Responding to David A. Wheeler 'ookami' via Metamath
  • Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
  • Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'ookami' via Metamath
  • [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'fl' via Metamath
  • [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') Norman Megill
  • Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
• [Metamath] Canonical location for Metamath databases Giovanni Mascellani
  • Re: [Metamath] Canonical location for Metamath databases David A. Wheeler
  • Re: [Metamath] Canonical location for Metamath databases Giovanni Mascellani
  • [Metamath] Re: Canonical location for Metamath databases Norman Megill
  • Re: [Metamath] Re: Canonical location for Metamath databases Giovanni Mascellani
  • Re: [Metamath] Re: Canonical location for Metamath databases Norman Megill
• [Metamath] A disproof of LNC? Joseph V
  • [Metamath] Re: A disproof of LNC? Joseph V

• Earlier messages
• Later messages