metamath  

Messages by Date

• 2026/03/10 Re: [Metamath] More than 50.000 theorems in set.mm 'Alexander van der Vekens' via Metamath
• 2026/03/09 Re: [Metamath] More than 50.000 theorems in set.mm Eric Schmidt
• 2026/03/09 Re: [Metamath] More than 50.000 theorems in set.mm 'David A. Wheeler' via Metamath
• 2026/03/09 [Metamath] More than 50.000 theorems in set.mm 'Alexander van der Vekens' via Metamath
• 2026/03/04 [Metamath] [PMC] 2-year anniversary | Deriving minimal single axioms from one another '[email protected]' via Metamath
• 2026/02/23 [Metamath] New proof assistant 'Cernatescu Filip' via Metamath
• 2026/02/20 [Metamath] Hi 'Cernatescu Filip' via Metamath
• 2026/02/19 GPT-5.3-Codex AI vs ω-categories — Re: [Metamath] Introducing ProofScaffold [email protected]
• 2026/02/19 Re: [Metamath] Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath [email protected]
• 2026/02/11 Re: [Metamath] Re: Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Mingli Yuan
• 2026/02/11 Re: [Metamath] Re: Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Mingli Yuan
• 2026/02/11 Re: [Metamath] Re: Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Glauco
• 2026/02/11 Re: [Metamath] Re: Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Mingli Yuan
• 2026/02/11 Re: [Metamath] Re: Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Mingli Yuan
• 2026/02/11 [Metamath] Re: Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Glauco
• 2026/02/10 [Metamath] Introducing ProofScaffold: A Modular, AI-Friendly Toolchain for Metamath Mingli Yuan
• 2026/02/03 [Metamath] How to formalize binary search and similar algorithms? Ender Ting
• 2026/01/17 Re: [Metamath] Use of parentheses for new definitions Ender Ting
• 2026/01/16 Re: [Metamath] Use of parentheses for new definitions 'David A. Wheeler' via Metamath
• 2026/01/15 Re: [Metamath] Use of parentheses for new definitions 'Thierry Arnoux' via Metamath
• 2026/01/15 Re: [Metamath] Use of parentheses for new definitions Matthew House
• 2026/01/15 [Metamath] Use of parentheses for new definitions Ender Ting
• 2026/01/03 [Metamath] Questions about Fitch tableaux in mmb, lean.mm1 'Meta Kunt' via Metamath
• 2026/01/01 Re: [Metamath] tauto.mm1 Gino Giotto
• 2025/12/31 Re: [Metamath] tauto.mm1 Mario Carneiro
• 2025/12/31 [Metamath] tauto.mm1 Gino Giotto
• 2025/12/07 Re: [Metamath] Re: Advent of Metamath 2025 savask
• 2025/12/06 Re: [Metamath] Re: Advent of Metamath 2025 Antony Bartlett
• 2025/12/06 Re: [Metamath] Re: Advent of Metamath 2025 Igor Ieskov
• 2025/12/05 Re: [Metamath] Re: Advent of Metamath 2025 savask
• 2025/12/04 Re: [Metamath] Re: Advent of Metamath 2025 Gino Giotto
• 2025/12/03 Re: [Metamath] Re: Advent of Metamath 2025 Matthew House
• 2025/12/03 Re: [Metamath] Re: Advent of Metamath 2025 savask
• 2025/12/03 Re: [Metamath] Re: Advent of Metamath 2025 Gino Giotto
• 2025/12/02 Re: [Metamath] Re: Advent of Metamath 2025 Gino Giotto
• 2025/12/02 Re: [Metamath] Re: Advent of Metamath 2025 Gino Giotto
• 2025/12/01 Re: [Metamath] Re: Advent of Metamath 2025 Matthew House
• 2025/12/01 AW: [Metamath] Re: Advent of Metamath 2025 'Discher, Samiro' via Metamath
• 2025/12/01 [Metamath] Re: Advent of Metamath 2025 savask
• 2025/12/01 [Metamath] Re: Advent of Metamath 2025 '[email protected]' via Metamath
• 2025/11/30 [Metamath] Advent of Metamath 2025 savask
• 2025/11/29 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Igor Ieskov
• 2025/11/28 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Ender Ting
• 2025/11/28 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Igor Ieskov
• 2025/11/28 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Ender Ting
• 2025/11/22 Re: [Metamath] Inconsistency in old versions of ax-cc Jim Kingdon
• 2025/11/22 Re: [Metamath] Inconsistency in old versions of ax-cc Mario Carneiro
• 2025/11/22 Re: [Metamath] Metamath site down? Mario Carneiro
• 2025/11/22 Re: [Metamath] Metamath site down? lesynajk
• 2025/11/22 Re: [Metamath] Metamath site down? Igor Ieskov
• 2025/11/21 Re: [Metamath] Inconsistency in old versions of ax-cc Matthew House
• 2025/11/21 Re: [Metamath] Inconsistency in old versions of ax-cc Jim Kingdon
• 2025/11/21 [Metamath] Inconsistency in old versions of ax-cc Matthew House
• 2025/11/21 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Marlo Bruder
• 2025/11/21 Re: [Metamath] Metamath site down? Mario Carneiro
• 2025/11/21 Re: [Metamath] Metamath site down? llesyna
• 2025/11/19 Re: [Metamath] Metamath site down? Jim Kingdon
• 2025/11/19 Re: [Metamath] Metamath site down? Mario Carneiro
• 2025/11/17 Re: [Metamath] Metamath site down? 'David A. Wheeler' via Metamath
• 2025/11/17 Re: [Metamath] Metamath site down? [email protected]
• 2025/11/16 Re: [Metamath] Metamath site down? Mario Carneiro
• 2025/11/16 Re: [Metamath] Metamath site down? Falcon Dai
• 2025/11/15 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Ender Ting
• 2025/11/14 Re: [Metamath] MM1 proofs with tactics, how are they created/understood/analyzed ? Mario Carneiro
• 2025/11/14 [Metamath] MM1 proofs with tactics, how are they created/understood/analyzed ? Sylvain Kerjean
• 2025/11/14 Re: [Metamath] Metamath site down? Mario Carneiro
• 2025/11/13 Re: [Metamath] Metamath site down? Mario Carneiro
• 2025/11/13 [Metamath] Metamath site down? Cris Perdue
• 2025/11/11 [Metamath] Principia Mathematica theorems derived from Łukasiewicz axioms [email protected]
• 2025/10/28 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Marlo Bruder
• 2025/10/27 Re: [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Mario Carneiro
• 2025/10/27 [Metamath] A brand new proof assistant called mmt1 is out now. Check it out! Marlo Bruder
• 2025/10/23 Re: [Metamath] metamath-docker and profiling checkmm.cpp 'David A. Wheeler' via Metamath
• 2025/10/23 Re: [Metamath] metamath-docker and profiling checkmm.cpp Mario Carneiro
• 2025/10/22 [Metamath] Re: Can ax-11 be rederived from its DV form without ax-13? Matthew House
• 2025/10/22 [Metamath] Re: Can ax-11 be rederived from its DV form without ax-13? Matthew House
• 2025/10/21 [Metamath] Line 555669 Mázsa Péter
• 2025/10/18 [Metamath] Re: Improved pattern search in metamath-lamp Igor Ieskov
• 2025/10/18 [Metamath] Improved pattern search in metamath-lamp Igor Ieskov
• 2025/10/18 [Metamath] Parsing comments in *.mm files Igor Ieskov
• 2025/10/18 Re: [Metamath] Parsing comments in *.mm files Matthew House
• 2025/10/18 [Metamath] FYI: Seminar "Mathematics in the Age of AI" by Jeremy Avigad (Carnegie Mellon University) 'David A. Wheeler' via Metamath
• 2025/10/18 [Metamath] Can ax-11 be rederived from its DV form without ax-13? Matthew House
• 2025/10/18 [Metamath] Re: checkmm.cpp Eric Schmidt
• 2025/10/18 [Metamath] Re: Can ax-11 be rederived from its DV form without ax-13? Matthew House
• 2025/10/18 Re: [Metamath] Question about mmj2 style unifiers Antony Bartlett
• 2025/10/18 Re: [Metamath] Question about mmj2 style unifiers Antony Bartlett
• 2025/10/18 Re: [Metamath] Question about mmj2 style unifiers Marlo Bruder
• 2025/10/18 Re: [Metamath] Question about mmj2 style unifiers Marlo Bruder
• 2025/10/17 Re: [Metamath] Question about verifier speed Mario Carneiro
• 2025/10/17 Re: [Metamath] Question about verifier speed Marlo Bruder
• 2025/10/17 [Metamath] Question about verifier speed Marlo Bruder
• 2025/10/17 Re: [Metamath] Question about verifier speed Antony Bartlett
• 2025/10/17 Re: [Metamath] Question about verifier speed Marlo Bruder
• 2025/10/17 Re: [Metamath] Question about verifier speed Mario Carneiro
• 2025/10/16 Re: [Metamath] Question about verifier speed Antony Bartlett
• 2025/10/13 [Metamath] metamath-docker and profiling checkmm.cpp Antony Bartlett
• 2025/10/13 Re: [Metamath] Question about mmj2 style unifiers 'Thierry Arnoux' via Metamath
• 2025/10/11 [Metamath] Re: Improved pattern search in metamath-lamp Marlo Bruder
• 2025/10/10 Re: [Metamath] Question about verifier speed Matthew House
• 2025/10/01 Re: [Metamath] API spec for a mmj2 style unifer running on the JavaScript platform Glauco
• 2025/10/01 Re: [Metamath] API spec for a mmj2 style unifer running on the JavaScript platform Glauco
• 2025/10/01 Re: [Metamath] API spec for a mmj2 style unifer running on the JavaScript platform Glauco
• 2025/10/01 Re: [Metamath] API spec for a mmj2 style unifer running on the JavaScript platform Antony Bartlett
• 2025/09/30 Re: [Metamath] Question about mmj2 style unifiers Igor Ieskov
• 2025/09/30 Re: [Metamath] Question about mmj2 style unifiers Igor Ieskov
• 2025/09/28 Re: [Metamath] Question about mmj2 style unifiers Antony Bartlett
• 2025/09/28 Re: [Metamath] Question about mmj2 style unifiers Antony Bartlett
• 2025/09/28 Re: [Metamath] Question about mmj2 style unifiers Glauco
• 2025/09/28 Re: [Metamath] Question about mmj2 style unifiers Marlo Bruder
• 2025/09/27 Re: [Metamath] Question about mmj2 style unifiers Glauco
• 2025/09/27 Re: [Metamath] Question about mmj2 style unifiers Matthew House
• 2025/09/27 Re: [Metamath] Question about mmj2 style unifiers Glauco
• 2025/09/27 [Metamath] Question about mmj2 style unifiers Marlo Bruder
• 2025/09/27 Re: [Metamath] Question about mmj2 style unifiers Matthew House
• 2025/09/20 [Metamath] checkmm.cpp Antony Bartlett
• 2025/09/18 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Zarathustra Goertzel
• 2025/09/17 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Jim Kingdon
• 2025/09/17 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Matthew House
• 2025/09/17 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Jim Kingdon
• 2025/09/17 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] 'David A. Wheeler' via Metamath
• 2025/09/16 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Matthew House
• 2025/09/16 Re: [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Matthew House
• 2025/09/16 [Metamath] Codex wrote an MM verifier in Go pretty easily [AI Progress Report] Zarathustra Goertzel
• 2025/09/13 [Metamath] Re: On a question of Gino Giotto re df-cleq and ax-8 Gino Giotto
• 2025/09/11 Re: [Metamath] Grammatical databases and logical typecodes Matthew House
• 2025/09/11 [Metamath] Grammatical databases and logical typecodes Marlo Bruder
• 2025/09/09 [Metamath] Re: On a question of Gino Giotto re df-cleq and ax-8 Matthew House
• 2025/09/06 [Metamath] Re: On a question of Gino Giotto re df-cleq and ax-8 Matthew House
• 2025/09/06 [Metamath] Re: On a question of Gino Giotto re df-cleq and ax-8 Matthew House
• 2025/09/04 [Metamath] On a question of Gino Giotto re df-cleq and ax-8 Matthew House
• 2025/09/03 Re: [Metamath] Questions about description parsing Mario Carneiro
• 2025/09/03 [Metamath] Questions about description parsing Marlo Bruder
• 2025/09/03 Re: [Metamath] What are first/second order variables in Metamath Zero? Mario Carneiro
• 2025/09/01 Re: [Metamath] What are first/second order variables in Metamath Zero? 'Bulhwi Cha' via Metamath
• 2025/08/29 Re: [Metamath] Are first order variables in Metamath Zero variables of the object logic? Mario Carneiro
• 2025/08/29 Re: [Metamath] What are first/second order variables in Metamath Zero? Mario Carneiro
• 2025/08/29 Re: [Metamath] Are first order variables in Metamath Zero variables of the object logic? 'Bulhwi Cha' via Metamath
• 2025/08/29 [Metamath] What are first/second order variables in Metamath Zero? 'Bulhwi Cha' via Metamath
• 2025/08/29 [Metamath] Are first order variables in Metamath Zero variables of the object logic? 'Bulhwi Cha' via Metamath
• 2025/08/26 [Metamath] Re: Proof Assistants Marlo Bruder
• 2025/08/23 Re: [Metamath] Constructing a well-order from a family of well-orders? Matthew House
• 2025/08/23 Re: [Metamath] Metamath Zero's definition of free variables in an expression Mario Carneiro
• 2025/08/23 Re: [Metamath] Metamath Zero's definition of free variables in an expression 'Bulhwi Cha' via Metamath
• 2025/08/23 Re: [Metamath] Metamath Zero's definition of free variables in an expression Mario Carneiro
• 2025/08/23 Re: [Metamath] Constructing a well-order from a family of well-orders? Mario Carneiro
• 2025/08/22 [Metamath] A modest proposal for the syl renames Matthew House
• 2025/08/22 [Metamath] Metamath Zero's definition of free variables in an expression 'Bulhwi Cha' via Metamath
• 2025/08/21 [Metamath] Constructing a well-order from a family of well-orders? Matthew House
• 2025/08/21 Re: [Metamath] Constructing a well-order from a family of well-orders? Matthew House
• 2025/08/21 Re: [Metamath] Constructing a well-order from a family of well-orders? Mario Carneiro
• 2025/08/21 Re: [Metamath] Constructing a well-order from a family of well-orders? Mario Carneiro
• 2025/08/05 Re: [Metamath] Proposal for two changes to the set axioms of set.mm 'ML' via Metamath
• 2025/08/04 Re: [Metamath] Proposal for two changes to the set axioms of set.mm Jim Kingdon
• 2025/08/04 [Metamath] Proposal for two changes to the set axioms of set.mm 'ML' via Metamath
• 2025/07/28 [Metamath] A curious bug in metamath-exe verification Matthew House
• 2025/07/27 Re: [Metamath] Work variable syntax Jim Kingdon
• 2025/07/27 [Metamath] Re: Work variable syntax Glauco
• 2025/07/27 [Metamath] Work variable syntax Marlo Bruder
• 2025/07/22 Re: [Metamath] Wrong inf symbol 'Thierry Arnoux' via Metamath
• 2025/07/17 [Metamath] Wrong inf symbol Tang Ross
• 2025/07/17 Re: [Metamath] A flaw in the metamath definition system? Mario Carneiro
• 2025/07/13 Re: [Metamath] Digest for [email protected] - 1 update in 1 topic Steven Nguyen
• 2025/07/13 Re: [Metamath] Re: A flaw in the metamath definition system? Jim Kingdon
• 2025/07/13 Re: [Metamath] Digest for [email protected] - 1 update in 1 topic Ludwig Maes
• 2025/07/13 Re: [Metamath] Re: A flaw in the metamath definition system? Steven Nguyen
• 2025/07/13 [Metamath] Re: A flaw in the metamath definition system? Gino Giotto
• 2025/07/13 [Metamath] Re: A flaw in the metamath definition system? savask
• 2025/07/12 [Metamath] A flaw in the metamath definition system? Gino Giotto
• 2025/07/08 Re: [Metamath] Finding the proof I need quickly and efficiently Alessandro Griseta
• 2025/07/04 Re: [Metamath] Finding the proof I need quickly and efficiently Jim Kingdon
• 2025/07/04 [Metamath] Re: Finding the proof I need quickly and efficiently Glauco
• 2025/07/04 Re: Re: [Metamath] Finding the proof I need quickly and efficiently 'Meta Kunt' via Metamath
• 2025/07/04 Re: [Metamath] Finding the proof I need quickly and efficiently Mario Carneiro
• 2025/07/04 [Metamath] Finding the proof I need quickly and efficiently Alessandro Griseta
• 2025/07/01 [Metamath] Invitation to construction of finite fields 'Meta Kunt' via Metamath
• 2025/06/25 [Metamath] Re: Surprising mathematical backgrounds - Pope Leo XIV has a Bachelor's in mathematics 'Alexander van der Vekens' via Metamath
• 2025/06/21 Re: [Metamath] Question about the independence of a statement Benoit
• 2025/06/18 [Metamath] Re: Surprising mathematical backgrounds - Pope Leo XIV has a Bachelor's in mathematics Gino Giotto
• 2025/06/18 [Metamath] Re: Surprising mathematical backgrounds - Pope Leo XIV has a Bachelor's in mathematics Igor Ieskov
• 2025/06/18 [Metamath] Re: Surprising mathematical backgrounds - Pope Leo XIV has a Bachelor's in mathematics 'Alexander van der Vekens' via Metamath
• 2025/06/10 Re: [Metamath] Proof Assistants Steven Nguyen
• 2025/06/10 Re: [Metamath] Re: Proof Assistants Marlo Bruder
• 2025/06/09 Re: [Metamath] Proof Design based on Natural Deduction 'Meta Kunt' via Metamath
• 2025/06/08 Re: [Metamath] Proof Design based on Natural Deduction 'David A. Wheeler' via Metamath
• 2025/06/08 Re: [Metamath] Proof Design based on Natural Deduction [email protected]
• 2025/06/08 Re: [Metamath] Proof Design based on Natural Deduction 'Thierry Arnoux' via Metamath
• 2025/06/08 Re: [Metamath] Proof Design based on Natural Deduction Mario Carneiro
• 2025/06/08 Re: [Metamath] Proof Assistants Igor Ieskov
• 2025/06/07 Re: [Metamath] Proof Assistants Jim Kingdon
• 2025/06/07 [Metamath] Proof Design based on Natural Deduction [email protected]
• 2025/06/07 Re: [Metamath] Re: Proof Assistants 'Thierry Arnoux' via Metamath
• 2025/06/07 [Metamath] Re: Proof Assistants Glauco
• 2025/06/07 [Metamath] Proof Assistants Marlo Bruder
• 2025/06/06 Re: [Metamath] Size of Metamath/set.mm 'Fabian Huch' via Metamath
• 2025/06/06 Re: [Metamath] Size of Metamath/set.mm 'Fabian Huch' via Metamath
• 2025/06/05 Re: [Metamath] Size of Metamath/set.mm Mario Carneiro
• 2025/06/05 Re: [Metamath] Size of Metamath/set.mm 'David A. Wheeler' via Metamath
• 2025/06/05 Re: [Metamath] Size of Metamath/set.mm 'David A. Wheeler' via Metamath
• 2025/06/05 [Metamath] Size of Metamath/set.mm 'Fabian Huch' via Metamath

• Earlier messages