metamath  

Messages by Thread

• • Re: [Metamath] Re: Denoting morphisms in set.mm David Starner
  • Re: [Metamath] Re: Denoting morphisms in set.mm Norman Megill
  • [Metamath] Re: Denoting morphisms in set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Denoting morphisms in set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Denoting morphisms in set.mm Mario Carneiro
  • Re: [Metamath] Re: Denoting morphisms in set.mm Benoit
• [Metamath] Stacking symbols in html / unicode Benoit
  • Re: [Metamath] Stacking symbols in html / unicode André L F S Bacci
  • Re: [Metamath] Stacking symbols in html / unicode André L F S Bacci
  • Re: [Metamath] Stacking symbols in html / unicode Norman Megill
  • Re: [Metamath] Stacking symbols in html / unicode Benoit
  • Re: [Metamath] Stacking symbols in html / unicode Norman Megill
  • Re: [Metamath] Stacking symbols in html / unicode Jens-Wolfhard Schicke-Uffmann
  • Re: [Metamath] Stacking symbols in html / unicode Jon P
  • Re: [Metamath] Stacking symbols in html / unicode Benoit
  • Re: [Metamath] Stacking symbols in html / unicode David A. Wheeler
  • Re: [Metamath] Stacking symbols in html / unicode Jim Kingdon
  • Re: [Metamath] Stacking symbols in html / unicode David A. Wheeler
• [Metamath] How can I find the dependencies at the Table of Contents level? Anarcocap-socdem
  • Re: [Metamath] How can I find the dependencies at the Table of Contents level? Mario Carneiro
  • Re: [Metamath] How can I find the dependencies at the Table of Contents level? Thierry Arnoux
  • Re: [Metamath] How can I find the dependencies at the Table of Contents level? Thierry Arnoux
• Re: [Metamath] Re: George Hotz, a 5+ hours video complaining about Metamath, with 14000+ views and 163 thumb up Thierry Arnoux
• [Metamath] Metamath contributions and COVID-19? David A. Wheeler
  • Re: [Metamath] Metamath contributions and COVID-19? Jim Kingdon
  • [Metamath] Re: Metamath contributions and COVID-19? 'Alexander van der Vekens' via Metamath
• [Metamath] Any other major Metamath/set.mm events? David A. Wheeler
  • [Metamath] Re: Any other major Metamath/set.mm events? savask
  • Re: [Metamath] Re: Any other major Metamath/set.mm events? David A. Wheeler
• [Metamath] Images wanted for contributors (for Gource) David A. Wheeler
  • Re: [Metamath] Images wanted for contributors (for Gource) 'Stanislas Polu' via Metamath
  • Re: [Metamath] Images wanted for contributors (for Gource) Jon P
• [Metamath] Fwd: AI and lemmas Norman Megill
  • Re: [Metamath] Fwd: AI and lemmas 'Stanislas Polu' via Metamath
