metamath

Messages by Date

2023/02/27 Re: [Metamath] Future website directions David A. Wheeler
2023/02/27 Re: [Metamath] Metamatix Thierry Arnoux
2023/02/26 Re: [Metamath] Future website directions Mario Carneiro
2023/02/26 Re: [Metamath] Future website directions David A. Wheeler
2023/02/26 Re: [Metamath] Metamatix David A. Wheeler
2023/02/25 Re: [Metamath] Future website directions Mario Carneiro
2023/02/25 Re: [Metamath] Future website directions Jon P
2023/02/25 [Metamath] Metamatix Thierry Arnoux
2023/02/24 [Metamath] Re: An exhaustive generator for the mmsolitaire project Samiro Discher
2023/02/20 Re: [Metamath] Re: Formalizing Fermat's Last Theorem Mario Carneiro
2023/02/20 Re: [Metamath] Re: Formalizing Fermat's Last Theorem Jim Kingdon
2023/02/20 Re: [Metamath] Re: Formalizing Fermat's Last Theorem David Crisp
2023/02/20 Re: [Metamath] shorter proofs for some theorems in set.mm Thierry Arnoux
2023/02/20 Re: [Metamath] shorter proofs for some theorems in set.mm Igor Ieskov
2023/02/19 Re: [Metamath] Future website directions David A. Wheeler
2023/02/19 Re: [Metamath] Future website directions Glauco
2023/02/19 Re: [Metamath] Future website directions Antony Bartlett
2023/02/19 Re: [Metamath] Future website directions Mario Carneiro
2023/02/19 [Metamath] Future website directions David A. Wheeler
2023/02/19 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
2023/02/19 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
2023/02/19 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Antony Bartlett
2023/02/18 Re: [Metamath] Re: Formalizing Fermat's Last Theorem Jim Kingdon
2023/02/18 [Metamath] Re: Formalizing Fermat's Last Theorem Steven Nguyen
2023/02/18 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
2023/02/18 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/18 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
2023/02/18 Re: [Metamath] shorter proofs for some theorems in set.mm Benoit
2023/02/18 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/18 [Metamath] Re: Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Benoit
2023/02/18 Re: [Metamath] shorter proofs for some theorems in set.mm Benoit
2023/02/17 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Cris Perdue
2023/02/17 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
2023/02/17 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Auguste Poiroux
2023/02/16 [Metamath] Formalizing Fermat's Last Theorem Jim Kingdon
2023/02/16 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/16 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Jon P
2023/02/16 Re: [Metamath] shorter proofs for some theorems in set.mm David A. Wheeler
2023/02/16 Re: [Metamath] shorter proofs for some theorems in set.mm Igor Ieskov
2023/02/16 Re: [Metamath] shorter proofs for some theorems in set.mm 'Alexander van der Vekens' via Metamath
2023/02/16 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/16 Re: [Metamath] shorter proofs for some theorems in set.mm David A. Wheeler
2023/02/15 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/15 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Johnathan Mercer
2023/02/15 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/15 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Igor Ieskov
2023/02/15 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David Wheeler
2023/02/14 Re: [Metamath] Fyi: Linode rebrand heiphohmia via Metamath
2023/02/14 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Igor Ieskov
2023/02/14 [Metamath] Fyi: Linode rebrand David A. Wheeler
2023/02/14 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Mario Carneiro
2023/02/14 Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Cris Perdue
2023/02/14 [Metamath] Re: Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) Jon P
2023/02/13 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/02/13 [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML tools, esp Generative Pre-trained Transformers (GPTs) David A. Wheeler
2023/02/13 Re: [Metamath] Hardened us.metamath.org David A. Wheeler
2023/02/12 Re: [Metamath] Hardened us.metamath.org Mázsa Péter
2023/02/12 Re: [Metamath] Hardened us.metamath.org Jim Kingdon
2023/02/12 [Metamath] Hardened us.metamath.org David A. Wheeler
2023/02/12 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant Glauco
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/02/11 Re: [Metamath] Thanks for being a vibrant & active community Jim Kingdon
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant Jim Kingdon
2023/02/11 [Metamath] Thanks for being a vibrant & active community David A. Wheeler
2023/02/11 [Metamath] us.metamath.org now has CORS headers, so web client-side applications can access its public data David A. Wheeler
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant Glauco
2023/02/11 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/02/10 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/02/10 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/02/04 Re: [Metamath] status of nnne0ALT Benoit
2023/02/04 [Metamath] Re: Performance of the GPT-enhanced automatic provers by sections Jon P
2023/02/04 Re: [Metamath] status of nnne0ALT Benoit
2023/02/01 Re: [Metamath] status of nnne0ALT heiphohmia via Metamath
2023/02/01 Re: [Metamath] status of nnne0ALT Mario Carneiro
2023/02/01 [Metamath] status of nnne0ALT Zheng Fan
2023/01/25 Re: [Metamath] Trouble running mmj2 M Malik
2023/01/25 Re: [Metamath] Trouble running mmj2 M Malik
2023/01/25 Re: [Metamath] Trouble running mmj2 Glauco
2023/01/25 Re: [Metamath] Trouble running mmj2 David A. Wheeler
2023/01/25 Re: [Metamath] Trouble running mmj2 M Malik
2023/01/24 Re: [Metamath] Trouble running mmj2 M Malik
2023/01/24 [Metamath] Performance of the GPT-enhanced automatic provers by sections Zheng Fan
2023/01/23 Re: [Metamath] Trouble running mmj2 Jim Kingdon
2023/01/23 [Metamath] Trouble running mmj2 M Malik
2023/01/23 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/21 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2023/01/18 Re: [Metamath] Euclidean spaces as free left modules? Thierry Arnoux
2023/01/17 [Metamath] Euclidean spaces as free left modules? 'Alexander van der Vekens' via Metamath
2023/01/13 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/12 Re: [Metamath] Web-based mmj2-like proof assistant Thierry Arnoux
2023/01/12 Re: [Metamath] Web-based mmj2-like proof assistant Thierry Arnoux
2023/01/12 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/12 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/01/11 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/11 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/11 Re: [Metamath] Web-based mmj2-like proof assistant Thierry Arnoux
2023/01/10 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/01/10 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/09 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/01/09 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Glauco
2023/01/08 Re: [Metamath] FYI: Google Lens works really well with Schwabhauser Jim Kingdon
2023/01/08 [Metamath] FYI: Google Lens works really well with Schwabhauser David A. Wheeler
2023/01/08 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2023/01/08 Re: [Metamath] Is MPE really *just* first order? Jim Kingdon
2023/01/08 Re: [Metamath] Web-based mmj2-like proof assistant Thierry Arnoux
2023/01/08 Re: [Metamath] Re: Why does this verify? Thierry Arnoux
2023/01/08 Re: [Metamath] Is MPE really *just* first order? 'Alexander van der Vekens' via Metamath
2023/01/06 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/05 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/05 Re: [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/05 [Metamath] Re: Web-based mmj2-like proof assistant Glauco
2023/01/05 Re: [Metamath] Web-based mmj2-like proof assistant David A. Wheeler
2023/01/05 Re: [Metamath] Web-based mmj2-like proof assistant Antony Bartlett
2023/01/04 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2023/01/03 [Metamath] Web-based mmj2-like proof assistant Igor Ieskov
2023/01/03 Re: [Metamath] Should eliminate the GIF directories & just use Unicode? David A. Wheeler
2023/01/02 Re: [Metamath] Re: Should eliminate the GIF directories & just use Unicode? Mario Carneiro
2023/01/02 Re: [Metamath] Re: Should eliminate the GIF directories & just use Unicode? Jim Kingdon
2023/01/02 Re: [Metamath] Should eliminate the GIF directories & just use Unicode? Mario Carneiro
2023/01/02 Re: [Metamath] Should eliminate the GIF directories & just use Unicode? David A. Wheeler
2023/01/02 [Metamath] Re: Should eliminate the GIF directories & just use Unicode? Benoit
2023/01/02 [Metamath] Re: Should eliminate the GIF directories & just use Unicode? Glauco
2023/01/02 [Metamath] Re: Should eliminate the GIF directories & just use Unicode? Samiro Discher
2023/01/02 [Metamath] Should eliminate the GIF directories & just use Unicode? David A. Wheeler
2022/12/30 Re: [Metamath] Re: Why does this verify? Glauco
2022/12/30 Re: [Metamath] Re: Why does this verify? Shelby Doolittle
2022/12/29 Re: [Metamath] Re: Why does this verify? Mario Carneiro
2022/12/29 [Metamath] Re: Why does this verify? Mario Carneiro
2022/12/29 [Metamath] Why does this verify? Shelby Doolittle
2022/12/26 Re: [Metamath] Yamma Antony Bartlett
2022/12/25 Re: [Metamath] Yamma Glauco
2022/12/25 Re: [Metamath] Yamma Antony Bartlett
2022/12/25 Re: [Metamath] Yamma Glauco
2022/12/25 Re: [Metamath] Yamma Antony Bartlett
2022/12/24 Re: [Metamath] Yamma David A. Wheeler
2022/12/23 [Metamath] Re: Yamma Glauco
2022/12/23 [Metamath] Yamma Antony Bartlett
2022/12/22 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Glauco
2022/12/22 Re: [Metamath] miniF2F database Kunhao Zheng
2022/12/22 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2022/12/21 Re: [Metamath] miniF2F database Kunhao Zheng
2022/12/21 Re: [Metamath] Uncomfortable with definitions as axioms ... help? Mario Carneiro
2022/12/21 [Metamath] Uncomfortable with definitions as axioms ... help? Samuel Goto
2022/12/21 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Samuel Goto
2022/12/21 Re: [Metamath] miniF2F database Johnathan Mercer
2022/12/21 Re: [Metamath] miniF2F database Mario Carneiro
2022/12/21 [Metamath] miniF2F database Zheng Fan
2022/12/19 [Metamath] website problem with symbols download Jim Kingdon
2022/12/19 [Metamath] Command line tools in Docker Antony Bartlett
2022/12/14 [Metamath] Re: Directed Graph Theory 'Alexander van der Vekens' via Metamath
2022/12/11 Re: [Metamath] Re: My contribution to Metamath's mmsolitaire project Jim Kingdon
2022/12/11 [Metamath] Re: My contribution to Metamath's mmsolitaire project Samiro Discher
2022/12/10 [Metamath] Directed Graph Theory Simon Dold
2022/12/10 Re: [Metamath] Alternative Proofs Antony Bartlett
2022/12/07 [Metamath] feature to print html with show trace? Stefan Allan
2022/12/05 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Glauco
2022/12/05 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2022/12/04 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Glauco
2022/12/04 Re: [Metamath] Alternative Proofs Glauco
2022/12/04 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2022/12/04 Re: [Metamath] Alternative Proofs 'Alexander van der Vekens' via Metamath
2022/12/03 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer sgoto
2022/12/03 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer sgoto
2022/12/03 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2022/12/02 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer sgoto
2022/11/29 Re: [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Antony Bartlett
2022/11/29 [Metamath] Yet another independent-ish client-side JS parser, verifier and explorer Samuel Goto
2022/11/25 [Metamath] Re: Strange behaviour of Metamath Benoit
2022/11/24 [Metamath] Re: Strange behaviour of Metamath Gino Giotto
2022/11/23 Re: [Metamath] Having trouble understanding (sqrt2irr) Gonzalo Polavieja
2022/11/23 [Metamath] Re: Strange behaviour of Metamath Benoit
2022/11/23 Re: [Metamath] Having trouble understanding (sqrt2irr) David A. Wheeler
2022/11/23 [Metamath] Strange behaviour of Metamath Gino Giotto
2022/11/23 [Metamath] Re: pull request review Benoit
2022/11/23 [Metamath] pull request review Jim Kingdon
2022/11/22 Re: [Metamath] Having trouble understanding (sqrt2irr) Mázsa Péter
2022/11/22 Re: [Metamath] Having trouble understanding (sqrt2irr) Mario Carneiro
2022/11/22 Re: [Metamath] Having trouble understanding (sqrt2irr) David A. Wheeler
2022/11/22 Re: [Metamath] Having trouble understanding (sqrt2irr) Mario Carneiro
2022/11/22 Re: [Metamath] Having trouble understanding (sqrt2irr) David A. Wheeler
2022/11/21 Re: [Metamath] Having trouble understanding (sqrt2irr) Mario Carneiro
2022/11/21 Re: [Metamath] Having trouble understanding (sqrt2irr) M Malik
2022/11/20 Re: [Metamath] Having trouble understanding (sqrt2irr) Mario Carneiro
2022/11/20 [Metamath] Having trouble understanding (sqrt2irr) M Malik
2022/11/20 Re: [Metamath] Bugs in Metamath Gino Giotto
2022/11/19 Re: [Metamath] Bugs in Metamath Mario Carneiro
2022/11/19 Re: [Metamath] Bugs in Metamath Mario Carneiro
2022/11/19 Re: [Metamath] Bugs in Metamath Gino Giotto
2022/11/19 Re: [Metamath] Bugs in Metamath Mario Carneiro
2022/11/19 [Metamath] Bugs in Metamath Gino Giotto
2022/11/14 Re: [Metamath] Buiding on metamath-knife Jim Kingdon
2022/11/14 Re: [Metamath] Buiding on metamath-knife Mario Carneiro
2022/11/14 Re: [Metamath] Buiding on metamath-knife Zheng Fan
2022/11/13 Re: [Metamath] Buiding on metamath-knife Mario Carneiro
2022/11/13 Re: [Metamath] Buiding on metamath-knife Zheng Fan
2022/11/12 Re: [Metamath] Buiding on metamath-knife Mario Carneiro
2022/11/12 Re: [Metamath] Buiding on metamath-knife Zheng Fan