metamath  

Messages by Thread

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

• Earlier messages
• Later messages