• [Metamath] Proven: e is transcendental, Metamath 100 #67, by Glauco David A. Wheeler
  • [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco Thomas Brendan Leahy
  • [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco savask
  • [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco savask
  • Re: [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco David A. Wheeler
  • [Metamath] Suggestions on recovering aacllem? David A. Wheeler
  • [Metamath] Re: Suggestions on recovering aacllem? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Suggestions on recovering aacllem? 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Suggestions on recovering aacllem? David A. Wheeler
• [Metamath] Could CLAIM be added to the keywords for bibliographic cross-reference ? Glauco
  • [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Norman Megill
  • [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Glauco
  • Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? David A. Wheeler
  • Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Norman Megill
  • Re: [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? Thierry Arnoux
  • [Metamath] Re: Could CLAIM be added to the keywords for bibliographic cross-reference ? 'Alexander van der Vekens' via Metamath
• [Metamath] Metamath as a medical tool José Manuel Rodríguez Caballero
  • Re: [Metamath] Metamath as a medical tool Mario Carneiro
  • Re: [Metamath] Metamath as a medical tool David A. Wheeler
  • Re: [Metamath] Metamath as a medical tool José Manuel Rodríguez Caballero
  • Re: [Metamath] Metamath as a medical tool Mario Carneiro
  • Re: [Metamath] Metamath as a medical tool David A. Wheeler
  • Re: [Metamath] Metamath as a medical tool José Manuel Rodríguez Caballero
• [Metamath] Travis (Continuous Integration) results not showing on GitHub David A. Wheeler
  • Re: [Metamath] Travis (Continuous Integration) results not showing on GitHub David A. Wheeler
• [Metamath] Why would proof shortening be useful? Marnix Klooster
  • [Metamath] Re: Why would proof shortening be useful? Norman Megill
  • [Metamath] Re: Why would proof shortening be useful? Richard Penner
  • Re: [Metamath] Re: Why would proof shortening be useful? Mario Carneiro
  • Re: [Metamath] Re: Why would proof shortening be useful? Benoit
  • RE: [Metamath] Why would proof shortening be useful? Dirk-Anton Broersen
  • [Metamath] Re: Why would proof shortening be useful? 'ookami' via Metamath
• [Metamath] Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • [Metamath] Re: Deep Learning powered proof shortening Benoit
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • RE: [Metamath] Re: Deep Learning powered proof shortening Dirk-Anton Broersen
  • Re: [Metamath] Re: Deep Learning powered proof shortening Benoit
  • RE: [Metamath] Re: Deep Learning powered proof shortening Dirk-Anton Broersen
  • Re: [Metamath] Re: Deep Learning powered proof shortening Benoit
  • Re: [Metamath] Re: Deep Learning powered proof shortening Benoit
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening Norman Megill
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening savask
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening savask
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening savask
  • Re: [Metamath] Re: Deep Learning powered proof shortening Jim Kingdon
  • Re: [Metamath] Re: Deep Learning powered proof shortening Jon P
  • Re: [Metamath] Deep Learning powered proof shortening OlivierBinda
  • Re: [Metamath] Deep Learning powered proof shortening Jim Kingdon
  • [Metamath] Re: Deep Learning powered proof shortening 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening David A. Wheeler
  • Re: [Metamath] Re: Deep Learning powered proof shortening Thierry Arnoux
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening David A. Wheeler
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Deep Learning powered proof shortening 'Stanislas Polu' via Metamath
• [Metamath] Re: Prime numbers in Triangular intervals Thierry Arnoux
  • [Metamath] RE: Prime numbers in Triangular intervals Dirk-Anton Broersen
• [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 'Stanislas Polu' via Metamath
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 'Stanislas Polu' via Metamath
  • Re: [Metamath] Problem launching mmj2 Mario Carneiro
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 Mario Carneiro
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 Mario Carneiro
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 Mario Carneiro
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 Mario Carneiro
  • Re: [Metamath] Problem launching mmj2 Benoit
  • Re: [Metamath] Problem launching mmj2 Benoit
• [Metamath] Re: [Agda] [Coq-Club] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory? Ken Kubota
• [Metamath] e. in the context of fol or sol + Peano Norman Megill
  • Re: [Metamath] e. in the context of fol or sol + Peano Thierry Arnoux
  • [Metamath] Re: e. in the context of fol or sol + Peano Norman Megill
  • [Metamath] Re: e. in the context of fol or sol + Peano Sine Flexione
• [Metamath] A frozen FOL 'fl' via Metamath
• [Metamath] Second-order theory 'fl' via Metamath
  • Re: [Metamath] Second-order theory Ken Kubota
  • Re: [Metamath] Second-order theory Mario Carneiro
  • Re: [Metamath] Second-order theory Ken Kubota
  • Re: [Metamath] Second-order theory Norman Megill
  • Re: [Metamath] Second-order theory Ken Kubota
  • Re: [Metamath] Second-order theory Mario Carneiro
  • Re: [Metamath] Second-order theory Ken Kubota
  • Re: [Metamath] Second-order theory Mario Carneiro
• [Metamath] Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Ken Kubota
  • [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Mario Carneiro
  • Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Mario Carneiro
  • Re: [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • [Metamath] Re: Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? 'fl' via Metamath
  • Re: [Metamath] Type Theory vs. Set Theory – Re: [Coq-Club] [Agda] Why dependent type theory? Ken Kubota
  • [Metamath] Concepts within Type Theory – Re: [Coq-Club] [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory? Ken Kubota
  • [Metamath] Re: [Coq-Club] Concepts within Type Theory – Re: [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory? Ken Kubota
• [Metamath] reinterpret ax-3 'ookami' via Metamath
  • Re: [Metamath] reinterpret ax-3 Mario Carneiro
  • Re: [Metamath] reinterpret ax-3 'ookami' via Metamath
  • Re: [Metamath] reinterpret ax-3 Benoit
  • Re: [Metamath] reinterpret ax-3 Mario Carneiro
  • Re: [Metamath] reinterpret ax-3 Mario Carneiro
  • Re: [Metamath] reinterpret ax-3 Benoit
  • Re: [Metamath] reinterpret ax-3 Mario Carneiro
  • Re: [Metamath] reinterpret ax-3 Benoit
• [Metamath] If the humanity disappears (3) 'fl' via Metamath
• [Metamath] If the humanity disappears (2) 'fl' via Metamath
  • [Metamath] Re: If the humanity disappears (2) vvs
• Re: [Metamath] Re: Deprecated sections of set.mm Jon P
  • Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
  • Re: [Metamath] Re: Deprecated sections of set.mm Jon P
  • Re: [Metamath] Re: Deprecated sections of set.mm Mario Carneiro
  • Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
  • Re: [Metamath] Re: Deprecated sections of set.mm Jon P
  • Re: [Metamath] Re: Deprecated sections of set.mm 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
  • Re: [Metamath] Re: Deprecated sections of set.mm Norman Megill
• Re: [Metamath] Re: Formalizing IMO B2.1972 heiphohmia via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Jon P
• [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • [Metamath] Re: Formalizing IMO B2.1972 Benoit
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Benoit
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Thierry Arnoux
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Benoit
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Benoit
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Benoit
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Jon P
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Mario Carneiro
  • NN vs. NN0 again Was: Re: [Metamath] Re: Formalizing IMO B2.1972 Norman Megill
  • Re: NN vs. NN0 again Was: Re: [Metamath] Re: Formalizing IMO B2.1972 'fl' via Metamath
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Jim Kingdon
  • Re: [Metamath] Re: Formalizing IMO B2.1972 Thierry Arnoux
  • Re: [Metamath] Re: Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
  • Re: [Metamath] Formalizing IMO B2.1972 Jim Kingdon
  • [Metamath] Re: Formalizing IMO B2.1972 Jon P

• Earlier messages
• Later messages