metamath  

Messages by Date

• 2021/11/15 Re: [Metamath] Excluding (/) from extensible structure to be a function David A. Wheeler
• 2021/11/15 Re: [Metamath] Excluding (/) from extensible structure to be a function 'Alexander van der Vekens' via Metamath
• 2021/11/14 Re: [Metamath] Excluding (/) from extensible structure to be a function Mario Carneiro
• 2021/11/14 [Metamath] Excluding (/) from extensible structure to be a function 'Alexander van der Vekens' via Metamath
• 2021/11/14 Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM) Antony Bartlett
• 2021/11/13 Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM) Mario Carneiro
• 2021/11/13 Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM) Mario Carneiro
• 2021/11/13 Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM) Antony Bartlett
• 2021/11/13 [Metamath] AGI research on metamath and grant proposals Jon P
• 2021/11/08 [Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request? Norman Megill
• 2021/11/06 [Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request? Benoit
• 2021/11/06 [Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request? 'Alexander van der Vekens' via Metamath
• 2021/11/05 Re: [Metamath] Valuation Jim Kingdon
• 2021/11/05 Re: [Metamath] Valuation Kyle Wyonch
• 2021/11/05 Re: [Metamath] Valuation Thierry Arnoux
• 2021/11/04 [Metamath] Valuation Jim Kingdon
• 2021/11/04 Re: [Metamath] New community verifier? Thierry Arnoux
• 2021/11/04 Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Glauco
• 2021/11/04 Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Jim Kingdon
• 2021/11/04 Re: [Metamath] New community verifier? Zheng Fan
• 2021/11/04 Re: [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Mario Carneiro
• 2021/11/04 [Metamath] Mandatory "standard" formatting prior to submitting a pull request? Glauco
• 2021/11/02 Re: [Metamath] Two cleanliness scripts Jerry James
• 2021/11/02 Re: [Metamath] Two cleanliness scripts Benoit
• 2021/11/01 Re: [Metamath] Two cleanliness scripts Jerry James
• 2021/11/01 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Thierry Arnoux
• 2021/11/01 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/11/01 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/11/01 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/11/01 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/11/01 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Thierry Arnoux
• 2021/10/31 Re: [Metamath] Two cleanliness scripts Benoit
• 2021/10/31 Re: [Metamath] Two cleanliness scripts Jerry James
• 2021/10/31 Re: [Metamath] Two cleanliness scripts Benoit
• 2021/10/31 [Metamath] Superior limit Benoit
• 2021/10/31 Re: [Metamath] Two cleanliness scripts Jerry James
• 2021/10/31 [Metamath] Re: Meta Benoit
• 2021/10/31 [Metamath] Meta 'Alexander van der Vekens' via Metamath
• 2021/10/30 Re: [Metamath] Two cleanliness scripts Benoit
• 2021/10/29 Re: [Metamath] Two cleanliness scripts Jerry James
• 2021/10/29 Re: [Metamath] Two cleanliness scripts Jerry James
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/10/29 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/29 Re: [Metamath] Two cleanliness scripts Benoit
• 2021/10/28 Re: [Metamath] Two cleanliness scripts Thierry Arnoux
• 2021/10/28 [Metamath] Two cleanliness scripts Jerry James
• 2021/10/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/10/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Scott Fenton
• 2021/10/28 [Metamath] Definitions vs "conservative and eliminable" Cris Perdue
• 2021/10/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Thierry Arnoux
• 2021/10/28 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Benoit
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/27 [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Norman Megill
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/27 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/10/26 Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) Mario Carneiro
• 2021/10/26 [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq) 'ookami' via Metamath
• 2021/10/26 [Metamath] Re: Erweiterung df-cleq Norman Megill
• 2021/10/26 [Metamath] Erweiterung df-cleq 'ookami' via Metamath
• 2021/10/20 Re: [Metamath] Proof-of-concept for 'syntax axiom based parsing' Thierry Arnoux
• 2021/10/20 [Metamath] Free Azure credits for open source projects - might be useful for Metamath David A. Wheeler
• 2021/10/20 [Metamath] Proof-of-concept for 'syntax axiom based parsing' Marnix Klooster
• 2021/10/06 Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM) Antony Bartlett
• 2021/10/01 Re: [Metamath] Is there a proof for "2+2=4" without passing through the reals? David A. Wheeler
• 2021/10/01 [Metamath] Re: Is there a proof for "2+2=4" without passing through the reals? Norman Megill
• 2021/10/01 [Metamath] Re: Is there a proof for "2+2=4" without passing through the reals? Anarcocap-socdem
• 2021/10/01 [Metamath] Re: Is there a proof for "2+2=4" without passing through the reals? Norman Megill
• 2021/10/01 [Metamath] Is there a proof for "2+2=4" without passing through the reals? Anarcocap-socdem
• 2021/09/30 Re: [Metamath] An attempt to build Metamath for WebAssembly (WASM) Mario Carneiro
• 2021/09/30 [Metamath] An attempt to build Metamath for WebAssembly (WASM) Antony Bartlett
• 2021/09/29 Re: [Metamath] Re: Reopened: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/24 Re: [Metamath] Re: Reopened: How to define 'Not Free' Benoit
• 2021/09/24 Re: [Metamath] Multiple Typesetting Comments David A. Wheeler
• 2021/09/21 [Metamath] Re: Multiple Typesetting Comments Brian Larson
• 2021/09/21 Re: [Metamath] Re: Reopened: How to define 'Not Free' Jim Kingdon
• 2021/09/21 [Metamath] Re: Reopened: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/21 [Metamath] Re: Reopened: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/20 [Metamath] Re: mmj2 on Java 13? 'Alexander van der Vekens' via Metamath
• 2021/09/20 Re: [Metamath] Multiple Typesetting Comments Brian Larson
• 2021/09/20 [Metamath] Re: Multiple Typesetting Comments Norman Megill
• 2021/09/20 [Metamath] Re: mmj2 on Java 13? Brian Larson
• 2021/09/20 [Metamath] mmj2 on Java 13? Brian Larson
• 2021/09/19 [Metamath] Multiple Typesetting Comments Brian Larson
• 2021/09/17 [Metamath] Re: How tricky is it to define predicate calculus without equality? Norman Megill
• 2021/09/17 [Metamath] How tricky is it to define predicate calculus without equality? Gustavo Gonçalves
• 2021/09/12 Re: [Metamath] Metamath and Reverse math Mingli Yuan
• 2021/09/12 Re: [Metamath] Metamath and Reverse math Jim Kingdon
• 2021/09/12 [Metamath] Re: Reopened: How to define 'Not Free' Benoit
• 2021/09/12 [Metamath] Metamath and Reverse math Mingli Yuan
• 2021/09/12 [Metamath] Re: Reopened: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/12 Re: [Metamath] Reopen: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/12 Re: [Metamath] Reopen: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/12 Re: [Metamath] Reopen: How to define 'Not Free' Mario Carneiro
• 2021/09/12 [Metamath] Reopened: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/12 [Metamath] Reopen: How to define 'Not Free' 'ookami' via Metamath
• 2021/09/11 Re: [Metamath] would fvexd be a bad idea? Norman Megill
• 2021/09/10 Re: [Metamath] would fvexd be a bad idea? Benoit
• 2021/09/09 Re: [Metamath] would fvexd be a bad idea? 'Alexander van der Vekens' via Metamath
• 2021/09/08 Re: [Metamath] would fvexd be a bad idea? 'ookami' via Metamath
• 2021/09/05 Re: [Metamath] would fvexd be a bad idea? Jim Kingdon
• 2021/09/05 [Metamath] would fvexd be a bad idea? Glauco
• 2021/08/28 Re: [Metamath] New community verifier? David A. Wheeler
• 2021/08/17 Re: [Metamath] New community verifier? Mario Carneiro
• 2021/08/17 Re: [Metamath] New community verifier? Thierry Arnoux
• 2021/08/16 Re: [Metamath] New community verifier? Mario Carneiro
• 2021/08/16 Re: [Metamath] New community verifier? Thierry Arnoux
• 2021/08/15 Re: [Metamath] New community verifier? Mario Carneiro
• 2021/08/15 Re: [Metamath] New community verifier? David A. Wheeler
• 2021/08/15 Re: [Metamath] New community verifier? Norman Megill
• 2021/08/15 Re: HF set theory – Re: [Metamath] Predicate Calculus Functions Norman Megill
• 2021/08/15 Re: HF set theory – Re: [Metamath] Predicate Calculus Functions Scott Fenton
• 2021/08/15 Re: HF set theory – Re: [Metamath] Predicate Calculus Functions Scott Fenton
• 2021/08/15 HF set theory – Re: [Metamath] Predicate Calculus Functions Ken Kubota
• 2021/08/15 Re: [Metamath] New community verifier? Mario Carneiro
• 2021/08/15 Re: [Metamath] New community verifier? Thierry Arnoux
• 2021/08/14 Re: [Metamath] Predicate Calculus Functions Thierry Arnoux
• 2021/08/14 [Metamath] Predicate Calculus Functions Scott Fenton
• 2021/07/28 [Metamath] Re: Moving my theorems to the main body - principal objections, too long, fruit of the poison tree. savask
• 2021/07/28 [Metamath] Moving my theorems to the main body - principal objections, too long, fruit of the poison tree. [email protected]
• 2021/07/23 [Metamath] Re: The second supplement to the law of quadratic reciprocity. 'Alexander van der Vekens' via Metamath
• 2021/07/22 [Metamath] Re: List of most frequently used assertions 'Alexander van der Vekens' via Metamath
• 2021/07/21 [Metamath] Re: List of most frequently used assertions Norman Megill
• 2021/07/20 [Metamath] Re: List of most frequently used assertions 'Alexander van der Vekens' via Metamath
• 2021/07/19 [Metamath] Re: List of most frequently used assertions Norman Megill
• 2021/07/19 [Metamath] List of most frequently used assertions Kyle Wyonch
• 2021/07/03 Re: [Metamath] Wondering what is the minimum syntax needed for everything? Mario Carneiro
• 2021/07/03 Re: [Metamath] Wondering what is the minimum syntax needed for everything? Jim Kingdon
• 2021/07/03 [Metamath] Wondering what is the minimum syntax needed for everything? Gustavo Gonçalves
• 2021/06/22 [Metamath] Re: 0 = 1 (in peano.mm) Benoit
• 2021/06/22 Re: [Metamath] Re: 0 = 1 (in peano.mm) Jim Kingdon
• 2021/06/22 [Metamath] Re: 0 = 1 (in peano.mm) Patrick Brosnan
• 2021/06/21 [Metamath] Re: 0 = 1 (in peano.mm) Benoit
• 2021/06/21 [Metamath] 0 = 1 (in peano.mm) Patrick Brosnan
• 2021/06/21 Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory Thierry Arnoux
• 2021/06/20 Re: [Metamath] The second supplement to the law of quadratic reciprocity. Thierry Arnoux
• 2021/06/20 [Metamath] The second supplement to the law of quadratic reciprocity. 'Alexander van der Vekens' via Metamath
• 2021/06/19 Re: [Metamath] Moving forward to weighted AM-GM inequality Thierry Arnoux
• 2021/06/19 [Metamath] Moving forward to weighted AM-GM inequality Kunhao Zheng
• 2021/06/18 Re: [Metamath] Recommendations for metamath hosting? Ashok Khanna
• 2021/06/16 Re: [Metamath] Re: Recommendations for metamath hosting? heiphohmia via Metamath
• 2021/06/16 Re: [Metamath] Re: Recommendations for metamath hosting? Norman Megill
• 2021/06/15 Re: [Metamath] Re: Recommendations for metamath hosting? Norman Megill
• 2021/06/14 Re: [Metamath] Re: Recommendations for metamath hosting? Cris Perdue
• 2021/06/14 [Metamath] Re: Recommendations for metamath hosting? Norman Megill
• 2021/06/14 Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory Mario Carneiro
• 2021/06/14 Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory Kunhao Zheng
• 2021/06/12 Re: [Metamath] Recommendations for metamath hosting? Cris Perdue
• 2021/06/12 Re: [Metamath] Recommendations for metamath hosting? Mázsa Péter
• 2021/06/12 [Metamath] Recommendations for metamath hosting? David A. Wheeler
• 2021/06/10 Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :) 'Stanislas Polu' via Metamath
• 2021/06/09 Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :) Norman Megill
• 2021/06/09 Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :) Mario Carneiro
• 2021/06/09 Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory Thierry Arnoux
• 2021/06/09 [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :) Jon P
• 2021/06/09 Re: [Metamath] [Question of Formalization & Proof] Inverse in number theory Thierry Arnoux
• 2021/06/09 [Metamath] [Question of Formalization & Proof] Inverse in number theory Kunhao Zheng
• 2021/06/07 Re: [Metamath] Metamath verifier in Zig Thierry Arnoux
• 2021/06/06 Re: [Metamath] Revision of PART 16 GRAPH THEORY in set.mm David A. Wheeler
• 2021/06/05 [Metamath] Revision of PART 16 GRAPH THEORY in set.mm 'Alexander van der Vekens' via Metamath
• 2021/05/16 Re: [Metamath] Planning to change mreexexd in main database. David A. Wheeler
• 2021/05/14 [Metamath] Re: Planning to change mreexexd in main database. Benoit
• 2021/05/14 [Metamath] Re: Planning to change mreexexd in main database. Norman Megill
• 2021/05/14 [Metamath] Planning to change mreexexd in main database. [email protected]
• 2021/05/09 Re: [Metamath] Re: Metamath verifier in Lean 4 Mario Carneiro
• 2021/05/09 Re: [Metamath] Re: Metamath verifier in Lean 4 Mario Carneiro
• 2021/05/09 [Metamath] Re: Metamath verifier in Lean 4 Benoit
• 2021/05/09 [Metamath] Re: Metamath verifier in Lean 4 vvs
• 2021/05/08 Re: [Metamath] Re: Metamath verifier in Lean 4 Norman Megill
• 2021/05/08 Re: [Metamath] Re: Metamath verifier in Lean 4 Mario Carneiro
• 2021/05/08 Re: [Metamath] Re: Metamath verifier in Lean 4 Norman Megill
• 2021/05/08 Re: [Metamath] Re: Metamath verifier in Lean 4 Mario Carneiro
• 2021/05/08 [Metamath] Re: Metamath verifier in Lean 4 vvs
• 2021/05/07 [Metamath] Metamath verifier in Lean 4 Mario Carneiro
• 2021/05/06 Re: [Metamath] Metamath verifier in Zig Marnix Klooster
• 2021/05/05 Re: [Metamath] Metamath verifier in Zig Mario Carneiro
• 2021/05/05 [Metamath] Metamath verifier in Zig Marnix Klooster
• 2021/05/04 Re: [Metamath] [Question on Formalization] How can I write number in base other than 10 Kunhao Zheng
• 2021/05/01 [Metamath] Something useful, perhaps. ocatmetamath
• 2021/05/01 Re: [Metamath] [Question on Formalization] How can I write number in base other than 10 David A. Wheeler
• 2021/05/01 [Metamath] Re: [Question on Formalization] How can I write number in base other than 10 Glauco
• 2021/05/01 Re: [Metamath] Re: [Question on Formalization] How can I write number in base other than 10 'Alexander van der Vekens' via Metamath

• Earlier messages
• Later messages