metamath  

Messages by Thread

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

• Earlier messages