metamath

Messages by Date

2020/07/14 Re: [Metamath] Introduction to Sophize Abhishek Chugh
2020/07/13 [Metamath] Reminder: We'd love to see more Metamath 100 proofs David A. Wheeler
2020/07/13 Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
2020/07/13 Re: [Metamath] Re: Canonical location for Metamath databases Norman Megill
2020/07/13 Re: [Metamath] Introduction to Sophize Jim Kingdon
2020/07/13 [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') Norman Megill
2020/07/13 [Metamath] Introduction to Sophize Abhishek Chugh
2020/07/13 [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'Alexander van der Vekens' via Metamath
2020/07/13 Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'ookami' via Metamath
2020/07/13 Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'Stanislas Polu' via Metamath
2020/07/12 Re: [Metamath] Re: Canonical location for Metamath databases Giovanni Mascellani
2020/07/12 Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
2020/07/12 [Metamath] Responding to David A. Wheeler 'ookami' via Metamath
2020/07/12 Re: [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
2020/07/12 [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'fl' via Metamath
2020/07/12 [Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A') 'ookami' via Metamath
2020/07/12 [Metamath] Proposal: Allow primed class variables in set.mm body (e.g., A') David A. Wheeler
2020/07/12 [Metamath] Re: Canonical location for Metamath databases Norman Megill
2020/07/12 Re: [Metamath] Canonical location for Metamath databases Giovanni Mascellani
2020/07/12 Re: [Metamath] Canonical location for Metamath databases David A. Wheeler
2020/07/12 [Metamath] Canonical location for Metamath databases Giovanni Mascellani
2020/07/12 [Metamath] Re: A disproof of LNC? Joseph V
2020/07/12 [Metamath] A disproof of LNC? Joseph V
2020/07/11 Re: [Metamath] Frege's Begriffsschrift Norman Megill
2020/07/11 Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
2020/07/10 Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
2020/07/10 Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Alexander van der Vekens' via Metamath
2020/07/10 Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
2020/07/09 Re: [Metamath] Frege's Begriffsschrift Richard Penner
2020/07/08 Re: [Metamath] OpenAI search tool for set.mm theorems 'Stanislas Polu' via Metamath
2020/07/08 Re: [Metamath] OpenAI search tool for set.mm theorems Mario Carneiro
2020/07/08 [Metamath] OpenAI search tool for set.mm theorems Auguste Poiroux
2020/07/07 Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
2020/07/07 [Metamath] Re: More proof shortenings from OpenAI's models Norman Megill
2020/07/06 Re: [Metamath] Re: More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
2020/07/06 [Metamath] Re: More proof shortenings from OpenAI's models 'Alexander van der Vekens' via Metamath
2020/07/04 Re: [Metamath] Perhaps we should create some unshortened "simple examples" David A. Wheeler
2020/07/04 Re: [Metamath] Perhaps we should create some unshortened "simple examples" 'Stanislas Polu' via Metamath
2020/07/04 Re: [Metamath] More proof shortenings from OpenAI's models 'Stanislas Polu' via Metamath
2020/07/04 Re: [Metamath] More proof shortenings from OpenAI's models Glauco
2020/07/04 Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
2020/07/04 Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
2020/07/04 Re: [Metamath] Frege's Begriffsschrift 'fl' via Metamath
2020/07/04 Re: [Metamath] More proof shortenings from OpenAI's models 'ookami' via Metamath
2020/07/03 [Metamath] Perhaps we should create some unshortened "simple examples" David A. Wheeler
2020/07/03 Re: [Metamath] Frege's Begriffsschrift David A. Wheeler
2020/07/03 [Metamath] Historical works 'fl' via Metamath
2020/07/03 Re: [Metamath] More proof shortenings from OpenAI's models David A. Wheeler
2020/07/03 [Metamath] Frege's Begriffsschrift 'fl' via Metamath
2020/07/03 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
2020/07/02 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
2020/07/02 Re: [Metamath] OpenAI Proof Assistant for Metamath David A. Wheeler
2020/07/02 Re: [Metamath] OpenAI Proof Assistant for Metamath David Starner
2020/07/02 Re: [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
2020/07/02 Re: [Metamath] OpenAI Proof Assistant for Metamath David A. Wheeler
2020/07/02 [Metamath] OpenAI Proof Assistant for Metamath 'Stanislas Polu' via Metamath
2020/06/24 Re: [Metamath] Metamath C OlivierBinda
2020/06/24 [Metamath] trying to construct cuberoot of 2 Dirk-Anton Broersen
2020/06/24 Re: [Metamath] Metamath C Giovanni Mascellani
2020/06/23 [Metamath] MM0 -> MM translation challenges Mario Carneiro
2020/06/23 Re: [Metamath] Re: Typo in comment to ~ caov? heiphohmia via Metamath
2020/06/23 Re: [Metamath] Re: Typo in comment to ~ caov? Antony Bartlett
2020/06/23 Re: [Metamath] Re: Typo in comment to ~ caov? 'Alexander van der Vekens' via Metamath
2020/06/22 Re: [Metamath] Re: Typo in comment to ~ caov? heiphohmia via Metamath
2020/06/22 [Metamath] Re: Typo in comment to ~ caov? 'Alexander van der Vekens' via Metamath
2020/06/22 [Metamath] Typo in comment to ~ caov? heiphohmia via Metamath
2020/06/20 [Metamath] Metamath C Mario Carneiro
2020/06/06 Re: [Metamath] Proofs by enumerating cases 'Stanislas Polu' via Metamath
2020/06/06 Re: [Metamath] Proofs by enumerating cases Mario Carneiro
2020/06/06 [Metamath] Proofs by enumerating cases 'Stanislas Polu' via Metamath
2020/05/30 Re: [Metamath] (FL) Re: Proposal: Change mmj2's CLI David A. Wheeler
2020/05/24 [Metamath] Re: (FL) tensor algebra 'Alexander van der Vekens' via Metamath
2020/05/23 [Metamath] Re: (FL) tensor algebra Norman Megill
2020/05/22 [Metamath] Re: (FL) tensor algebra 'Alexander van der Vekens' via Metamath
2020/05/22 Re: [Metamath] (FL) tensor algebra Jim Kingdon
2020/05/22 [Metamath] (FL) tensor algebra Norman Megill
2020/05/16 [Metamath] (FL) Re: Proposal: Change mmj2's CLI Norman Megill
2020/05/15 Re: [Metamath] (FL) Re: Proposal: Change mmj2's CLI David A. Wheeler
2020/05/15 Re: [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI heiphohmia via Metamath
2020/05/14 [Metamath] (FL) Re: Proposal: Change mmj2's CLI Norman Megill
2020/05/13 [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI Norman Megill
2020/05/13 Re: [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI André L F S Bacci
2020/05/13 [Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI Benoit
2020/05/12 [Metamath] (FL) Re: Proposal: Change mmj2's CLI Norman Megill
2020/05/11 Re: [Metamath] Proposal: Change mmj2's CLI Mario Carneiro
2020/05/11 Re: [Metamath] Proposal: Change mmj2's CLI Jim Kingdon
2020/05/11 [Metamath] Proposal: Change mmj2's CLI David A. Wheeler
2020/05/11 [Metamath] (FL) Words, Commons and binomial Norman Megill
2020/05/10 Re: [Metamath] Trisecting an angle Dirk-Anton Broersen
2020/05/10 Re: [Metamath] Trisecting an angle Jim Kingdon
2020/05/10 [Metamath] Trisecting an angle Dirk-Anton Broersen
2020/05/07 Re: [Metamath] Proposed installation conventions so things will be easier to install (FL) David A. Wheeler
2020/05/07 Re: [Metamath] Proposed installation conventions so things will be easier to install David Starner
2020/05/07 Re: [Metamath] Proposed installation conventions so things will be easier to install Giovanni Mascellani
2020/05/07 Re: [Metamath] Proposed installation conventions so things will be easier to install (FL) Giovanni Mascellani
2020/05/07 Re: [Metamath] Proposed installation conventions so things will be easier to install (FL) Norman Megill
2020/05/06 Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
2020/05/06 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/06 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/06 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/06 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/06 Re: [Metamath] Proposed installation conventions so things will be easier to install 'B. Wilson' via Metamath
2020/05/05 [Metamath] Updated Gource visualization now public! David A. Wheeler
2020/05/05 Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
2020/05/05 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/05 Re: [Metamath] Proposed installation conventions so things will be easier to install David Starner
2020/05/05 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/05 Re: [Metamath] Re: Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/05 Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
2020/05/05 [Metamath] Re: Calculational rendering of Metamath proofs, using Greasemonkey/Firefox Marnix Klooster
2020/05/04 [Metamath] Re: Proposed installation conventions so things will be easier to install savask
2020/05/04 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/04 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/04 Re: [Metamath] Proposed installation conventions so things will be easier to install 'B. Wilson' via Metamath
2020/05/04 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/04 Re: [Metamath] Proposed installation conventions so things will be easier to install Norman Megill
2020/05/03 Re: [Metamath] Proposed installation conventions so things will be easier to install Jim Kingdon
2020/05/03 Re: [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/02 [Metamath] Final (?) draft Gource visualization of set.mm David A. Wheeler
2020/05/02 [Metamath] Proposed installation conventions so things will be easier to install David A. Wheeler
2020/05/02 [Metamath] Re: Moving equality across an implication 'Alexander van der Vekens' via Metamath
2020/05/02 [Metamath] Moving equality across an implication David Starner
2020/05/02 [Metamath] Re: The conditional operator for propositions (now with a reference) 'Alexander van der Vekens' via Metamath
2020/05/01 [Metamath] The conditional operator for propositions (now with a reference) Benoit
2020/05/01 [Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell Norman Megill
2020/05/01 [Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell Norman Megill
2020/05/01 Re: [Metamath] Last-minute comments on updated Gource visualization? David A. Wheeler
2020/05/01 [Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell Benoit
2020/05/01 Re: [Metamath] Last-minute comments on updated Gource visualization? Benoit
2020/04/30 [Metamath] Best 2012 date for Eric Schmidt's paper "Reductions in Norman Megill’s axiom system for complex numbers"? David A. Wheeler
2020/04/30 Re: [Metamath] Last-minute comments on updated Gource visualization? David A. Wheeler
2020/04/30 Re: [Metamath] Formalizing IMO B2.1972 'Stanislas Polu' via Metamath
2020/04/30 Re: [Metamath] Formalizing IMO B2.1972 Marnix Klooster
2020/04/29 [Metamath] Last-minute comments on updated Gource visualization? David A. Wheeler
2020/04/29 [Metamath] FL: Nicod, Sheffer Whitehead and Russell Norman Megill
2020/04/28 Re: [Metamath] Packaging Metamath for Linux distros heiphohmia via Metamath
2020/04/28 Re: [Metamath] Packaging Metamath for Linux distros Norman Megill
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Jim Kingdon
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
2020/04/27 Re: [Metamath] Packaging Metamath for Linux distros David A. Wheeler
2020/04/27 Re: [Metamath] Packaging Metamath for Linux distros heiphohmia via Metamath
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Benoit
2020/04/27 Re: [Metamath] Packaging Metamath for Linux distros David A. Wheeler
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/27 Re: [Metamath] Packaging Metamath for Linux distros Norman Megill
2020/04/27 Re: [Metamath] Packaging Metamath for Linux distros Norman Megill
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/27 [Metamath] us2.metmath.org Norman Megill
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives heiphohmia via Metamath
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Thierry Arnoux
2020/04/27 Re: [Metamath] Re: FL: ++; binary connectives Benoit
2020/04/27 Re: [Metamath] Packaging Metamath for Linux distros heiphohmia via Metamath
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives heiphohmia via Metamath
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Thierry Arnoux
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Thierry Arnoux
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives heiphohmia via Metamath
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/26 Re: [Metamath] Re: FL: ++; binary connectives Benoit
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives 'Alexander van der Vekens' via Metamath
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Jim Kingdon
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Benoit
2020/04/25 [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Jim Kingdon
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives Benoit
2020/04/25 Re: [Metamath] Re: Suggestions on recovering aacllem? David A. Wheeler
2020/04/25 [Metamath] Re: Suggestions on recovering aacllem? 'Alexander van der Vekens' via Metamath
2020/04/25 Re: [Metamath] Re: FL: ++; binary connectives 'Alexander van der Vekens' via Metamath
2020/04/25 [Metamath] Re: Suggestions on recovering aacllem? 'Alexander van der Vekens' via Metamath
2020/04/24 [Metamath] Suggestions on recovering aacllem? David A. Wheeler
2020/04/24 Re: [Metamath] Re: Proven: e is transcendental, Metamath 100 #67, by Glauco David A. Wheeler
2020/04/24 Re: [Metamath] Re: FL: ++; binary connectives David A. Wheeler
2020/04/24 Re: [Metamath] Re: FL: ++; binary connectives Mario Carneiro
2020/04/24 [Metamath] Re: FL: ++; binary connectives Norman Megill
2020/04/24 Re: [Metamath] FL: ++; binary connectives Mario Carneiro
2020/04/24 [Metamath] FL: ++; binary connectives Norman Megill
2020/04/24 [Metamath] Re: bj-df-if and df-ifp Benoit
2020/04/23 [Metamath] Re: bj-df-if and df-ifp Richard Penner
2020/04/22 [Metamath] Re: bj-df-if and df-ifp Benoit
2020/04/21 [Metamath] bj-df-if and df-ifp Richard Penner
2020/04/20 Re: [Metamath] Re: Denoting morphisms in set.mm Benoit
2020/04/19 Re: [Metamath] Re: Denoting morphisms in set.mm Mario Carneiro
2020/04/19 [Metamath] Re: Denoting morphisms in set.mm 'Alexander van der Vekens' via Metamath
2020/04/19 [Metamath] Re: Denoting morphisms in set.mm 'Alexander van der Vekens' via Metamath
2020/04/19 [Metamath] Re: mmj2 users on Windows processing set.mm: May need to increase memory 'Alexander van der Vekens' via Metamath
2020/04/18 Re: [Metamath] Re: Denoting morphisms in set.mm Norman Megill