metamath

Messages by Date

2020/04/18 Re: [Metamath] Re: Denoting morphisms in set.mm Norman Megill
2020/04/18 [Metamath] Re: Can a floating hypothesis become essential? Norman Megill
2020/04/18 [Metamath] mmj2 users on Windows processing set.mm: May need to increase memory David A. Wheeler
2020/04/18 Re: [Metamath] Re: Denoting morphisms in set.mm David Starner
2020/04/18 [Metamath] Re: Can a floating hypothesis become essential? savask
2020/04/18 [Metamath] Re: Denoting morphisms in set.mm Norman Megill
2020/04/18 [Metamath] Re: Can a floating hypothesis become essential? Norman Megill
2020/04/18 [Metamath] Re: Denoting morphisms in set.mm Norman Megill
2020/04/18 [Metamath] Re: New contributions Jon P
2020/04/17 [Metamath] Can a floating hypothesis become essential? savask
2020/04/17 Re: [Metamath] New contributions 'Stanislas Polu' via Metamath
2020/04/16 Re: [Metamath] New contributions Jim Kingdon
2020/04/16 [Metamath] New contributions David Starner
2020/04/16 [Metamath] Denoting morphisms in set.mm Benoit
2020/04/14 Re: [Metamath] Stacking symbols in html / unicode Jim Kingdon
2020/04/14 Re: [Metamath] Stacking symbols in html / unicode David A. Wheeler
2020/04/14 Re: [Metamath] Stacking symbols in html / unicode Benoit
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode Jon P
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode Jens-Wolfhard Schicke-Uffmann
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode David A. Wheeler
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode Norman Megill
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode Benoit
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode Norman Megill
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode André L F S Bacci
2020/04/13 Re: [Metamath] Stacking symbols in html / unicode André L F S Bacci
2020/04/13 Re: [Metamath] How can I find the dependencies at the Table of Contents level? Thierry Arnoux
2020/04/13 Re: [Metamath] How can I find the dependencies at the Table of Contents level? Thierry Arnoux
2020/04/13 [Metamath] Stacking symbols in html / unicode Benoit
2020/04/13 Re: [Metamath] How can I find the dependencies at the Table of Contents level? Mario Carneiro
2020/04/13 [Metamath] How can I find the dependencies at the Table of Contents level? Anarcocap-socdem
2020/04/13 [Metamath] Re: Metamath contributions and COVID-19? 'Alexander van der Vekens' via Metamath
2020/04/12 Re: [Metamath] Metamath contributions and COVID-19? Jim Kingdon
2020/04/12 Re: [Metamath] Re: George Hotz, a 5+ hours video complaining about Metamath, with 14000+ views and 163 thumb up Thierry Arnoux
2020/04/12 Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Thierry Arnoux
2020/04/12 [Metamath] Metamath contributions and COVID-19? David A. Wheeler
2020/04/12 Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Norman Megill
2020/04/12 Re: [Metamath] Re: Any other major Metamath/set.mm events? David A. Wheeler
2020/04/12 [Metamath] Re: Any other major Metamath/set.mm events? savask
2020/04/12 [Metamath] Any other major Metamath/set.mm events? David A. Wheeler
2020/04/11 Re: [Metamath] Images wanted for contributors (for Gource) Jon P
2020/04/11 Re: [Metamath] Images wanted for contributors (for Gource) 'Stanislas Polu' via Metamath
2020/04/11 [Metamath] Images wanted for contributors (for Gource) David A. Wheeler
2020/04/10 [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco savask
2020/04/10 [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco savask
2020/04/10 [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco Thomas Brendan Leahy
2020/04/09 [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? 'Alexander van der Vekens' via Metamath
2020/04/08 Re: [Metamath] Fwd: AI and lemmas 'Stanislas Polu' via Metamath
2020/04/08 [Metamath] Fwd: AI and lemmas Norman Megill
2020/04/07 [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco 'Alexander van der Vekens' via Metamath
2020/04/07 [Metamath] Proven: e is transcendental, Metamath 100 #67, by Glauco David A. Wheeler
2020/04/05 Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? David A. Wheeler
2020/04/05 [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Glauco
2020/04/05 [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Norman Megill
2020/04/05 [Metamath] Could CLAIM be added to the keywords for bibliographic cross-reference ? Glauco
2020/04/04 Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
2020/04/04 Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
2020/04/03 Re: [Metamath] Re: About Metamath zero (mm0) Mario Carneiro
2020/04/03 Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
2020/03/31 Re: [Metamath] Re: Deep Learning powered proof shortening Jim Kingdon
2020/03/31 Re: [Metamath] Re: Deep Learning powered proof shortening Jon P
2020/03/31 Re: [Metamath] Re: Deep Learning powered proof shortening savask
2020/03/31 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/31 Re: [Metamath] Re: Deep Learning powered proof shortening savask
2020/03/31 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/30 Re: [Metamath] Metamath as a medical tool José Manuel Rodríguez Caballero
2020/03/30 Re: [Metamath] Re: Deep Learning powered proof shortening savask
2020/03/30 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/29 Re: [Metamath] Metamath as a medical tool David A. Wheeler
2020/03/29 Re: [Metamath] Metamath as a medical tool Mario Carneiro
2020/03/29 Re: [Metamath] Metamath as a medical tool José Manuel Rodríguez Caballero
2020/03/29 Re: [Metamath] Metamath as a medical tool David A. Wheeler
2020/03/29 Re: [Metamath] Metamath as a medical tool Mario Carneiro
2020/03/29 Re: [Metamath] Re: Riemann-zeta ratio-test rabbit-hole Steve Rodriguez
2020/03/29 [Metamath] Metamath as a medical tool José Manuel Rodríguez Caballero
2020/03/29 [Metamath] Re: Why would proof shortening be useful? 'ookami' via Metamath
2020/03/29 Re: [Metamath] Re: Deep Learning powered proof shortening David A. Wheeler
2020/03/29 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/29 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/29 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/29 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/29 Re: [Metamath] Re: Deep Learning powered proof shortening Thierry Arnoux
2020/03/28 Re: [Metamath] Re: Deep Learning powered proof shortening David A. Wheeler
2020/03/28 Re: [Metamath] Travis (Continuous Integration) results not showing on GitHub David A. Wheeler
2020/03/28 [Metamath] Travis (Continuous Integration) results not showing on GitHub David A. Wheeler
2020/03/28 [Metamath] Re: Deep Learning powered proof shortening 'Alexander van der Vekens' via Metamath
2020/03/28 Re: [Metamath] Re: Deep Learning powered proof shortening Norman Megill
2020/03/28 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/27 Re: [Metamath] Re: Deep Learning powered proof shortening Benoit
2020/03/27 RE: [Metamath] Why would proof shortening be useful? Dirk-Anton Broersen
2020/03/27 Re: [Metamath] Re: Deep Learning powered proof shortening Benoit
2020/03/27 Re: [Metamath] Re: Why would proof shortening be useful? Benoit
2020/03/27 Re: [Metamath] Re: Why would proof shortening be useful? Mario Carneiro
2020/03/27 [Metamath] Re: Why would proof shortening be useful? Richard Penner
2020/03/27 [Metamath] Re: Why would proof shortening be useful? Norman Megill
2020/03/27 [Metamath] Why would proof shortening be useful? Marnix Klooster
2020/03/26 RE: [Metamath] Re: Deep Learning powered proof shortening Dirk-Anton Broersen
2020/03/26 Re: [Metamath] Re: Deep Learning powered proof shortening Benoit
2020/03/26 RE: [Metamath] Re: Deep Learning powered proof shortening Dirk-Anton Broersen
2020/03/26 Re: [Metamath] Deep Learning powered proof shortening Jim Kingdon
2020/03/26 Re: [Metamath] Deep Learning powered proof shortening OlivierBinda
2020/03/26 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/26 Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/26 [Metamath] Re: Deep Learning powered proof shortening Benoit
2020/03/26 [Metamath] Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
2020/03/24 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/24 [Metamath] RE: Prime numbers in Triangular intervals Dirk-Anton Broersen
2020/03/24 [Metamath] Re: Prime numbers in Triangular intervals Thierry Arnoux
2020/03/24 Re: [Metamath] Formalizing IMO B2.1972 Dirk-Anton Broersen
2020/03/24 Re: [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/24 Re: [Metamath] Formalizing IMO B2.1972 Marnix Klooster
2020/03/23 Re: [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/23 Re: [Metamath] Formalizing IMO B2.1972 Marnix Klooster
2020/03/23 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/23 Re: [Metamath] Problem launching mmj2 Mario Carneiro
2020/03/23 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/23 Re: [Metamath] Problem launching mmj2 Mario Carneiro
2020/03/23 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/23 Re: [Metamath] Problem launching mmj2 Mario Carneiro
2020/03/23 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/22 [Metamath] Re: e. in the context of fol or sol + Peano Sine Flexione
2020/03/20 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/18 Re: [Metamath] Problem launching mmj2 Mario Carneiro
2020/03/18 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/18 Re: [Metamath] Problem launching mmj2 Mario Carneiro
2020/03/18 Re: [Metamath] Problem launching mmj2 'Stanislas Polu' via Metamath
2020/03/18 Re: [Metamath] Problem launching mmj2 Benoit
2020/03/17 Re: [Metamath] Problem launching mmj2 'Stanislas Polu' via Metamath
2020/03/17 [Metamath] Problem launching mmj2 Benoit
2020/03/16 Re: [Metamath] Second-order theory Mario Carneiro
2020/03/16 Re: [Metamath] Second-order theory Ken Kubota
2020/03/16 Re: [Metamath] Second-order theory Mario Carneiro
2020/03/16 Re: [Metamath] Second-order theory Ken Kubota
2020/03/16 Re: [Metamath] Second-order theory Norman Megill
2020/03/16 [Metamath] Re: e. in the context of fol or sol + Peano Norman Megill
2020/03/16 [Metamath] Re: [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory? Ken Kubota
2020/03/16 Re: [Metamath] e. in the context of fol or sol + Peano Thierry Arnoux
2020/03/16 Re: [Metamath] Second-order theory Ken Kubota
2020/03/15 [Metamath] e. in the context of fol or sol + Peano Norman Megill
2020/03/14 Re: [Metamath] Second-order theory Mario Carneiro
2020/03/14 [Metamath] Re: [Coq-Club] Concepts within Type Theory – Re: [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory? Ken Kubota
2020/03/14 Re: [Metamath] Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Ken Kubota
2020/03/14 Re: [Metamath] Second-order theory Ken Kubota
2020/03/14 [Metamath] A frozen FOL 'fl' via Metamath
2020/03/14 [Metamath] Second-order theory 'fl' via Metamath
2020/03/13 [Metamath] Concepts within Type Theory – Re: [Coq-Club] [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory? Ken Kubota
2020/03/12 [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/12 [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/12 Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/12 Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
2020/03/12 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/12 Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
2020/03/12 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/11 Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Mario Carneiro
2020/03/11 Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/11 Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/11 Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Mario Carneiro
2020/03/11 [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/10 [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
2020/03/10 Re: [Metamath] reinterpret ax-3 Benoit
2020/03/09 Re: [Metamath] reinterpret ax-3 Mario Carneiro
2020/03/09 Re: [Metamath] reinterpret ax-3 Benoit
2020/03/09 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/09 Re: [Metamath] Re: Formalizing IMO B2.1972 Jon P
2020/03/09 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/09 [Metamath] Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Ken Kubota
2020/03/08 Re: [Metamath] reinterpret ax-3 Mario Carneiro
2020/03/08 Re: [Metamath] reinterpret ax-3 Mario Carneiro
2020/03/08 Re: [Metamath] reinterpret ax-3 Benoit
2020/03/08 Re: [Metamath] reinterpret ax-3 'ookami' via Metamath
2020/03/08 Re: [Metamath] reinterpret ax-3 Mario Carneiro
2020/03/08 [Metamath] reinterpret ax-3 'ookami' via Metamath
2020/03/07 [Metamath] If the humanity disappears (3) 'fl' via Metamath
2020/03/07 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/07 Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
2020/03/07 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/06 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/06 Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
2020/03/06 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/05 Re: [Metamath] Re: Analysis of full 'minimize' run on set.mm Norman Megill
2020/03/05 Re: [Metamath] Re: Analysis of full 'minimize' run on set.mm Norman Megill
2020/03/05 Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
2020/03/05 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/04 Re: NN vs. NN0 again Was: Re: [Metamath] Re: Formalizing IMO B2.1972 'fl' via Metamath
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/04 Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
2020/03/04 NN vs. NN0 again Was: Re: [Metamath] Re: Formalizing IMO B2.1972 Norman Megill
2020/03/04 Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 Benoit
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 Thierry Arnoux
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 Jim Kingdon
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 Benoit
2020/03/04 Re: [Metamath] Re: Deprecated sections of set.mm 'Alexander van der Vekens' via Metamath
2020/03/04 Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/03/04 Re: [Metamath] Re: Deprecated sections of set.mm Jon P
2020/03/02 Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
2020/03/02 Re: [Metamath] Re: About Metamath zero (mm0) Olivier Binda
2020/03/02 Re: [Metamath] Re: Deprecated sections of set.mm Mario Carneiro