metamath  

Messages by Date

• 2020/10/07 Re: [Metamath] Simple substitution in Metamath 'Alexandre Frechette' via Metamath
• 2020/10/07 Re: [Metamath] Simple substitution in Metamath David A. Wheeler
• 2020/10/07 Re: [Metamath] Simple substitution in Metamath David A. Wheeler
• 2020/10/07 Re: [Metamath] Simple substitution in Metamath Mario Carneiro
• 2020/10/07 [Metamath] Simple substitution in Metamath 'Alexandre Frechette' via Metamath
• 2020/09/25 [Metamath] FYI: Metamath databases, executable, and book are archived as part of the GitHub Arctic Code Vault David A. Wheeler
• 2020/09/24 [Metamath] Re: Automatic proof verification Norman Megill
• 2020/09/24 Re: [Metamath] Automatic proof verification [email protected]
• 2020/09/24 Re: [Metamath] Automatic proof verification David Starner
• 2020/09/23 [Metamath] Automatic proof verification [email protected]
• 2020/09/16 Re: [Metamath] Re: Resources for newbies [email protected]
• 2020/09/16 [Metamath] Re: GPT-f AITP'20 Presentation [email protected]
• 2020/09/15 [Metamath] GPT-f AITP'20 Presentation 'Stanislas Polu' via Metamath
• 2020/09/11 Re: [Metamath] Re: Resources for newbies ginx
• 2020/09/10 Re: [Metamath] Re: Resources for newbies Mario Carneiro
• 2020/09/10 Re: [Metamath] Re: Resources for newbies ginx
• 2020/09/09 Re: [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
• 2020/09/09 Re: [Metamath] GPT-f paper savask
• 2020/09/09 Re: [Metamath] Re: Resources for newbies Mario Carneiro
• 2020/09/09 Re: [Metamath] Re: Resources for newbies Norman Megill
• 2020/09/09 Re: [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
• 2020/09/09 Re: [Metamath] GPT-f paper savask
• 2020/09/09 Re: [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
• 2020/09/09 Re: [Metamath] GPT-f paper David A. Wheeler
• 2020/09/09 Re: [Metamath] Re: Resources for newbies ginx
• 2020/09/09 Re: [Metamath] Going from AM-GM to AM-GM 3 'Stanislas Polu' via Metamath
• 2020/09/09 [Metamath] GPT-f paper 'Stanislas Polu' via Metamath
• 2020/09/08 Re: [Metamath] Going from AM-GM to AM-GM 3 Mario Carneiro
• 2020/09/08 [Metamath] Going from AM-GM to AM-GM 3 'Stanislas Polu' via Metamath
• 2020/09/08 Re: [Metamath] Re: Resources for newbies Jim Kingdon
• 2020/09/08 Re: [Metamath] Re: Resources for newbies [email protected]
• 2020/09/07 Re: [Metamath] Re: Resources for newbies David A. Wheeler
• 2020/09/07 Re: [Metamath] Re: Resources for newbies Thierry Arnoux
• 2020/09/07 Re: [Metamath] Re: Resources for newbies David A. Wheeler
• 2020/09/07 Re: [Metamath] Re: Resources for newbies David A. Wheeler
• 2020/09/07 [Metamath] Re: Resources for newbies Norman Megill
• 2020/09/07 Re: [Metamath] Re: Resources for newbies 'Stanislas Polu' via Metamath
• 2020/09/07 [Metamath] Re: Resources for newbies Norman Megill
• 2020/09/07 [Metamath] Resources for newbies ginx
• 2020/09/06 Re: [Metamath] Re: metamath.exe - added "/extract" to "write source" Norman Megill
• 2020/09/05 [Metamath] Re: metamath.exe - added "/extract" to "write source" 'Alexander van der Vekens' via Metamath
• 2020/09/05 Re: [Metamath] Re: metamath.exe - added "/extract" to "write source" Mario Carneiro
• 2020/09/05 [Metamath] Re: metamath.exe - added "/extract" to "write source" Norman Megill
• 2020/09/05 [Metamath] Re: metamath.exe - added "/extract" to "write source" Glauco
• 2020/09/05 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/05 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/05 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/05 Re: [Metamath] Re: Matrix indexing start Benoit
• 2020/09/04 [Metamath] Re: metamath.exe - added "/extract" to "write source" 'Alexander van der Vekens' via Metamath
• 2020/09/04 Re: [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
• 2020/09/04 Re: [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
• 2020/09/04 [Metamath] metamath.exe - added "/extract" to "write source" Norman Megill
• 2020/09/04 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/03 Re: [Metamath] Re: Matrix indexing start Norman Megill
• 2020/09/03 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/03 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start David A. Wheeler
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Norman Megill
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start 'Stanislas Polu' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 [Metamath] Re: Matrix indexing start Norman Megill
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
• 2020/09/02 Re: [Metamath] Fwd: New metamath game on Android Thierry Arnoux
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start savask
• 2020/09/02 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/09/01 Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
• 2020/09/01 [Metamath] Fwd: New metamath game on Android Norman Megill
• 2020/08/30 Re: [Metamath] Re: Overloading symbol names David A. Wheeler
• 2020/08/30 Re: [Metamath] Re: Overloading symbol names 'Alexander van der Vekens' via Metamath
• 2020/08/30 Re: [Metamath] Re: Overloading symbol names Mario Carneiro
• 2020/08/30 [Metamath] Re: Overloading symbol names Norman Megill
• 2020/08/30 [Metamath] Re: Overloading symbol names Norman Megill
• 2020/08/30 [Metamath] Re: Overloading symbol names Norman Megill
• 2020/08/30 Re: [Metamath] Overloading symbol names David A. Wheeler
• 2020/08/30 [Metamath] Re: Overloading symbol names Steve Rodriguez
• 2020/08/30 [Metamath] Overloading symbol names 'Alexander van der Vekens' via Metamath
• 2020/08/29 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/08/29 Re: [Metamath] Re: Matrix indexing start Thierry Arnoux
• 2020/08/29 Re: [Metamath] Re: Matrix indexing start 'fl' via Metamath
• 2020/08/29 Re: [Metamath] Re: Matrix indexing start David A. Wheeler
• 2020/08/28 Re: [Metamath] Re: Matrix indexing start Norman Megill
• 2020/08/28 Re: [Metamath] Re: Matrix indexing start Jim Kingdon
• 2020/08/28 Re: [Metamath] Re: Matrix indexing start Mario Carneiro
• 2020/08/28 [Metamath] Re: Matrix indexing start Benoit
• 2020/08/28 [Metamath] Re: Matrix indexing start 'Alexander van der Vekens' via Metamath
• 2020/08/28 [Metamath] Matrix indexing start Thierry Arnoux
• 2020/08/26 [Metamath] Re: Reworking recursion 'fl' via Metamath
• 2020/08/23 Re: [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs Thierry Arnoux
• 2020/08/23 [Metamath] Re: Reworking recursion 'fl' via Metamath
• 2020/08/23 [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs 'fl' via Metamath
• 2020/08/22 Re: [Metamath] Re: Travis tests are not reliably showing on GitHub David A. Wheeler
• 2020/08/22 [Metamath] Re: The version date of set.mm is less recent than the contribution date for imadifss Glauco
• 2020/08/22 [Metamath] Re: The version date of set.mm is less recent than the contribution date for imadifss Norman Megill
• 2020/08/22 [Metamath] The version date of set.mm is less recent than the contribution date for imadifss Glauco
• 2020/08/22 [Metamath] Re: Travis tests are not reliably showing on GitHub Benoit
• 2020/08/21 [Metamath] Travis tests are not reliably showing on GitHub David A. Wheeler
• 2020/08/21 Re: [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs David A. Wheeler
• 2020/08/21 [Metamath] Re: Reminder: We'd love to see more Metamath 100 proofs Thomas Brendan Leahy
• 2020/08/20 Re: [Metamath] Re: Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise? David A. Wheeler
• 2020/08/20 [Metamath] Re: Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise? vvs
• 2020/08/20 [Metamath] Could undemostrated theorems be stated as definitions / axioms, in order to solve a problem / exercise? Anarcocap-socdem
• 2020/08/19 [Metamath] Re: The conditional operator for propositions (now with a reference) Benoit
• 2020/08/17 [Metamath] Re: bianir Norman Megill
• 2020/08/17 [Metamath] bianir 'roger witte' via Metamath
• 2020/08/15 Re: [Metamath] Promoting to the main body ad4ant* , ad5ant* and a couple more Jim Kingdon
• 2020/08/15 [Metamath] Re: Promoting to the main body ad4ant* , ad5ant* and a couple more Norman Megill
• 2020/08/15 [Metamath] Promoting to the main body ad4ant* , ad5ant* and a couple more Glauco
• 2020/08/12 Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. David A. Wheeler
• 2020/08/12 Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Stef O'Rear
• 2020/08/12 Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Steve Rodriguez
• 2020/08/12 Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Jon P
• 2020/08/11 Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Mario Carneiro
• 2020/08/11 Re: [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Mario Carneiro
• 2020/08/11 [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. Jon P
• 2020/08/11 [Metamath] Re: A < B -> A and B are real and it's use in theorem statements. 'Alexander van der Vekens' via Metamath
• 2020/08/11 [Metamath] A < B -> A and B are real and it's use in theorem statements. Jon P
• 2020/08/08 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? savask
• 2020/08/08 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Thierry Arnoux
• 2020/08/08 Re: [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
• 2020/08/08 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Jon P
• 2020/08/07 [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? savask
• 2020/08/07 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Thierry Arnoux
• 2020/08/07 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Mario Carneiro
• 2020/08/07 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Abhishek Chugh
• 2020/08/07 Re: [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? Mario Carneiro
• 2020/08/07 [Metamath] Re: Goldbach's conjecture(s) - a challange for (open)AI? savask
• 2020/08/06 Re: [Metamath] Goldbach's conjecture(s) - a challange for (open)AI? 'Alexander van der Vekens' via Metamath
• 2020/08/06 Re: [Metamath] Goldbach's conjecture(s) - a challange for (open)AI? 'Stanislas Polu' via Metamath
• 2020/08/06 [Metamath] Goldbach's conjecture(s) - a challange for (open)AI? 'Alexander van der Vekens' via Metamath
• 2020/08/05 Re: [Metamath] Re: CICM 2020: Metamath Zero talk Mario Carneiro
• 2020/08/05 Re: [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
• 2020/08/03 Re: [Metamath] Re: Reworking recursion Scott Fenton
• 2020/08/02 Re: [Metamath] Re: Reworking recursion Benoit
• 2020/08/02 Re: [Metamath] Re: CICM 2020: Metamath Zero talk Mario Carneiro
• 2020/08/02 Re: [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
• 2020/08/01 Re: [Metamath] Re: Reworking recursion Jim Kingdon
• 2020/08/01 Re: [Metamath] Re: Reworking recursion Norman Megill
• 2020/07/31 Re: [Metamath] Re: CICM 2020: Metamath Zero talk Mario Carneiro
• 2020/07/31 [Metamath] Re: CICM 2020: Metamath Zero talk Jon P
• 2020/07/30 Re: [Metamath] Re: Reworking recursion Scott Fenton
• 2020/07/30 Re: [Metamath] Re: Reworking recursion David A. Wheeler
• 2020/07/30 Re: [Metamath] CICM 2020: Metamath Zero talk David A. Wheeler
• 2020/07/30 [Metamath] Re: Reworking recursion Norman Megill
• 2020/07/30 Re: [Metamath] CICM 2020: Metamath Zero talk Mario Carneiro
• 2020/07/29 Re: [Metamath] CICM 2020: Metamath Zero talk Raph Levien
• 2020/07/29 [Metamath] CICM 2020: Metamath Zero talk Mario Carneiro
• 2020/07/29 [Metamath] Reworking recursion Scott Fenton
• 2020/07/21 [Metamath] Re: Building Metamath Automation Framework Abhishek Chugh
• 2020/07/21 [Metamath] Re: Building Metamath Automation Framework Jon P
• 2020/07/21 Re: [Metamath] Graphics in set.mm comments Richard Penner
• 2020/07/21 [Metamath] Re: Building Metamath Automation Framework Abhishek Chugh
• 2020/07/20 Re: [Metamath] Graphics in set.mm comments Thierry Arnoux
• 2020/07/20 Re: [Metamath] Graphics in set.mm comments David A. Wheeler
• 2020/07/20 [Metamath] Graphics in set.mm comments Richard Penner
• 2020/07/20 [Metamath] Re: Building Metamath Automation Framework Abhishek Chugh
• 2020/07/19 Re: [Metamath] Now public: Video on proving Schwabhäuser 4.6 David A. Wheeler
• 2020/07/19 [Metamath] Now public: Video on proving Schwabhäuser 4.6 David A. Wheeler
• 2020/07/19 Re: [Metamath] OpenAI Proof Assistant for Metamath Jon P
• 2020/07/19 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
• 2020/07/19 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
• 2020/07/19 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
• 2020/07/19 Re: [Metamath] OpenAI Proof Assistant for Metamath Jon P
• 2020/07/18 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
• 2020/07/18 Re: [Metamath] OpenAI Proof Assistant for Metamath Thierry Arnoux
• 2020/07/17 [Metamath] Building Metamath Automation Framework Abhishek Chugh
• 2020/07/17 [Metamath] Any comments on version #3 of my presentation Schwabhauser4.6.pptx? David A. Wheeler
• 2020/07/17 Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
• 2020/07/17 Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? Marnix Klooster
• 2020/07/17 Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? Marnix Klooster
• 2020/07/16 [Metamath] Building Metamath Automation Framework Abhishek Chugh
• 2020/07/16 Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
• 2020/07/16 Re: [Metamath] OpenAI search tool for set.mm theorems Auguste Poiroux
• 2020/07/15 [Metamath] New unlisted video available: "Formalizing Geometric Proof Schwabhäuser 4.6 in the Metamath Proof Explorer" David A. Wheeler
• 2020/07/15 Re: [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
• 2020/07/15 [Metamath] Re: Any comments on my draft presentation Schwabhauser4.6.pptx? 'Alexander van der Vekens' via Metamath
• 2020/07/15 Re: [Metamath] Any comments on my draft presentation Schwabhauser4.6.pptx? Thierry Arnoux
• 2020/07/14 [Metamath] Any comments on my draft presentation Schwabhauser4.6.pptx? David A. Wheeler
• 2020/07/14 Re: [Metamath] Introduction to Sophize Abhishek Chugh
• 2020/07/14 Re: [Metamath] Introduction to Sophize David A. Wheeler
• 2020/07/14 Re: [Metamath] Introduction to Sophize Abhishek Chugh
• 2020/07/14 Re: [Metamath] Introduction to Sophize Mario Carneiro
• 2020/07/14 Re: [Metamath] Introduction to Sophize Abhishek Chugh
• 2020/07/14 Re: [Metamath] Introduction to Sophize Mario Carneiro

• Earlier messages
• Later messages