metamath  

Messages by Date

• 2025/05/30 Re: [Metamath] Question on definitions (in particular for copab) Jim Kingdon
• 2025/05/30 Re: [Metamath] Question on definitions (in particular for copab) [email protected]
• 2025/05/30 Re: [Metamath] Question on definitions (in particular for copab) Mario Carneiro
• 2025/05/30 [Metamath] Question on definitions (in particular for copab) [email protected]
• 2025/05/26 Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
• 2025/05/26 Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
• 2025/05/26 Re: [Metamath] Re: MM0 -> MM translation challenges Jim Kingdon
• 2025/05/26 Re: [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
• 2025/05/25 Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
• 2025/05/25 Re: [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
• 2025/05/25 Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
• 2025/05/25 Re: [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
• 2025/05/25 Re: [Metamath] Re: MM0 -> MM translation challenges Mario Carneiro
• 2025/05/25 [Metamath] Re: MM0 -> MM translation challenges Gino Giotto
• 2025/05/08 [Metamath] Surprising mathematical backgrounds - Pope Leo XIV has a Bachelor's in mathematics 'David A. Wheeler' via Metamath
• 2025/04/30 Re: [Metamath] Utility theorems for numbers Steven Nguyen
• 2025/04/29 Re: [Metamath] Metamath2Py: Python Translation of Metamath Theorems & Dataset Release Pavel Kamenev
• 2025/04/29 Re: [Metamath] Utility theorems for numbers Ender Ting
• 2025/04/29 Re: [Metamath] Utility theorems for numbers 'Meta Kunt' via Metamath
• 2025/04/29 [Metamath] Utility theorems for numbers Ender Ting
• 2025/04/28 Re: [Metamath] *** BUG #1501 Metamath - Version 0.199.pre 29-Jan-2022 'David A. Wheeler' via Metamath
• 2025/04/28 Re: [Metamath] *** BUG #1501 Metamath - Version 0.199.pre 29-Jan-2022 Jim Kingdon
• 2025/04/28 [Metamath] Fastest way to prove that polynomials satisfy UFD property 'Meta Kunt' via Metamath
• 2025/04/27 Re: [Metamath] *** BUG #1501 Metamath - Version 0.199.pre 29-Jan-2022 Caleb Nwokocha
• 2025/04/23 Re: [Metamath] *** BUG #1501 Metamath - Version 0.199.pre 29-Jan-2022 'David A. Wheeler' via Metamath
• 2025/04/23 Re: [Metamath] Metamath2Py: Python Translation of Metamath Theorems & Dataset Release 'David A. Wheeler' via Metamath
• 2025/04/22 [Metamath] *** BUG #1501 Metamath - Version 0.199.pre 29-Jan-2022 Caleb Nwokocha
• 2025/04/22 [Metamath] Metamath2Py: Python Translation of Metamath Theorems & Dataset Release Pavel Kamenev
• 2025/04/11 Re: [Metamath] Definition of product of polynomials. 'Thierry Arnoux' via Metamath
• 2025/04/10 Re: Re: [Metamath] Definition of product of polynomials. 'Meta Kunt' via Metamath
• 2025/04/09 Re: [Metamath] Definition of product of polynomials. 'Thierry Arnoux' via Metamath
• 2025/04/09 [Metamath] Definition of product of polynomials. 'Meta Kunt' via Metamath
• 2025/04/05 Re: [Metamath] Massive improvements found for pmproofs.txt and 1-base challenge Jim Kingdon
• 2025/04/05 Re: [Metamath] Massive improvements found for pmproofs.txt and 1-base challenge [email protected]
• 2025/03/30 [Metamath] Re: Automating theorems-from-text: database formatting Ender Ting
• 2025/03/28 [Metamath] Projection functions ducourtial.metamath.monologue534 via Metamath
• 2025/03/28 [Metamath] Re: Automating theorems-from-text: database formatting Glauco
• 2025/03/28 [Metamath] Re: Automating theorems-from-text: database formatting Ender Ting
• 2025/03/28 Re: [Metamath] Automating theorems-from-text: database formatting 'Thierry Arnoux' via Metamath
• 2025/03/28 Re: [Metamath] Automating theorems-from-text: database formatting 'Thierry Arnoux' via Metamath
• 2025/03/28 [Metamath] Re: Automating theorems-from-text: database formatting Glauco
• 2025/03/27 [Metamath] Automating theorems-from-text: database formatting Ender Ting
• 2025/03/19 [Metamath] Re: Yamma 0.0.19 Released: Glauco
• 2025/03/19 [Metamath] Yamma 0.0.19 Released: Glauco
• 2025/03/19 Re: Re: [Metamath] Greetings ducourtial.metamath.monologue534 via Metamath
• 2025/03/18 Re: [Possible phishing attempt] Re: [Metamath] Greetings Glauco
• 2025/03/18 Re: [Possible phishing attempt] Re: [Metamath] Greetings Glauco
• 2025/03/18 Re: [Possible phishing attempt] Re: [Metamath] Greetings ducourtial.metamath.monologue534 via Metamath
• 2025/03/17 Re: [Metamath] Greetings Jim Kingdon
• 2025/03/17 [Metamath] Greetings ducourtial.metamath.monologue534 via Metamath
• 2025/03/01 [Metamath] Re: Question on Theorem rspc about distinct variables Glauco
• 2025/03/01 Re: [Metamath] Question on Theorem rspc about distinct variables 'Thierry Arnoux' via Metamath
• 2025/03/01 [Metamath] Question on Theorem rspc about distinct variables [email protected]
• 2025/02/26 Re: [Metamath] Massive improvements found for pmproofs.txt and 1-base challenge 'David A. Wheeler' via Metamath
• 2025/02/26 [Metamath] Massive improvements found for pmproofs.txt and 1-base challenge [email protected]
• 2025/02/24 Re: [Metamath] Re: Error about the fact that type specified by $f statement is global even if variable is not. Mario Carneiro
• 2025/02/24 [Metamath] Re: Error about the fact that type specified by $f statement is global even if variable is not. Glauco
• 2025/02/22 [Metamath] Re: Metamath website - restarted, regen to restart tomorrow Glauco
• 2025/02/17 [Metamath] AI: OpenThinker by Open Thoughts [email protected]
• 2025/02/13 Re: [Metamath] Metamath website - restarted, regen to restart tomorrow Jim Kingdon
• 2025/02/13 [Metamath] Metamath website - restarted, regen to restart tomorrow 'David A. Wheeler' via Metamath
• 2025/02/10 Re: [Metamath] Yamma 0.0.18 Released: 'Thierry Arnoux' via Metamath
• 2025/02/09 [Metamath] Re: Yamma 0.0.18 Released: Glauco
• 2025/02/09 [Metamath] Yamma 0.0.18 Released: Glauco
• 2025/02/08 [Metamath] Metamath-lamp version 27 released Igor Ieskov
• 2025/02/08 Re: [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub [email protected]
• 2025/02/08 Re: [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub Caleb Nwokocha
• 2025/02/08 Re: [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub Glauco
• 2025/02/07 Re: [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub 'David A. Wheeler' via Metamath
• 2025/02/07 Re: [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub [email protected]
• 2025/02/07 Re: [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub 'David A. Wheeler' via Metamath
• 2025/02/06 [Metamath] Re: AI Generative Pretrained Transformer model for Metamath: GitHub [email protected]
• 2025/02/06 [Metamath] AI Generative Pretrained Transformer model for Metamath: GitHub [email protected]
• 2025/01/29 [Metamath] Error about the fact that type specified by $f statement is global even if variable is not. Sylvain Kerjean
• 2025/01/27 [Metamath] Re: Bourbaki and Metamath Sylvain Kerjean
• 2025/01/26 AW: [Metamath] Re: Upcoming contributions to proof minimization challenges Discher, Samiro
• 2025/01/25 [Metamath] Re: Yamma Glauco
• 2025/01/23 Re: [Metamath] Conditional Derivations (Carnap Book) Jim Kingdon
• 2025/01/23 [Metamath] Conditional Derivations (Carnap Book) jagra
• 2025/01/21 [Metamath] Re: Bourbaki and Metamath Sylvain Kerjean
• 2025/01/20 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/20 Re: [Metamath] Questions on doing more Set Theory and Metamath 'Thierry Arnoux' via Metamath
• 2025/01/20 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/19 Re: [Metamath] Questions on doing more Set Theory and Metamath Jim Kingdon
• 2025/01/19 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/19 Re: [Metamath] Re: Tactics for finding Metamath proofs in propositional logic Gino Giotto
• 2025/01/17 Re: [Metamath] [Lamp] add axiom/definition ? 'David A. Wheeler' via Metamath
• 2025/01/16 [Metamath] Re: [Lamp] add axiom/definition ? Igor Ieskov
• 2025/01/16 Re: [Metamath] Re: Tactics for finding Metamath proofs in propositional logic Mario Carneiro
• 2025/01/16 [Metamath] [Lamp] add axiom/definition ? Sylvain Kerjean
• 2025/01/16 Re: [Metamath] Questions on doing more Set Theory and Metamath Jim Kingdon
• 2025/01/16 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/16 Re: [Metamath] Questions on doing more Set Theory and Metamath 'Alexander van der Vekens' via Metamath
• 2025/01/16 Re: [Metamath] Questions on doing more Set Theory and Metamath savask
• 2025/01/16 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/15 Re: [Metamath] Questions on doing more Set Theory and Metamath Jim Kingdon
• 2025/01/15 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/14 Re: [Metamath] LAMP axiom/definition (and freeness) Steven Nguyen
• 2025/01/14 [Metamath] Re: Tactics for finding Metamath proofs in propositional logic Gino Giotto
• 2025/01/14 [Metamath] Re: Tactics for finding Metamath proofs in propositional logic Glauco
• 2025/01/14 Re: [Metamath] LAMP axiom/definition (and freeness) Sylvain Kerjean
• 2025/01/14 Re: [Metamath] Tactics for finding Metamath proofs in propositional logic 'Thierry Arnoux' via Metamath
• 2025/01/14 [Metamath] Tactics for finding Metamath proofs in propositional logic Gino Giotto
• 2025/01/13 Re: [Metamath] Questions on doing more Set Theory and Metamath 'Andrew Thompson Thompson' via Metamath
• 2025/01/13 Re: [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/13 Re: [Metamath] LAMP axiom/definition Igor Ieskov
• 2025/01/13 Re: [Metamath] Questions on doing more Set Theory and Metamath Scott Fenton
• 2025/01/13 Re: [Metamath] LAMP axiom/definition 'David A. Wheeler' via Metamath
• 2025/01/13 [Metamath] LAMP axiom/definition Sylvain Kerjean
• 2025/01/12 Re: [Metamath] Questions on doing more Set Theory and Metamath Jim Kingdon
• 2025/01/12 [Metamath] Re: Questions on doing more Set Theory and Metamath Glauco
• 2025/01/12 [Metamath] Questions on doing more Set Theory and Metamath Noam Pasman
• 2025/01/10 Re: [Metamath] Re: Upcoming contributions to proof minimization challenges Gino Giotto
• 2025/01/09 Re: [Metamath] Re: Upcoming contributions to proof minimization challenges [email protected]
• 2025/01/08 AW: [Metamath] Re: Upcoming contributions to proof minimization challenges Discher, Samiro
• 2025/01/08 [Metamath] Re: Upcoming contributions to proof minimization challenges Gino Giotto
• 2025/01/08 Re: [Metamath] Conway's Surreal numbers Jim Kingdon
• 2025/01/08 Re: [Metamath] some questions about wffs in set.mm Richard Penner
• 2025/01/08 Re: [Metamath] Conway's Surreal numbers Scott Fenton
• 2025/01/08 [Metamath] Conway's Surreal numbers Richard Penner
• 2025/01/06 Re: [Metamath] a Nim verifier (and yamma's MmParser.ts) Glauco
• 2025/01/06 [Metamath] Upcoming contributions to proof minimization challenges [email protected]
• 2025/01/06 Re: [Metamath] Advent of Metamath 2024 'Thierry Arnoux' via Metamath
• 2025/01/04 Re: [Metamath] a Nim verifier (and yamma's MmParser.ts) Jim Kingdon
• 2025/01/04 Re: [Metamath] Feedback from metakunt, a recent contributor 'Andrew Thompson Thompson' via Metamath
• 2025/01/04 Re: [Metamath] Feedback from metakunt, a recent contributor Jim Kingdon
• 2025/01/04 [Metamath] a Nim verifier (and yamma's MmParser.ts) Glauco
• 2025/01/04 [Metamath] Re: brismu: a relational interpretation of Lojban Glauco
• 2025/01/04 Re: [Metamath] Feedback from metakunt, a recent contributor 'Andrew Thompson Thompson' via Metamath
• 2025/01/04 Re: [Metamath] some questions about wffs in set.mm 'Peter Dolland' via Metamath
• 2025/01/04 [Metamath] Re: Feedback from metakunt, a recent contributor Glauco
• 2025/01/03 [Metamath] Re: brismu: a relational interpretation of Lojban [email protected]
• 2025/01/03 [Metamath] Re: brismu: a relational interpretation of Lojban Glauco
• 2025/01/03 Re: [Metamath] brismu: a relational interpretation of Lojban 'David A. Wheeler' via Metamath
• 2025/01/03 Re: [Metamath] some questions about wffs in set.mm Jim Kingdon
• 2025/01/03 [Metamath] some questions about wffs in set.mm 'Peter Dolland' via Metamath
• 2025/01/02 [Metamath] brismu: a relational interpretation of Lojban [email protected]
• 2025/01/01 Re: [Metamath] Re: Yamma Jim Kingdon
• 2025/01/01 [Metamath] Re: Yamma Glauco
• 2025/01/01 [Metamath] Re: Yamma Glauco
• 2024/12/27 AW: [Metamath] Article "Mathematicians found – and fixed – an error in a 60-year-old proof" (New Scientist) Discher, Samiro
• 2024/12/27 [Metamath] Article "Mathematicians found – and fixed – an error in a 60-year-old proof" (New Scientist) 'David A. Wheeler' via Metamath
• 2024/12/27 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/24 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/19 [Metamath] Re: Yamma Glauco
• 2024/12/18 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/18 Re: [Metamath] Advent of Metamath 2024 'David A. Wheeler' via Metamath
• 2024/12/17 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/16 Re: [Metamath] Advent of Metamath 2024 'Thierry Arnoux' via Metamath
• 2024/12/16 Re: [Metamath] Disjointness in set.mm 'Peter Dolland' via Metamath
• 2024/12/15 Re: [Metamath] Disjointness in set.mm Mario Carneiro
• 2024/12/15 Re: [Metamath] Disjointness in set.mm 'Peter Dolland' via Metamath
• 2024/12/14 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/14 Re: [Metamath] Advent of Metamath 2024 Mario Carneiro
• 2024/12/14 Re: [Metamath] Advent of Metamath 2024 [email protected]
• 2024/12/14 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/14 Re: [Metamath] Disjointness in set.mm 'Peter Dolland' via Metamath
• 2024/12/14 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/14 Re: [Metamath] Disjointness in set.mm Mario Carneiro
• 2024/12/14 [Metamath] Disjointness in set.mm 'Peter Dolland' via Metamath
• 2024/12/13 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/13 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/13 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/11 Re: [Metamath] Advent of Metamath 2024 Glauco
• 2024/12/11 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/11 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/10 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/09 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/09 Re: [Metamath] Advent of Metamath 2024 'David A. Wheeler' via Metamath
• 2024/12/09 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/08 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/08 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/08 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/08 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/07 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/07 Re: [Metamath] Advent of Metamath 2024 Igor Ieskov
• 2024/12/06 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/06 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/06 [Metamath] AI for Math Fund announcement 'Sarah Constantin' via Metamath
• 2024/12/05 Re: [Metamath] Advent of Metamath 2024 Glauco
• 2024/12/05 Re: [Metamath] Advent of Metamath 2024 Igor Ieskov
• 2024/12/04 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/03 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/03 Re: [Metamath] Re: combinatorics 'Peter Dolland' via Metamath
• 2024/12/03 Re: [Metamath] Re: combinatorics 'Peter Dolland' via Metamath
• 2024/12/03 Re: [Metamath] Re: combinatorics 'Peter Dolland' via Metamath
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 'Thierry Arnoux' via Metamath
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 Glauco
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 Gino Giotto
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 Glauco
• 2024/12/02 [Metamath] Re: Advent of Metamath 2024 Benoit
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 Mario Carneiro
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 Igor Ieskov
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 'Thierry Arnoux' via Metamath
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 Jorge Agra
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 savask
• 2024/12/02 Re: [Metamath] Advent of Metamath 2024 'Thierry Arnoux' via Metamath
• 2024/11/30 [Metamath] Advent of Metamath 2024 savask
• 2024/11/30 [Metamath] Copying df-plfl to my mathbox 'Meta Kunt' via Metamath

• Earlier messages
• Later messages