Most Recent Proofs - Metamath Proof Explorer

	Metamath Proof Explorer Most Recent Proofs
Mirrors > Home > MPE Home > Th. List > Recent		ILE Most Recent Other > MM 100

Most recent proofs These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 212ee7d9, also available here: set.mm (43MB) or set.mm.bz2 (compressed, 13MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43. The "OLD" versions are usually deleted after a year.

Other links Contact us. Mailing list: Metamath Google Group Updated 7-Dec-2021 . Contributing: How can I contribute to Metamath? Syndication: RSS feed (courtesy of Dan Getz) Related wikis: Ghilbert Google Group.

Recent news items (15-Nov-2025) Thierry Arnoux added a new proof to the 100 theorem list, The Impossibility of Trisecting the Angle and Doubling the Cube, trisecnconstr and 2sqr3nconstr.

(7-Aug-2021) Version 0.198 of the metamath program fixes a bug in "write source ... /rewrap" that prevented end-of-sentence punctuation from appearing in column 79, causing some rewrapped lines to be shorter than necessary. Because this affects about 2000 lines in set.mm, you should use version 0.198 or later for rewrapping before submitting to GitHub.

(7-May-2021) Mario Carneiro has written a Metamath verifier in Lean.

(5-May-2021) Marnix Klooster has written a Metamath verifier in Zig.

(24-Mar-2021) Metamath was mentioned in a couple of articles about OpenAI: Researchers find that large language models struggle with math and What Is GPT-F?.

(26-Dec-2020) Version 0.194 of the metamath program adds the keyword "htmlexturl" to the $t comment to specify external versions of theorem pages. This keyward has been added to set.mm, and you must update your local copy of set.mm for "verify markup" to pass with the new program version.

(19-Dec-2020) Aleksandr A. Adamov has translated the Wikipedia Metamath page into Russian.

(19-Nov-2020) Eric Schmidt's checkmm.cpp was used as a test case for C'est, "a non-standard version of the C++20 standard library, with enhanced support for compile-time evaluation." See C++20 Compile-time Metamath Proof Verification using C'est.

(10-Nov-2020) Filip Cernatescu has updated the XPuzzle (Android app) to version 1.2. XPuzzle is a puzzle with math formulas derived from the Metamath system. At the bottom of the web page is a link to the Google Play Store, where the app can be found.

(7-Nov-2020) Richard Penner created a cross-reference guide between Frege's logic notation and the notation used by set.mm.

(4-Sep-2020) Version 0.192 of the metamath program adds the qualifier '/extract' to 'write source'. See 'help write source' and also this Google Group post.

(23-Aug-2020) Version 0.188 of the metamath program adds keywords Conclusion, Fact, Introduction, Paragraph, Scolia, Scolion, Subsection, and Table to bibliographic references. See 'help write bibliography' for the complete current list.

Older news...

Color key:

Metamath Proof Explorer

Hilbert Space Explorer

User Mathboxes

Last updated on 9-Sep-2026 at 5:30 AM ET.

**Recent Additions to the Metamath Proof Explorer** Notes (last updated 7-Dec-2020 )
Date	Label	Description
Theorem

31-Aug-2026	angmgmbas 29285	The base set of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐽 = (AngMgm‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → (𝐴 / ∼ ) = (Base‘𝐽))

31-Aug-2026	angmgm 29284	The angle addition magma is a magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ 𝐽 = (AngMgm‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 2 ≤ (♯‘𝑃)) ⇒ ⊢ (𝜑 → 𝐽 ∈ Mgm)

31-Aug-2026	angmgm0g 29283	The identity element of the angle addition magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ 𝐽 = (AngMgm‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋})) ⇒ ⊢ (𝜑 → [⟨“𝑋𝑌𝑋”⟩] ∼ = (0_g‘𝐽))

31-Aug-2026	angmgmlem 29282	Lemma for angmgm 29284. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ 𝐽 = (AngMgm‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋})) ⇒ ⊢ (𝜑 → (𝐽 ∈ Mgm ∧ [⟨“𝑋𝑌𝑋”⟩] ∼ = (0_g‘𝐽)))

31-Aug-2026	angmgmval 29281	Explicit the value of the angle addition magma for a given geometry 𝐺. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ 𝐽 = (AngMgm‘𝐺) & ⊢ ≤ = (≤_∠‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐽 = ({⟨(Base‘ndx), 𝐴⟩, ⟨(+_g‘ndx), + ⟩, ⟨(le‘ndx), ≤ ⟩} /_s ∼ ))

31-Aug-2026	angmgmaddrid 29280	The right identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋})) & ⊢ (𝜑 → 𝐸 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐸 + ⟨“𝑋𝑌𝑋”⟩) ∼ 𝐸)

31-Aug-2026	angmgmaddlid 29279	The left identity element for the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ (𝑃 ∖ {𝑋})) & ⊢ (𝜑 → 𝐸 ∈ 𝐴) ⇒ ⊢ (𝜑 → (⟨“𝑋𝑌𝑋”⟩ + 𝐸) ∼ 𝐸)

31-Aug-2026	angmgmaddcl 29278	Closure of the addition of angles. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ (𝜑 → 𝐸 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐸 + 𝐹) ∈ 𝐴)

31-Aug-2026	cgrabasimass 29265	The angle congruence relation is hereditary. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ ∼ = (cgrA‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ( ∼ “ 𝐴) ⊆ 𝐴)

31-Aug-2026	cgraer 29264	The angle congruence relation is an equivalence relation. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ ∼ = (cgrA‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) ⇒ ⊢ (𝜑 → ( ∼ ∩ (𝐴 × 𝐴)) Er 𝐴)

31-Aug-2026	qusmnd 18894	Prove that a quotient structure is a monoid. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ (𝜑 → 𝑈 = (𝑅 /_s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+_g‘𝑅) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) ∼ (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∼ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑥 + 0 ) ∼ 𝑥) ⇒ ⊢ (𝜑 → (𝑈 ∈ Mnd ∧ [ 0 ] ∼ = (0_g‘𝑈)))

31-Aug-2026	qusmgm 18783	Prove that a quotient structure is a unital magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ (𝜑 → 𝑈 = (𝑅 /_s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+_g‘𝑅) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∼ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑥 + 0 ) ∼ 𝑥) ⇒ ⊢ (𝜑 → (𝑈 ∈ Mgm ∧ [ 0 ] ∼ = (0_g‘𝑈)))

31-Aug-2026	imasmgm2 18782	The image structure of a unital magma is a unital magma. (Contributed by Thierry Arnoux, 31-Aug-2026.)
⊢ (𝜑 → 𝑈 = (𝐹 “_s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+_g‘𝑅) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑥 + 0 )) = (𝐹‘𝑥)) ⇒ ⊢ (𝜑 → (𝑈 ∈ Mgm ∧ (𝐹‘ 0 ) = (0_g‘𝑈)))

30-Aug-2026	smflimlem6 47612	Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of [Fremlin1] p. 38 . This lemma proves that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by 𝐷. The proof uses fnrndomnum 10545 rather than fnrndomg 10546, and so does not require ax-ac 10465. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Vincent Gonzalez, 30-Aug-2026.)
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑍 = (ℤ_≥‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) & ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ_≥‘𝑛)dom (𝐹‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)) ∈ dom ⇝ } & ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ 𝑃 = (𝑚 ∈ 𝑍, 𝑘 ∈ ℕ ↦ {𝑠 ∈ 𝑆 ∣ {𝑥 ∈ dom (𝐹‘𝑚) ∣ ((𝐹‘𝑚)‘𝑥) < (𝐴 + (1 / 𝑘))} = (𝑠 ∩ dom (𝐹‘𝑚))}) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐺‘𝑥) ≤ 𝐴} ∈ (𝑆 ↾_t 𝐷))

30-Aug-2026	subsaliuncl 47194	A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. The proof uses fnrndomnum 10545 rather than fnrndomg 10546, and so does not require ax-ac 10465. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Vincent Gonzalez, 30-Aug-2026.)
⊢ (𝜑 → 𝑆 ∈ SAlg) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ 𝑇 = (𝑆 ↾_t 𝐷) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑇) ⇒ ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇)

30-Aug-2026	preimaaa 26562	An element of the preimage of the algebraic numbers by a nonconstant polynomial is an algebraic number. (Contributed by SN, 30-Aug-2026.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘ℚ)) & ⊢ (𝜑 → (deg‘𝐹) ≠ 0) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝔸) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝔸)

30-Aug-2026	plyconz 26547	The composition of a nonzero and a nonconstant polynomial is a nonzero polynomial. (Contributed by SN, 30-Aug-2026.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → 𝐹 ≠ 0_𝑝) & ⊢ (𝜑 → (deg‘𝐺) ≠ 0) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ≠ 0_𝑝)

30-Aug-2026	rnplynfin 26546	The range of a nonconstant polynomial is not a finite set. (Contributed by SN, 30-Aug-2026.)
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) & ⊢ (𝜑 → (deg‘𝐹) ≠ 0) ⇒ ⊢ (𝜑 → ¬ ran 𝐹 ∈ Fin)

30-Aug-2026	idpfv 26442	Value of the identity polynomial. (Contributed by SN, 30-Aug-2026.)
⊢ (𝐴 ∈ ℂ → (X_p‘𝐴) = 𝐴)

30-Aug-2026	1q 13018	The number 1 is rational. (Contributed by SN, 30-Aug-2026.)
⊢ 1 ∈ ℚ

30-Aug-2026	elmaprd 8853	Deduction associated with elmapd 8843. Reverse direction of elmapdd 8844. (Contributed by Thierry Arnoux, 13-Oct-2025.) Removed redundant hypotheses. (Revised by SN, 30-Aug-2026.)
⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑_m 𝐴)) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

28-Aug-2026	dvcot 50699	Derivative of the cotangent function. (Contributed by Jon Pennant, 28-Aug-2026.)
⊢ (ℂ D cot) = (𝑥 ∈ dom cot ↦ -((csc‘𝑥)↑2))

28-Aug-2026	dvcsc 50698	Derivative of the cosecant function. (Contributed by Jon Pennant, 28-Aug-2026.)
⊢ (ℂ D csc) = (𝑥 ∈ dom csc ↦ (-(csc‘𝑥) · (cot‘𝑥)))

28-Aug-2026	dvsec 50697	Derivative of the secant function. (Contributed by Jon Pennant, 28-Aug-2026.)
⊢ (ℂ D sec) = (𝑥 ∈ dom sec ↦ ((sec‘𝑥) · (tan‘𝑥)))

27-Aug-2026	veroquaddetzerod 50827	The Veronese matrix of six points satisfying a common nonzero homogeneous quadratic equation has determinant zero. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) & ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0) & ⊢ (𝜑 → 𝐾 ≠ ((1...6) × {0})) ⇒ ⊢ (𝜑 → (((1...6) maDet ℝ_fld)‘𝑉) = 0)

27-Aug-2026	veroquadnolindfd 50826	A nonzero homogeneous quadratic equation satisfied by all six points gives a linear dependence among the columns of the Veronese matrix. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) & ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0) & ⊢ (𝜑 → 𝐾 ≠ ((1...6) × {0})) ⇒ ⊢ (𝜑 → ¬ curry tpos 𝑉 LIndF (ℝ_fld freeLMod (1...6)))

27-Aug-2026	nellindf 50811	A nonzero coefficient vector whose weighted combination of 𝐹 sums to the zero vector implies that 𝐹 is not linearly independent. (Contributed by Jiamin Zhao, 27-Aug-2026.)
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ · = ( ·_𝑠 ‘𝑊) & ⊢ 0 = (0_g‘𝑊) & ⊢ 𝑌 = (0_g‘𝑅) & ⊢ 𝐿 = (Base‘(𝑅 freeLMod 𝐼)) ⇒ ⊢ (((𝑊 ∈ LMod ∧ 𝐼 ∈ V ∧ 𝐹:𝐼⟶𝐵) ∧ (𝐾 ∈ 𝐿 ∧ 𝐾 ≠ (𝐼 × {𝑌}) ∧ (𝑊 Σ_g (𝐾 ∘_f · 𝐹)) = 0 )) → ¬ 𝐹 LIndF 𝑊)

26-Aug-2026	dffr7 36543	Alternate quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 26-Aug-2026.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ Fix ( E ∘ (V ∖ (𝑅 ∘ ^◡ E ))))

26-Aug-2026	dffr5 36341	A quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 11-Apr-2011.) (Proof shortened by Scott Fenton, 26-Aug-2026.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ^◡𝑅)))

26-Aug-2026	cnvxp 6152	The converse of a Cartesian product. Exercise 11 of [Suppes] p. 67. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-11 2194. (Revised by SN, 26-Aug-2026.)
⊢ ^◡(𝐴 × 𝐵) = (𝐵 × 𝐴)

25-Aug-2026	fimact 10543	The image by a function of a countable set is countable. The proof uses imadomnum 10542 rather than imadomg 10541, and so does not require ax-ac 10465. (Contributed by Thierry Arnoux, 27-Mar-2018.) (Revised by Vincent Gonzalez, 25-Aug-2026.)
⊢ ((𝐴 ≼ ω ∧ Fun 𝐹) → (𝐹 “ 𝐴) ≼ ω)

25-Aug-2026	imadomnum 10542	A version of imadomg 10541 that does not require the axiom of choice ax-ac 10465. (Contributed by Vincent Gonzalez, 25-Aug-2026.)
⊢ (𝐴 ∈ dom card → (Fun 𝐹 → (𝐹 “ 𝐴) ≼ 𝐴))

24-Aug-2026	4p5e9 43148	4 + 5 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (4 + 5) = 9

24-Aug-2026	3p6e9 43147	3 + 6 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 6) = 9

24-Aug-2026	3p5e8 43146	3 + 5 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 5) = 8

24-Aug-2026	3p4e7 43145	3 + 4 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (3 + 4) = 7

24-Aug-2026	2p7e9 43144	2 + 7 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 7) = 9

24-Aug-2026	2p6e8 43143	2 + 6 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 6) = 8

24-Aug-2026	2p5e7 43142	2 + 5 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 5) = 7

24-Aug-2026	2p4e6 43141	2 + 4 = 6. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 4) = 6

24-Aug-2026	2p3e5 43140	2 + 3 = 5. (Contributed by SN, 24-Aug-2026.)
⊢ (2 + 3) = 5

24-Aug-2026	1p8e9 43139	1 + 8 = 9. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 8) = 9

24-Aug-2026	1p7e8 43138	1 + 7 = 8. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 7) = 8

24-Aug-2026	1p6e7 43137	1 + 6 = 7. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 6) = 7

24-Aug-2026	1p5e6 43136	1 + 5 = 6. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 5) = 6

24-Aug-2026	1p4e5 43135	1 + 4 = 5. (Contributed by SN, 24-Aug-2026.)
⊢ (1 + 4) = 5

24-Aug-2026	4p4e8ALT 43133	A shorter proof of 4p4e8 12423 if 6p2e8 12427 was moved up. The most clean way to do this would be to start with 7p2e9 12429, then go 6p2e8 12427, 6p3e9 12428, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12344 is shorter than using 4 = 3 + 1, 3cn 12350, and ax-1cn 11186. This also works with 5p4e9 12426. (Contributed by SN, 24-Aug-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (4 + 4) = 8

24-Aug-2026	ffsrn 33207	The range of a finitely supported function is finite. The proof uses fnrndomnum 10545 rather than fnrndomg 10546, and so does not require ax-ac 10465. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Vincent Gonzalez, 24-Aug-2026.)
⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ Fin)

24-Aug-2026	fnct 10548	If the domain of a function is countable, the function is countable. The proof uses fnrndomnum 10545 rather than fnrndomg 10546, and so does not require ax-ac 10465. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Revised by Vincent Gonzalez, 24-Aug-2026.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ≼ ω) → 𝐹 ≼ ω)

24-Aug-2026	dmct 10530	The domain of a countable set is countable. The proof uses fodomnum 10064 rather than fodomg 10528, and so does not require ax-ac 10465. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Revised by Vincent Gonzalez, 24-Aug-2026.)
⊢ (𝐴 ≼ ω → dom 𝐴 ≼ ω)

23-Aug-2026	angmgmaddcpbl 29277	Addition of angles is compatible with angle congruence. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐸 ∼ 𝐶) & ⊢ (𝜑 → 𝐹 ∼ 𝐷) ⇒ ⊢ (𝜑 → (𝐸 + 𝐹) ∼ (𝐶 + 𝐷))

23-Aug-2026	angmgmaddov2 29276	Value of the addition operation in the angle addition magma, in case the first angle is zero or flat. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍)) & ⊢ (𝜑 → 𝑆 ∈ 𝑃) & ⊢ (𝜑 → ⟨“𝑊𝑉𝑆”⟩ ∼ ⟨“𝑋𝑌𝑍”⟩) & ⊢ (𝜑 → (𝑉 − 𝑆) = (𝑌 − 𝑋)) ⇒ ⊢ (𝜑 → (⟨“𝑋𝑌𝑍”⟩ + ⟨“𝑈𝑉𝑊”⟩) = ⟨“𝑈𝑉𝑆”⟩)

23-Aug-2026	angmgmaddov1 29275	Value of the addition operation in the angle addition magma, in case the first angle is neither zero nor flat. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ + = (𝑒 ∈ 𝐴, 𝑓 ∈ 𝐴 ↦ if((𝑒‘0) ∈ ((𝑒‘1)𝐿(𝑒‘2)), ⟨“(𝑓‘0)(𝑓‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑓‘2)(𝑓‘1)𝑠”⟩ ∼ 𝑒 ∧ ((𝑓‘1) − 𝑠) = ((𝑒‘1) − (𝑒‘0))))”⟩, ⟨“(𝑒‘0)(𝑒‘1)(℩𝑠 ∈ 𝑃 (⟨“(𝑒‘2)(𝑒‘1)𝑠”⟩ ∼ 𝑓 ∧ ((𝑒‘1) − 𝑠) = ((𝑓‘1) − (𝑓‘0)) ∧ (((𝑒‘1)𝐿(𝑒‘2)) ∩ (𝑠𝐼(𝑒‘0))) ≠ ∅))”⟩)) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍)) & ⊢ (𝜑 → 𝑆 ∈ 𝑃) & ⊢ (𝜑 → ⟨“𝑍𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩) & ⊢ (𝜑 → (𝑌 − 𝑆) = (𝑉 − 𝑈)) & ⊢ (𝜑 → ((𝑌𝐿𝑍) ∩ (𝑆𝐼𝑋)) ≠ ∅) ⇒ ⊢ (𝜑 → (⟨“𝑋𝑌𝑍”⟩ + ⟨“𝑈𝑉𝑊”⟩) = ⟨“𝑋𝑌𝑆”⟩)

23-Aug-2026	angmgmaddov2lem 29274	Lemma for angmgmaddov2 29276. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → 𝑋 ∈ (𝑌𝐿𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑊𝑉𝑠”⟩ ∼ ⟨“𝑋𝑌𝑍”⟩ ∧ (𝑉 − 𝑠) = (𝑌 − 𝑋)))

23-Aug-2026	angmgmaddov1lem 29273	Lemma for angmgmaddov1 29275. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍)) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))

23-Aug-2026	angmgmaddeu7 29272	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where both angles are straight angles. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) & ⊢ (𝜑 → 𝑉 ∈ (𝑈𝐼𝑊)) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))

23-Aug-2026	angmgmaddeu6 29271	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where the first angle is a zero angle, and the second angle is a straight angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐼𝑍)) & ⊢ (𝜑 → 𝑈((hlG‘𝐺)‘𝑉)𝑊) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))

23-Aug-2026	angmgmaddeu5 29270	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where one angle is a zero angle, and the other angle is a straight angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → 𝑋((hlG‘𝐺)‘𝑌)𝑍) & ⊢ (𝜑 → 𝑉 ∈ (𝑈𝐼𝑊)) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))

23-Aug-2026	angmgmaddeu4 29269	There exists a unique point 𝑠 satisfying the conditions of angle addition. Case where both angles are zero angles. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → 𝑋((hlG‘𝐺)‘𝑌)𝑍) & ⊢ (𝜑 → 𝑈((hlG‘𝐺)‘𝑉)𝑊) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈)))

23-Aug-2026	angmgmaddeu3 29268	Existence of a unique point for building angle addition. Case where the second angle is a flat angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍)) & ⊢ (𝜑 → 𝑉 ∈ (𝑈𝐼𝑊)) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))

23-Aug-2026	angmgmaddeu2 29267	Existence of a unique point for building angle addition. Case where the second angle is a zero angle. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍)) & ⊢ (𝜑 → 𝑈((hlG‘𝐺)‘𝑉)𝑊) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))

23-Aug-2026	angmgmaddeu1 29266	There exists a unique point 𝑠 satisfying the conditions of angle addition. General case. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ≠ 𝑉) & ⊢ (𝜑 → 𝑉 ≠ 𝑊) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) & ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑌𝐿𝑍)) & ⊢ (𝜑 → ¬ 𝑈 ∈ (𝑉𝐿𝑊)) ⇒ ⊢ (𝜑 → ∃!𝑠 ∈ 𝑃 (⟨“𝑍𝑌𝑠”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩ ∧ (𝑌 − 𝑠) = (𝑉 − 𝑈) ∧ ((𝑌𝐿𝑍) ∩ (𝑠𝐼𝑋)) ≠ ∅))

23-Aug-2026	elcgrabasrd 29263	Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ≠ 𝑍) ⇒ ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∈ 𝐴)

23-Aug-2026	elcgrabasi 29262	Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 ∈ V & ⊢ 𝐴 = {𝑑 ∈ (𝑃 ↑_m (0..^3)) ∣ ((𝑑‘0) ≠ (𝑑‘1) ∧ (𝑑‘1) ≠ (𝑑‘2))} & ⊢ (𝜑 → 𝐸 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝐸 = ⟨“𝑥𝑦𝑧”⟩ ∧ (𝑥 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧)))

23-Aug-2026	tgaaddcpbl2 29240	The angular addition is compatible with angle congruence: by adding congruent angles together, we obtain congruent angles. Compared with tgaaddcpbl 29239, this version handles cases where 𝑈, 𝑉 and 𝑊 are aligned. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑆 ∈ 𝑃) & ⊢ (𝜑 → 𝑇 ∈ 𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝑃) & ⊢ (𝜑 → 𝑉 ∈ 𝑃) & ⊢ (𝜑 → 𝑊 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑍 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ≠ 𝑆) & ⊢ (𝜑 → 𝑉 ≠ 𝑇) & ⊢ (𝜑 → ((𝑌𝐿𝑆) ∩ (𝑋𝐼𝑍)) ≠ ∅) & ⊢ (𝜑 → ((𝑉𝐿𝑇) ∩ (𝑈𝐼𝑊)) ≠ ∅) & ⊢ (𝜑 → ⟨“𝑋𝑌𝑆”⟩ ∼ ⟨“𝑈𝑉𝑇”⟩) & ⊢ (𝜑 → ⟨“𝑆𝑌𝑍”⟩ ∼ ⟨“𝑇𝑉𝑊”⟩) ⇒ ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∼ ⟨“𝑈𝑉𝑊”⟩)

23-Aug-2026	zerocgra 29218	Zero angles are congruent. Zero angles, that is, angles of degree zero, can be expressed by stating that points 𝐴 and 𝐶 are on the same ray starting at 𝐵, that is, 𝐴(𝐾‘𝐵)𝐶. See also flatcgra 29219. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ ∼ = (cgrA‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐴(𝐾‘𝐵)𝐶) & ⊢ (𝜑 → 𝐷(𝐾‘𝐸)𝐹) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) ⇒ ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∼ ⟨“𝐷𝐸𝐹”⟩)

23-Aug-2026	lnoppinn0 29118	The segment between two points 𝑋 and 𝑌 on opposite sides of a line 𝐷 intersects 𝐷. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ 𝐿 = (LineG‘𝐺) & ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ ran 𝐿) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝑋𝑂𝑌) ⇒ ⊢ (𝜑 → (𝐷 ∩ (𝑋𝐼𝑌)) ≠ ∅)

23-Aug-2026	tghlsub 28973	Removing identical parts from the end of a ray segment preserves congruence. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐾 = (hlG‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐴(𝐾‘𝐵)𝐶) & ⊢ (𝜑 → 𝐷(𝐾‘𝐸)𝐹) & ⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) & ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐸 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = (𝐹 − 𝐷))

23-Aug-2026	tgsegconeu 28836	The point constructed in axtgsegcon 28813 is unique. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑃 = (Base‘𝐺) & ⊢ − = (dist‘𝐺) & ⊢ 𝐼 = (Itv‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TarskiG) & ⊢ (𝜑 → 𝑋 ∈ 𝑃) & ⊢ (𝜑 → 𝑌 ∈ 𝑃) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) ⇒ ⊢ (𝜑 → ∃!𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵)))

23-Aug-2026	s3rexrd 15026	Converse of s3rex 15025, deduction form. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) ⇒ ⊢ (𝜑 → ⟨“𝑋𝑌𝑍”⟩ ∈ (𝑆 ↑_m (0..^3)))

23-Aug-2026	s3rex 15025	Membership in a family of words of length 3. (Contributed by Thierry Arnoux, 23-Aug-2026.)
⊢ 𝑆 ∈ V ⇒ ⊢ (𝐴 ∈ (𝑆 ↑_m (0..^3)) ↔ ∃𝑥 ∈ 𝑆 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑆 𝐴 = ⟨“𝑥𝑦𝑧”⟩)

21-Aug-2026	degenmgm2 19059	A degenerate magma: although the operation is not defined for all pairs of elements of the base set, and its domain is not (a subset of) the base set, and the operation is not a function (see degenmgm2nfun 19058), the structure 𝑀 is still a magma according to our definition. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 2_o⟩}⟩} ⇒ ⊢ 𝑀 ∈ Mgm

21-Aug-2026	degenmgm2nfun 19058	The operation of a second degenerate magma is not a function. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 2_o⟩}⟩} ⇒ ⊢ ¬ Fun (+_g‘𝑀)

21-Aug-2026	degenmgm2opdm 19057	The domain of the operation of a second degenerate magma. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 2_o⟩}⟩} ⇒ ⊢ dom (+_g‘𝑀) = ({1_o} × {1_o, 2_o})

21-Aug-2026	degenmgmnfn 19055	The operation of a degenerate magma is not a function on its base set. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, ∅⟩, 1_o⟩}⟩} & ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ¬ (+_g‘𝑀) Fn (𝐵 × 𝐵)

21-Aug-2026	degenmgmbas 19054	The base set of a degenerate magma. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, ∅⟩, 1_o⟩}⟩} & ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ 𝐵 = {∅, 1_o}

21-Aug-2026	xpsnprg 7140	The Cartesian product of a singleton and an unordered pair. (Contributed by AV, 21-Aug-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈) → ({𝐴} × {𝐵, 𝐶}) = {⟨𝐴, 𝐵⟩, ⟨𝐴, 𝐶⟩})

19-Aug-2026	veroquadmodzerod 50825	The columns of the Veronese matrix, weighted by the coefficients 𝐾, sum to the zero vector of ℝ_fld freeLMod (1...6). (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) & ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0) ⇒ ⊢ (𝜑 → ((ℝ_fld freeLMod (1...6)) Σ_g (𝐾 ∘_f ( ·_𝑠 ‘(ℝ_fld freeLMod (1...6)))curry tpos 𝑉)) = (0_g‘(ℝ_fld freeLMod (1...6))))

19-Aug-2026	veroquadgsumlem 50824	Lemma for veroquadmodzerod 50825. Express the common homogeneous quadratic equation in ℝ_fld Σ_g form using the Veronese matrix 𝑉. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) & ⊢ (𝜑 → 𝐾:(1...6)⟶ℝ) & ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (((((𝐾‘1) · (((𝐴‘𝑖)‘1)↑2)) + ((𝐾‘2) · (((𝐴‘𝑖)‘2)↑2))) + ((𝐾‘3) · (((𝐴‘𝑖)‘3)↑2))) + ((((𝐾‘4) · (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2))) + ((𝐾‘5) · (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)))) + ((𝐾‘6) · (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))) = 0) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (1...6)) → (ℝ_fld Σ_g (𝑗 ∈ (1...6) ↦ ((𝐾‘𝑗) · ((curry 𝑉‘𝑖)‘𝑗)))) = 0)

19-Aug-2026	veronesematrowexpd 50823	Currying the Veronese matrix gives the indexed family of Veronese images, with each image expressed explicitly by coordinates. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → curry 𝑉 = (𝑖 ∈ (1...6) ↦ (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, (((𝐴‘𝑖)‘1)↑2), if(𝑘 = 2, (((𝐴‘𝑖)‘2)↑2), if(𝑘 = 3, (((𝐴‘𝑖)‘3)↑2), if(𝑘 = 4, (((𝐴‘𝑖)‘1) · ((𝐴‘𝑖)‘2)), if(𝑘 = 5, (((𝐴‘𝑖)‘2) · ((𝐴‘𝑖)‘3)), (((𝐴‘𝑖)‘3) · ((𝐴‘𝑖)‘1))))))))))

19-Aug-2026	veronesematrowd 50822	Currying the Veronese matrix gives the indexed family of Veronese images of the points 𝐴‘𝑖. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → curry 𝑉 = (𝑖 ∈ (1...6) ↦ (veronese‘(𝐴‘𝑖))))

19-Aug-2026	veronesematbasd 50821	The matrix whose 𝑖-th row is the Veronese image of 𝐴‘𝑖 belongs to the base set of (1...6) Mat ℝ_fld. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ 𝑉 = (𝑖 ∈ (1...6), 𝑗 ∈ (1...6) ↦ ((veronese‘(𝐴‘𝑖))‘𝑗)) & ⊢ (𝜑 → 𝐴:(1...6)⟶(ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → 𝑉 ∈ (Base‘((1...6) Mat ℝ_fld)))

19-Aug-2026	veronesefvcl 50813	Every coordinate of the Veronese map of a real 3-vector is real. (Contributed by Jiamin Zhao, 19-Aug-2026.)
⊢ ((𝑄 ∈ (ℝ ↑_m (1...3)) ∧ 𝐾 ∈ (1...6)) → ((veronese‘𝑄)‘𝐾) ∈ ℝ)

19-Aug-2026	omeiunle 47353	The outer measure of the indexed union of a countable set is less than or equal to the extended sum of the outer measures. The proof uses abrexct 23686 rather than fnrndomg 10546, and so does not require ax-ac 10465. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Vincent Gonzalez, 19-Aug-2026.)
⊢ Ⅎ𝑛𝜑 & ⊢ Ⅎ𝑛𝐸 & ⊢ (𝜑 → 𝑂 ∈ OutMeas) & ⊢ 𝑋 = ∪ dom 𝑂 & ⊢ 𝑍 = (ℤ_≥‘𝑁) & ⊢ (𝜑 → 𝐸:𝑍⟶𝒫 𝑋) ⇒ ⊢ (𝜑 → (𝑂‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ≤ (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑂‘(𝐸‘𝑛)))))

19-Aug-2026	disjinfi 46032	Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶. The proof uses fodomfi 9286 rather than fodomg 10528, and so does not require ax-ac 10465. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Revised by Vincent Gonzalez, 19-Aug-2026.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝜑 → 𝐶 ∈ Fin) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)

19-Aug-2026	sigaclci 34650	A sigma-algebra is closed under countable intersections. Deduction version. The proof uses abrexct 23686 rather than abrexdom2jm 32991, and so does not require ax-ac 10465. (Contributed by Thierry Arnoux, 19-Sep-2016.) (Revised by Vincent Gonzalez, 19-Aug-2026.)
⊢ (((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆) ∧ (𝐴 ≼ ω ∧ 𝐴 ≠ ∅)) → ∩ 𝐴 ∈ 𝑆)

19-Aug-2026	madefi 28186	The made set of an ordinal natural is finite. (Contributed by Scott Fenton, 20-Aug-2025.) (Proof shortened by Vincent Gonzalez, 19-Aug-2026.)
⊢ (𝐴 ∈ ω → ( M ‘𝐴) ∈ Fin)

18-Aug-2026	degenmgm 19056	A degenerate magma: although the operation is not defined for all pairs of elements of the base set ((∅(+_g‘𝑀)1_o) and (∅(+_g‘𝑀)∅) are not defined, and therefore are ∅ by definition, which is contained in the base set), and its domain is not (a subset of) the base set (2_o is in the domain of the operation, but not in the base set) , the structure 𝑀 is still a magma according to our definition. (Contributed by AV, 18-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, ∅⟩, 1_o⟩}⟩} ⇒ ⊢ 𝑀 ∈ Mgm

18-Aug-2026	degenmgmopdm 19053	The domain of the operation of a degenerate magma. (Contributed by AV, 18-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1_o}⟩, ⟨(+_g‘ndx), {⟨⟨1_o, 1_o⟩, 1_o⟩, ⟨⟨1_o, 2_o⟩, 1_o⟩, ⟨⟨1_o, ∅⟩, 1_o⟩}⟩} ⇒ ⊢ dom (+_g‘𝑀) = ({1_o} × {∅, 1_o, 2_o})

18-Aug-2026	mndideu 18853	The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by Mario Carneiro, 8-Dec-2014.) (Proof shortened by AV, 18-Aug-2026.)
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+_g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))

18-Aug-2026	mgmideud 18759	Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 18-Aug-2026.)
⊢ (𝜑 → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)) ⇒ ⊢ (𝜑 → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))

18-Aug-2026	fvtp0 7203	The undefined value of a function with a domain of three elements. (Contributed by AV, 18-Aug-2026.)
⊢ 𝐷 ∈ V & ⊢ 𝐸 ∈ V & ⊢ 𝐹 ∈ V & ⊢ 𝑋 ∈ V ⇒ ⊢ ((𝑋 ≠ 𝐴 ∧ 𝑋 ≠ 𝐵 ∧ 𝑋 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝑋) = ∅)

18-Aug-2026	xpsntpg 7141	The Cartesian product of a singleton and an unordered triple. (Contributed by AV, 18-Aug-2026.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑇)) → ({𝐴} × {𝐵, 𝐶, 𝐷}) = {⟨𝐴, 𝐵⟩, ⟨𝐴, 𝐶⟩, ⟨𝐴, 𝐷⟩})

17-Aug-2026	veronesevrowd 50820	The Veronese map at a point, expressed explicitly as a piecewise maps-to function on the six coordinates. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → (veronese‘𝑃) = (𝑘 ∈ (1...6) ↦ if(𝑘 = 1, ((𝑃‘1)↑2), if(𝑘 = 2, ((𝑃‘2)↑2), if(𝑘 = 3, ((𝑃‘3)↑2), if(𝑘 = 4, ((𝑃‘1) · (𝑃‘2)), if(𝑘 = 5, ((𝑃‘2) · (𝑃‘3)), ((𝑃‘3) · (𝑃‘1)))))))))

17-Aug-2026	veronesev6lem 50819	Lemma for veronesevrowd 50820. Value of the sixth coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → ((veronese‘𝑃)‘6) = ((𝑃‘3) · (𝑃‘1)))

17-Aug-2026	veronesev5lem 50818	Lemma for veronesevrowd 50820. Value of the fifth coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → ((veronese‘𝑃)‘5) = ((𝑃‘2) · (𝑃‘3)))

17-Aug-2026	veronesev4lem 50817	Lemma for veronesevrowd 50820. Value of the fourth coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → ((veronese‘𝑃)‘4) = ((𝑃‘1) · (𝑃‘2)))

17-Aug-2026	veronesev3lem 50816	Lemma for veronesevrowd 50820. Value of the third coordinate of the Veronese map at a point. (Contributed by Jiamin Zhao, 17-Aug-2026.)
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑_m (1...3))) ⇒ ⊢ (𝜑 → ((veronese‘𝑃)‘3) = ((𝑃‘3)↑2))

17-Aug-2026	difelsiga 34653	A sigma-algebra is closed under class differences. The proof goes through difunielsiga 34651 and unelsiga 34652 rather than countable intersection, and so does not use ax-ac 10465. (Contributed by Thierry Arnoux, 13-Sep-2016.) (Proof shortened by Vincent Gonzalez, 17-Aug-2026.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 ∖ 𝐵) ∈ 𝑆)

17-Aug-2026	difunielsiga 34651	A sigma-algebra is closed under complement relative to its base set. This is immediate from the definition, see issiga 34630, but the library states it nowhere in this form. (Contributed by Vincent Gonzalez, 17-Aug-2026.)
⊢ ((𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝑆) → (∪ 𝑆 ∖ 𝐴) ∈ 𝑆)

Older news:

(29-Jul-2020) Mario Carneiro presented MM0 at the CICM conference. See this Google Group post which includes a YouTube link.

(20-Jul-2020) Rohan Ridenour found 5 shorter D-proofs in our Shortest known proofs... file. In particular, he reduced *4.39 from 901 to 609 steps. A note on the Metamath Solitaire page mentions a tool that he worked with.

(19-Jul-2020) David A. Wheeler posted a video (https://youtu.be/3R27Qx69jHc) on how to (re)prove Schwabh�user 4.6 for the Metamath Proof Explorer. See also his older videos.

(19-Jul-2020) In version 0.184 of the metamath program, "verify markup" now checks that mathboxes are independent i.e. do not cross-reference each other. To turn off this check, use "/mathbox_skip"

(30-Jun-2020) In version 0.183 of the metamath program, (1) "verify markup" now has checking for (i) underscores in labels, (ii) that *ALT and *OLD theorems have both discouragement tags, and (iii) that lines don't have trailing spaces. (2) "save proof.../rewrap" no longer left-aligns $p/$a comments that contain the string "<HTML>"; see this note.

(5-Apr-2020) Glauco Siliprandi added a new proof to the 100 theorem list, e is Transcendental etransc, bringing the Metamath total to 74.

(12-Feb-2020) A bug in the 'minimize' command of metamath.exe versions 0.179 (29-Nov-2019) and 0.180 (10-Dec-2019) may incorrectly bring in the use of new axioms. Version 0.181 fixes it.

(20-Jan-2020) David A. Wheeler created a video called Walkthrough of the tutorial in mmj2. See the Google Group announcement for more details. (All of his videos are listed on the Other Metamath-Related Topics page.)

(18-Jan-2020) The FOMM 2020 talks are on youtube now. Mario Carneiro's talk is Metamath Zero, or: How to Verify a Verifier. Since they are washed out in the video, the PDF slides are available separately.

(14-Dec-2019) Glauco Siliprandi added a new proof to the 100 theorem list, Fourier series convergence fourier, bringing the Metamath total to 73.

(25-Nov-2019) Alexander van der Vekens added a new proof to the 100 theorem list, The Cayley-Hamilton Theorem cayleyhamilton, bringing the Metamath total to 72.

(25-Oct-2019) Mario Carneiro's paper "Metamath Zero: The Cartesian Theorem Prover" (submitted to CPP 2020) is now available on arXiv: https://arxiv.org/abs/1910.10703. There is a related discussion on Hacker News.

(30-Sep-2019) Mario Carneiro's talk about MM0 at ITP 2019 is available on YouTube: x86 verification from scratch (24 minutes). Google Group discussion: Metamath Zero.

(29-Sep-2019) David Wheeler created a fascinating Gource video that animates the construction of set.mm, available on YouTube: Metamath set.mm contributions viewed with Gource through 2019-09-26 (4 minutes). Google Group discussion: Gource video of set.mm contributions.

(24-Sep-2019) nLab added a page for Metamath. It mentions Stefan O'Rear's Busy Beaver work using the set.mm axiomatization (and fails to mention Mario's definitional soundness checker)

(1-Sep-2019) Xuanji Li published a Visual Studio Code extension to support metamath syntax highlighting.

(10-Aug-2019) (revised 21-Sep-2019) Version 0.178 of the metamath program has the following changes: (1) "minimize_with" will now prevent dependence on new $a statements unless the new qualifier "/allow_new_axioms" is specified. For routine usage, it is suggested that you use "minimize_with * /allow_new_axioms * /no_new_axioms_from ax-*" instead of just "minimize_with *". See "help minimize_with" and this Google Group post. Also note that the qualifier "/allow_growth" has been renamed to "/may_grow". (2) "/no_versioning" was added to "write theorem_list".

(8-Jul-2019) Jon Pennant announced the creation of a Metamath search engine. Try it and feel free to comment on it at https://groups.google.com/d/msg/metamath/cTeU5AzUksI/5GesBfDaCwAJ.

(16-May-2019) Set.mm now has a major new section on elementary geometry. This begins with definitions that implement Tarski's axioms of geometry (including concepts such as congruence and betweenness). This uses set.mm's extensible structures, making them easier to use for many circumstances. The section then connects Tarski geometry with geometry in Euclidean places. Most of the work in this section is due to Thierry Arnoux, with earlier work by Mario Carneiro and Scott Fenton. [Reported by DAW.]

(9-May-2019) We are sad to report that long-time contributor Alan Sare passed away on Mar. 23. There is some more information at the top of his mathbox (click on "Mathbox for Alan Sare") and his obituary. We extend our condolences to his family.

(10-Mar-2019) Jon Pennant and Mario Carneiro added a new proof to the 100 theorem list, Heron's formula heron, bringing the Metamath total to 71.

(22-Feb-2019) Alexander van der Vekens added a new proof to the 100 theorem list, Cramer's rule cramer, bringing the Metamath total to 70.

(6-Feb-2019) David A. Wheeler has made significant improvements and updates to the Metamath book. Any comments, errors found, or suggestions are welcome and should be turned into an issue or pull request at https://github.com/metamath/metamath-book (or sent to me if you prefer).

(26-Dec-2018) I added Appendix 8 to the MPE Home Page that cross-references new and old axiom numbers.

(20-Dec-2018) The axioms have been renumbered according to this Google Groups post.

(24-Nov-2018) Thierry Arnoux created a new page on topological structures. The page along with its SVG files are maintained on GitHub.

(11-Oct-2018) Alexander van der Vekens added a new proof to the 100 theorem list, the Friendship Theorem friendship, bringing the Metamath total to 69.

(1-Oct-2018) Naip Moro has written gramm, a Metamath proof verifier written in Antlr4/Java.

(16-Sep-2018) The definition df-riota has been simplified so that it evaluates to the empty set instead of an Undef value. This change affects a significant part of set.mm.

(2-Sep-2018) Thierry Arnoux added a new proof to the 100 theorem list, Euler's partition theorem eulerpart, bringing the Metamath total to 68.

(1-Sep-2018) The Kate editor now has Metamath syntax highlighting built in. (Communicated by Wolf Lammen.)

(15-Aug-2018) The Intuitionistic Logic Explorer now has a Most Recent Proofs page.

(4-Aug-2018) Version 0.163 of the metamath program now indicates (with an asterisk) which Table of Contents headers have associated comments.

(10-May-2018) George Szpiro, journalist and author of several books on popular mathematics such as Poincare's Prize and Numbers Rule, used a genetic algorithm to find shorter D-proofs of "*3.37" and "meredith" in our Shortest known proofs... file.

(19-Apr-2018) The EMetamath Eclipse plugin has undergone many improvements since its initial release as the change log indicates. Thierry uses it as his main proof assistant and writes, "I added support for mmj2's auto-transformations, which allows it to infer several steps when building proofs. This added a lot of comfort for writing proofs.... I can now switch back and forth between the proof assistant and editing the Metamath file.... I think no other proof assistant has this feature."

(11-Apr-2018) Benoît Jubin solved an open problem about the "Axiom of Twoness," showing that it is necessary for completeness. See item 14 on the "Open problems and miscellany" page.

(25-Mar-2018) Giovanni Mascellani has announced mmpp, a new proof editing environment for the Metamath language.

(27-Feb-2018) Bill Hale has released an app for the Apple iPad and desktop computer that allows you to browse Metamath theorems and their proofs.

(17-Jan-2018) Dylan Houlihan has kindly provided a new mirror site. He has also provided an rsync server; type "rsync uk.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(15-Jan-2018) The metamath program, version 0.157, has been updated to implement the file inclusion conventions described in the 21-Dec-2017 entry of mmnotes.txt.

(11-Dec-2017) I added a paragraph, suggested by Gérard Lang, to the distinct variable description here.

(10-Dec-2017) Per FL's request, his mathbox will be removed from set.mm. If you wish to export any of his theorems, today's version (master commit 1024a3a) is the last one that will contain it.

(11-Nov-2017) Alan Sare updated his completeusersproof program.

(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript. He also wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.

(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)

(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.

(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.

(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.

(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.

(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).

(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.

(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.

(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.

(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.

(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.

(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.

(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.

(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.

(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.

(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.

(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica

(12-Aug-2016) A Gitter chat room has been created for Metamath.

(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project

(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.

(4-Aug-2016) Mario gave two presentations at CICM 2016.

(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.

(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.

(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.

(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.

(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).

(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language.

(10-Jun-2016) If you are using metamath program versions 0.128, 0.129, or 0.130, please update to version 0.131. (In the bad versions, 'minimize_with' ignores distinct variable violations.)

(1-Jun-2016) Mario Carneiro added new proofs to the 100 theorem list, the Prime Number Theorem pnt and the Perfect Number Theorem perfect, bringing the Metamath total to 58.

(12-May-2016) Mario Carneiro added a new proof to the 100 theorem list, Dirichlet's theorem dirith, bringing the Metamath total to 56. (Added 17-May-2016) An informal exposition of the proof can be found at http://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html

(10-Mar-2016) Metamath program version 0.125 adds a new qualifier, /fast, to 'save proof'. See the mmnotes.txt entry of 10-Mar-2016.

(6-Mar-2016) The most recent set.mm has a large update converting variables from letters to symbols. See this Google Groups post.

(16-Feb-2016) Mario Carneiro's new paper "Models for Metamath" can be found here and on arxiv.org.

(6-Feb-2016) There are now 22 math symbols that can be used as variable names. See mmascii.html near the 50th table row, starting with "./\".

(29-Jan-2016) Metamath program version 0.123 adds /packed and /explicit qualifiers to 'save proof' and 'show proof'. See this Google Groups post.

(13-Jan-2016) The Unicode math symbols now provide for external CSS and use the XITS web font. Thanks to David A. Wheeler, Mario Carneiro, Cris Perdue, Jason Orendorff, and Frédéric Liné for discussions on this topic. Two commands, htmlcss and htmlfont, were added to the $t comment in set.mm and are recognized by Metamath program version 0.122.

(21-Dec-2015) Axiom ax-12, now renamed ax-12o, was replaced by a new shorter equivalent, ax-12. The equivalence is provided by theorems ax12o and ax12.

(13-Dec-2015) A new section on the theory of classes was added to the MPE Home Page. Thanks to Gérard Lang for suggesting this section and improvements to it.

(17-Nov-2015) Metamath program version 0.121: 'verify markup' was added to check comment markup consistency; see 'help verify markup'. You are encouraged to make sure 'verify markup */f' has no warnings prior to mathbox submissions. The date consistency rules are given in this Google Groups post.

(23-Sep-2015) Drahflow wrote, "I am currently working on yet another proof assistant, main reason being: I understand stuff best if I code it. If anyone is interested: https://github.com/Drahflow/Igor (but in my own programming language, so expect a complicated build process :P)"

(23-Aug-2015) Ivan Kuckir created MM Tool, a Metamath proof verifier and editor written in JavaScript that runs in a browser.

(25-Jul-2015) Axiom ax-10 is shown to be redundant by theorem ax10 , so it was removed from the predicate calculus axiom list.

(19-Jul-2015) Mario Carneiro gave two talks related to Metamath at CICM 2015, which are linked to at Other Metamath-Related Topics.

(18-Jul-2015) The metamath program has been updated to version 0.118. 'show trace_back' now has a '/to' qualifier to show the path back to a specific axiom such as ax-ac. See 'help show trace_back'.

(12-Jul-2015) I added the HOL Explorer for Mario Carneiro's hol.mm database. Although the home page needs to be filled out, the proofs can be accessed.

(11-Jul-2015) I started a new page, Other Metamath-Related Topics, that will hold miscellaneous material that doesn't fit well elsewhere (or is hard to find on this site). Suggestions welcome.

(23-Jun-2015) Metamath's mascot, Penny the cat (2007 photo), passed away today. She was 18 years old.

(21-Jun-2015) Mario Carneiro added 3 new proofs to the 100 theorem list: All Primes (1 mod 4) Equal the Sum of Two Squares 2sq, The Law of Quadratic Reciprocity lgsquad and the AM-GM theorem amgm, bringing the Metamath total to 55.

(13-Jun-2015) Stefan O'Rear's smm, written in JavaScript, can now be used as a standalone proof verifier. This brings the total number of independent Metamath verifiers to 8, written in just as many languages (C, Java. JavaScript, Python, Haskell, Lua, C#, C++).

(12-Jun-2015) David A. Wheeler added 2 new proofs to the 100 theorem list: The Law of Cosines lawcos and Ptolemy's Theorem ptolemy, bringing the Metamath total to 52.

(30-May-2015) The metamath program has been updated to version 0.117. (1) David A. Wheeler provided an enhancement to speed up the 'improve' command by 28%; see README.TXT for more information. (2) In web pages with proofs, local hyperlinks on step hypotheses no longer clip the Expression cell at the top of the page.

(9-May-2015) Stefan O'Rear has created an archive of older set.mm releases back to 1998: https://github.com/sorear/set.mm-history/.

(7-May-2015) The set.mm dated 7-May-2015 is a major revision, updated by Mario, that incorporates the new ordered pair definition df-op that was agreed upon. There were 700 changes, listed at the top of set.mm. Mathbox users are advised to update their local mathboxes. As usual, if any mathbox user has trouble incorporating these changes into their mathbox in progress, Mario or I will be glad to do them for you.

(7-May-2015) Mario has added 4 new theorems to the 100 theorem list: Ramsey's Theorem ramsey, The Solution of a Cubic cubic, The Solution of the General Quartic Equation quart, and The Birthday Problem birthday. In the Supplementary List, Stefan O'Rear added the Hilbert Basis Theorem hbt.

(28-Apr-2015) A while ago, Mario Carneiro wrote up a proof of the unambiguity of set.mm's grammar, which has now been added to this site: grammar-ambiguity.txt.

(22-Apr-2015) The metamath program has been updated to version 0.114. In MM-PA, 'show new_proof/unknown' now shows the relative offset (-1, -2,...) used for 'assign' arguments, suggested by Stefan O'Rear.

(20-Apr-2015) I retrieved an old version of the missing "Metamath 100" page from archive.org and updated it to what I think is the current state: mm_100.html. Anyone who wants to edit it can email updates to this page to me.

(19-Apr-2015) The metamath program has been updated to version 0.113, mostly with patches provided by Stefan O'Rear. (1) 'show statement %' (or any command allowing label wildcards) will select statements whose proofs were changed in current session. ('help search' will show all wildcard matching rules.) (2) 'show statement =' will select the statement being proved in MM-PA. (3) The proof date stamp is now created only if the proof is complete.

(18-Apr-2015) There is now a section for Scott Fenton's NF database: New Foundations Explorer.

(16-Apr-2015) Mario describes his recent additions to set.mm at https://groups.google.com/forum/#!topic/metamath/VAGNmzFkHCs. It include 2 new additions to the Formalizing 100 Theorems list, Leibniz' series for pi (leibpi) and the Konigsberg Bridge problem (konigsberg)

(10-Mar-2015) Mario Carneiro has written a paper, "Arithmetic in Metamath, Case Study: Bertrand's Postulate," for CICM 2015. A preprint is available at arXiv:1503.02349.

(23-Feb-2015) Scott Fenton has created a Metamath formalization of NF set theory: https://github.com/sctfn/metamath-nf/. For more information, see the Metamath Google Group posting.

(28-Jan-2015) Mario Carneiro added Wilson's Theorem (wilth), Ascending or Descending Sequences (erdsze, erdsze2), and Derangements Formula (derangfmla, subfaclim), bringing the Metamath total for Formalizing 100 Theorems to 44.

(19-Jan-2015) Mario Carneiro added Sylow's Theorem (sylow1, sylow2, sylow2b, sylow3), bringing the Metamath total for Formalizing 100 Theorems to 41.

(9-Jan-2015) The hypothesis order of mpbi*an* was changed. See the Notes entry of 9-Jan-2015.

(1-Jan-2015) Mario Carneiro has written a paper, "Conversion of HOL Light proofs into Metamath," that has been submitted to the Journal of Formalized Reasoning. A preprint is available on arxiv.org.

(22-Nov-2014) Stefan O'Rear added the Solutions to Pell's Equation (rmxycomplete) and Liouville's Theorem and the Construction of Transcendental Numbers (aaliou), bringing the Metamath total for Formalizing 100 Theorems to 40.

(22-Nov-2014) The metamath program has been updated with version 0.111. (1) Label wildcards now have a label range indicator "~" so that e.g. you can show or search all of the statements in a mathbox. See 'help search'. (Stefan O'Rear added this to the program.) (2) A qualifier was added to 'minimize_with' to prevent the use of any axioms not already used in the proof e.g. 'minimize_with * /no_new_axioms_from ax-*' will prevent the use of ax-ac if the proof doesn't already use it. See 'help minimize_with'.

(10-Oct-2014) Mario Carneiro has encoded the axiomatic basis for the HOL theorem prover into a Metamath source file, hol.mm.

(24-Sep-2014) Mario Carneiro added the Sum of the Angles of a Triangle (ang180), bringing the Metamath total for Formalizing 100 Theorems to 38.

(15-Sep-2014) Mario Carneiro added the Fundamental Theorem of Algebra (fta), bringing the Metamath total for Formalizing 100 Theorems to 37.

(3-Sep-2014) Mario Carneiro added the Fundamental Theorem of Integral Calculus (ftc1, ftc2). This brings the Metamath total for Formalizing 100 Theorems to 35. (added 14-Sep-2014) Along the way, he added the Mean Value Theorem (mvth), bringing the total to 36.

(16-Aug-2014) Mario Carneiro started a Metamath blog at http://metamath-blog.blogspot.com/.

(10-Aug-2014) Mario Carneiro added Erdős's proof of the divergence of the inverse prime series (prmrec). This brings the Metamath total for Formalizing 100 Theorems to 34.

(31-Jul-2014) Mario Carneiro added proofs for Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + .... (basel) and The Factor and Remainder Theorems (facth, plyrem). This brings the Metamath total for Formalizing 100 Theorems to 33.

(16-Jul-2014) Mario Carneiro added proofs for Four Squares Theorem (4sq), Formula for the Number of Combinations (hashbc), and Divisibility by 3 Rule (3dvds). This brings the Metamath total for Formalizing 100 Theorems to 31.

(11-Jul-2014) Mario Carneiro added proofs for Divergence of the Harmonic Series (harmonic), Order of a Subgroup (lagsubg), and Lebesgue Measure and Integration (itgcl). This brings the Metamath total for Formalizing 100 Theorems to 28.

(7-Jul-2014) Mario Carneiro presented a talk, "Natural Deduction in the Metamath Proof Language," at the 6PCM conference. Slides Audio

(25-Jun-2014) In version 0.108 of the metamath program, the 'minimize_with' command is now more automated. It now considers compressed proof length; it scans the statements in forward and reverse order and chooses the best; and it avoids $d conflicts. The '/no_distinct', '/brief', and '/reverse' qualifiers are obsolete, and '/verbose' no longer lists all statements scanned but gives more details about decision criteria.

(12-Jun-2014) To improve naming uniformity, theorems about operation values now use the abbreviation "ov". For example, df-opr, opreq1, oprabval5, and oprvres are now called df-ov, oveq1, ov5, and ovres respectively.

(11-Jun-2014) Mario Carneiro finished a major revision of set.mm. His notes are under the 11-Jun-2014 entry in the Notes

(4-Jun-2014) Mario Carneiro provided instructions and screenshots for syntax highlighting for the jEdit editor for use with Metamath and mmj2 source files.

(19-May-2014) Mario Carneiro added a feature to mmj2, in the build at https://github.com/digama0/mmj2/raw/dev-build/mmj2jar/mmj2.jar, which tests all but 5 definitions in set.mm for soundness. You can turn on the test by adding
SetMMDefinitionsCheckWithExclusions,ax-*,df-bi,df-clab,df-cleq,df-clel,df-sbc
to your RunParms.txt file.

(17-May-2014) A number of labels were changed in set.mm, listed at the top of set.mm as usual. Note in particular that the heavily-used visset, elisseti, syl11anc, syl111anc were changed respectively to vex, elexi, syl2anc, syl3anc.

(16-May-2014) Scott Fenton formalized a proof for "Sum of kth powers": fsumkthpow. This brings the Metamath total for Formalizing 100 Theorems to 25.

(9-May-2014) I (Norm Megill) presented an overview of Metamath at the "Formalization of mathematics in proof assistants" workshop at the Institut Henri Poincar� in Paris. The slides for this talk are here.

(22-Jun-2014) Version 0.107 of the metamath program adds a "PART" indention level to the Statement List table of contents, adds 'show proof ... /size' to show source file bytes used, and adds 'show elapsed_time'. The last one is helpful for measuring the run time of long commands. See 'help write theorem_list', 'help show proof', and 'help show elapsed_time' for more information.

(2-May-2014) Scott Fenton formalized a proof of Sum of the Reciprocals of the Triangular Numbers: trirecip. This brings the Metamath total for Formalizing 100 Theorems to 24.

(19-Apr-2014) Scott Fenton formalized a proof of the Formula for Pythagorean Triples: pythagtrip. This brings the Metamath total for Formalizing 100 Theorems to 23.

(11-Apr-2014) David A. Wheeler produced a much-needed and well-done video for mmj2, called "Introduction to Metamath & mmj2". Thanks, David!

(15-Mar-2014) Mario Carneiro formalized a proof of Bertrand's postulate: bpos. This brings the Metamath total for Formalizing 100 Theorems to 22.

(18-Feb-2014) Mario Carneiro proved that complex number axiom ax-cnex is redundant (theorem cnex). See also Real and Complex Numbers.

(11-Feb-2014) David A. Wheeler has created a theorem compilation that tracks those theorems in Freek Wiedijk's Formalizing 100 Theorems list that have been proved in set.mm. If you find a error or omission in this list, let me know so it can be corrected. (Update 1-Mar-2014: Mario has added eulerth and bezout to the list.)

(4-Feb-2014) Mario Carneiro writes:

The latest commit on the mmj2 development branch introduced an exciting new feature, namely syntax highlighting for mmp files in the main window. (You can pick up the latest mmj2.jar at https://github.com/digama0/mmj2/blob/develop/mmj2jar/mmj2.jar .) The reason I am asking for your help at this stage is to help with design for the syntax tokenizer, which is responsible for breaking down the input into various tokens with names like "comment", "set", and "stephypref", which are then colored according to the user's preference. As users of mmj2 and metamath, what types of highlighting would be useful to you?
One limitation of the tokenizer is that since (for performance reasons) it can be started at any line in the file, highly contextual coloring, like highlighting step references that don't exist previously in the file, is difficult to do. Similarly, true parsing of the formulas using the grammar is possible but likely to be unmanageably slow. But things like checking theorem labels against the database is quite simple to do under the current setup.
That said, how can this new feature be optimized to help you when writing proofs?

(13-Jan-2014) Mathbox users: the *19.21a*, *19.23a* series of theorems have been renamed to *alrim*, *exlim*. You can update your mathbox with a global replacement of string '19.21a' with 'alrim' and '19.23a' with 'exlim'.

(5-Jan-2014) If you downloaded mmj2 in the past 3 days, please update it with the current version, which fixes a bug introduced by the recent changes that made it unable to read in most of the proofs in the textarea properly.

(4-Jan-2014) I added a list of "Allowed substitutions" under the "Distinct variable groups" list on the theorem web pages, for example axsep. This is an experimental feature and comments are welcome.

(3-Jan-2014) Version 0.102 of the metamath program produces more space-efficient compressed proofs (still compatible with the specification in Appendix B of the Metamath book) using an algorithm suggested by Mario Carneiro. See 'help save proof' in the program. Also, mmj2 now generates proofs in the new format. The new mmj2 also has a mandatory update that fixes a bug related to the new format; you must update your mmj2 copy to use it with the latest set.mm.

(23-Dec-2013) Mario Carneiro has updated many older definitions to use the maps-to notation. If you have difficulty updating your local mathbox, contact him or me for assistance.

(1-Nov-2013) 'undo' and 'redo' commands were added to the Proof Assistant in metamath program version 0.07.99. See 'help undo' in the program.

(8-Oct-2013) Today's Notes entry describes some proof repair techniques.

(5-Oct-2013) Today's Notes entry explains some recent extensible structure improvements.

(8-Sep-2013) Mario Carneiro has revised the square root and sequence generator definitions. See today's Notes entry.

(3-Aug-2013) Mario Carneiro writes: "I finally found enough time to create a GitHub repository for development at https://github.com/digama0/mmj2. A permalink to the latest version plus source (akin to mmj2.zip) is https://github.com/digama0/mmj2/zipball/, and the jar file on its own (mmj2.jar) is at https://github.com/digama0/mmj2/blob/master/mmj2jar/mmj2.jar?raw=true. Unfortunately there is no easy way to automatically generate mmj2jar.zip, but this is available as part of the zip distribution for mmj2.zip. History tracking will be handled by the repository now. Do you have old versions of the mmj2 directory? I could add them as historical commits if you do."

(18-Jun-2013) Mario Carneiro has done a major revision and cleanup of the construction of real and complex numbers. In particular, rather than using equivalence classes as is customary for the construction of the temporary rationals, he used only "reduced fractions", so that the use of the axiom of infinity is avoided until it becomes necessary for the construction of the temporary reals.

(18-May-2013) Mario Carneiro has added the ability to produce compressed proofs to mmj2. This is not an official release but can be downloaded here if you want to try it: mmj2.jar. If you have any feedback, send it to me (NM), and I will forward it to Mario. (Disclaimer: this release has not been endorsed by Mel O'Cat. If anyone has been in contact with him, please let me know.)

(29-Mar-2013) Charles Greathouse reduced the size of our PNG symbol images using the pngout program.

(8-Mar-2013) Wolf Lammen has reorganized the theorems in the "Logical negation" section of set.mm into a more orderly, less scattered arrangement.

(27-Feb-2013) Scott Fenton has done a large cleanup of set.mm, eliminating *OLD references in 144 proofs. See the Notes entry for 27-Feb-2013.

(21-Feb-2013) *ATTENTION MATHBOX USERS* The order of hypotheses of many syl* theorems were changed, per a suggestion of Mario Carneiro. You need to update your local mathbox copy for compatibility with the new set.mm, or I can do it for you if you wish. See the Notes entry for 21-Feb-2013.

(16-Feb-2013) Scott Fenton shortened the direct-from-axiom proofs of *3.1, *3.43, *4.4, *4.41, *4.5, *4.76, *4.83, *5.33, *5.35, *5.36, and meredith in the "Shortest known proofs of the propositional calculus theorems from Principia Mathematica" (pmproofs.txt).

(27-Jan-2013) Scott Fenton writes, "I've updated Ralph Levien's mmverify.py. It's now a Python 3 program, and supports compressed proofs and file inclusion statements. This adds about fifty lines to the original program. Enjoy!"

(10-Jan-2013) A new mathbox was added for Mario Carneiro, who has contributed a number of cardinality theorems without invoking the Axiom of Choice. This is nice work, and I will be using some of these (those suffixed with "NEW") to replace the existing ones in the main part of set.mm that currently invoke AC unnecessarily.

(4-Jan-2013) As mentioned in the 19-Jun-2012 item below, Eric Schmidt discovered that the complex number axioms axaddcom (now addcom) and ax0id (now addid1) are redundant (schmidt-cnaxioms.pdf, .tex). In addition, ax1id (now mulid1) can be weakened to ax1rid. Scott Fenton has now formalized this work, so that now there are 23 instead of 25 axioms for real and complex numbers in set.mm. The Axioms for Complex Numbers page has been updated with these results. An interesting part of the proof, showing how commutativity of addition follows from other laws, is in addcomi.

(27-Nov-2012) The frequently-used theorems "an1s", "an1rs", "ancom13s", "ancom31s" were renamed to "an12s", "an32s", "an13s", "an31s" to conform to the convention for an12 etc.

(4-Nov-2012) The changes proposed in the Notes, renaming Grp to GrpOp etc., have been incorporated into set.mm. See the list of changes at the top of set.mm. If you want me to update your mathbox with these changes, send it to me along with the version of set.mm that it works with.

(20-Sep-2012) Mel O'Cat updated https://us.metamath.org/ocat/mmj2/TESTmmj2jar.zip. See the README.TXT for a description of the new features.

(21-Aug-2012) Mel O'Cat has uploaded SearchOptionsMockup9.zip, a mockup for the new search screen in mmj2. See the README.txt file for instructions. He will welcome feedback via x178g243 at yahoo.com.

(19-Jun-2012) Eric Schmidt has discovered that in our axioms for complex numbers, axaddcom and ax0id are redundant. (At some point these need to be formalized for set.mm.) He has written up these and some other nice results, including some independence results for the axioms, in schmidt-cnaxioms.pdf (schmidt-cnaxioms.tex).

(23-Apr-2012) Frédéric Liné sent me a PDF (LaTeX source) developed with Lamport's pf2 package. He wrote: "I think it works well with Metamath since the proofs are in a tree form. I use it to have a sketch of a proof. I get this way a better understanding of the proof and I can cut down its size. For instance, inpreima5 was reduced by 50% when I wrote the corresponding proof with pf2."

(5-Mar-2012) I added links to Wikiproofs and its recent changes in the "Wikis" list at the top of this page.

(12-Jan-2012) Thanks to William Hoza who sent me a ZFC T-shirt, and thanks to the ZFC models (courtesy of the Inaccessible Cardinals agency).

Front	Back	Detail

(24-Nov-2011) In metamath program version 0.07.71, the 'minimize_with' command by default now scans from bottom to top instead of top to bottom, since empirically this often (although not always) results in a shorter proof. A top to bottom scan can be specified with a new qualifier '/reverse'. You can try both methods (starting from the same original proof, of course) and pick the shorter proof.

(15-Oct-2011) From Mel O'Cat:
I just uploaded mmj2.zip containing the 1-Nov-2011 (20111101) release: https://us.metamath.org/ocat/mmj2/mmj2.zip https://us.metamath.org/ocat/mmj2/mmj2.md5
A few last minute tweaks:
1. I now bless double-click starting of mmj2.bat (MacMMJ2.command in Mac OS-X)! See mmj2\QuickStart.html
2. Much improved support of Mac OS-X systems. See mmj2\QuickStart.html
3. I tweaked the Command Line Argument Options report to
a) print every time;
b) print as much as possible even if there are errors in the command line arguments -- and the last line printed corresponds to the argument in error;
c) removed Y/N argument on the command line to enable/disable the report. this simplifies things.
4) Documentation revised, including the PATutorial.
See CHGLOG.TXT for list of all changes. Good luck. And thanks for all of your help!

(15-Sep-2011) MATHBOX USERS: I made a large number of label name changes to set.mm to improve naming consistency. There is a script at the top of the current set.mm that you can use to update your mathbox or older set.mm. Or if you wish, I can do the update on your next mathbox submission - in that case, please include a .zip of the set.mm version you used.

(30-Aug-2011) Scott Fenton shortened the direct-from-axiom proofs of *3.33, *3.45, *4.36, and meredith in the "Shortest known proofs of the propositional calculus theorems from Principia Mathematica" (pmproofs.txt).

(21-Aug-2011) A post on reddit generated 60,000 hits (and a TOS violation notice from my provider...),

(18-Aug-2011) The Metamath Google Group has a discussion of my canonical conjunctions proposal. Any feedback directly to me (Norm Megill) is also welcome.

(4-Jul-2011) John Baker has provided (metamath_kindle.zip) "a modified version of [the] metamath.tex [Metamath] book source that is formatted for the Kindle. If you compile the document the resulting PDF can be loaded into into a Kindle and easily read." (Update: the PDF file is now included also.)

(3-Jul-2011) Nested 'submit' calls are now allowed, in metamath program version 0.07.68. Thus you can create or modify a command file (script) from within a command file then 'submit' it. While 'submit' cannot pass arguments (nor are there plans to add this feature), you can 'substitute' strings in the 'submit' target file before calling it in order to emulate this.

(28-Jun-2011)The metamath program version 0.07.64 adds the '/include_mathboxes' qualifier to 'minimize_with'; by default, 'minimize_with *' will now skip checking user mathboxes. Since mathboxes should be independent from each other, this will help prevent accidental cross-"contamination". Also, '/rewrap' was added to 'write source' to automatically wrap $a and $p comments so as to conform to the current formatting conventions used in set.mm. This means you no longer have to be concerned about line length < 80 etc.

(19-Jun-2011) ATTENTION MATHBOX USERS: The wff variables et, ze, si, and rh are now global. This change was made primarily to resolve some conflicts between mathboxes, but it will also let you avoid having to constantly redeclare these locally in the future. Unfortunately, this change can affect the $f hypothesis order, which can cause proofs referencing theorems that use these variables to fail. All mathbox proofs currently in set.mm have been corrected for this, and you should refresh your local copy for further development of your mathbox. You can correct your proofs that are not in set.mm as follows. Only the proofs that fail under the current set.mm (using version 0.07.62 or later of the metamath program) need to be modified.

To fix a proof that references earlier theorems using et, ze, si, and rh, do the following (using a hypothetical theorem 'abc' as an example): 'prove abc' (ignore error messages), 'delete floating', 'initialize all', 'unify all/interactive', 'improve all', 'save new_proof/compressed'. If your proof uses dummy variables, these must be reassigned manually.

To fix a proof that uses et, ze, si, and rh as local variables, make sure the proof is saved in 'compressed' format. Then delete the local declarations ($v and $f statements) and follow the same steps above to correct the proof.

I apologize for the inconvenience. If you have trouble fixing your proofs, you can contact me for assistance.

Note: Versions of the metamath program before 0.07.62 did not flag an error when global variables were redeclared locally, as it should have according to the spec. This caused these spec violations to go unnoticed in some older set.mm versions. The new error messages are in fact just informational and can be ignored when working with older set.mm versions.

(7-Jun-2011) The metamath program version 0.07.60 fixes a bug with the 'minimize_with' command found by Andrew Salmon.

(12-May-2010) Andrew Salmon shortened many proofs, shown above. For comparison, I have temporarily kept the old version, which is suffixed with OLD, such as oridmOLD for oridm.

(9-Dec-2010) Eric Schmidt has written a Metamath proof verifier in C++, called checkmm.cpp.

(3-Oct-2010) The following changes were made to the tokens in set.mm. The subset and proper subset symbol changes to C_ and C. were made to prevent defeating the parenthesis matching in Emacs. Other changes were made so that all letters a-z and A-Z are now available for variable names. One-letter constants such as _V, _e, and _i are now shown on the web pages with Roman instead of italic font, to disambiguate italic variable names. The new convention is that a prefix of _ indicates Roman font and a prefix of ~ indicates a script (curly) font. Thanks to Stefan Allan and Frédéric Liné for discussions leading to this change.

Old	New	Description
C.	_C	binomial coefficient
E	_E	epsilon relation
e	_e	Euler's constant
I	_I	identity relation
i	_i	imaginary unit
V	_V	universal class
(_	C_	subset
(.	C.	proper subset
P~	~P	power class
H~	~H	Hilbert space

(25-Sep-2010) The metamath program (version 0.07.54) now implements the current Metamath spec, so footnote 2 on p. 92 of the Metamath book can be ignored.

(24-Sep-2010) The metamath program (version 0.07.53) fixes bug 2106, reported by Michal Burger.

(14-Sep-2010) The metamath program (version 0.07.52) has a revamped LaTeX output with 'show statement xxx /tex', which produces the combined statement, description, and proof similar to the web page generation. Also, 'show proof xxx /lemmon/renumber' now matches the web page step numbers. ('show proof xxx/renumber' still has the indented form conforming to the actual RPN proof, with slightly different numbering.)

(9-Sep-2010) The metamath program (version 0.07.51) was updated with a modification by Stefan Allan that adds hyperlinks the the Ref column of proofs.

(12-Jun-2010) Scott Fenton contributed a D-proof (directly from axioms) of Meredith's single axiom (see the end of pmproofs.txt). A description of Meredith's axiom can be found in theorem meredith.

(11-Jun-2010) A new Metamath mirror was added in Austria, courtesy of Kinder-Enduro.

(28-Feb-2010) Raph Levien's Ghilbert project now has a new Ghilbert site and a Google Group.

(26-Jan-2010) Dmitri Vlasov writes, "I admire the simplicity and power of the metamath language, but still I see its great disadvantage - the proofs in metamath are completely non-manageable by humans without proof assistants. Therefore I decided to develop another language, which would be a higher-level superstructure language towards metamath, and which will support human-readable/writable proofs directly, without proof assistants. I call this language mdl (acronym for 'mathematics development language')." The latest version of Dmitri's translators from metamath to mdl and back can be downloaded from http://mathdevlanguage.sourceforge.net/. Currently only Linux is supported, but Dmitri says is should not be difficult to port it to other platforms that have a g++ compiler.

(11-Sep-2009) The metamath program (version 0.07.48) has been updated to enforce the whitespace requirement of the current spec.

(10-Sep-2009) Matthew Leitch has written an nice article, "How to write mathematics clearly", that briefly mentions Metamath. Overall it makes some excellent points. (I have written to him about a few things I disagree with.)

(28-May-2009) AsteroidMeta is back on-line. Note the URL change.

(12-May-2009) Charles Greathouse wrote a Greasemonkey script to reformat the axiom list on Metamath web site proof pages. This is a beta version; he will appreciate feedback.

(11-May-2009) Stefan Allan modified the metamath program to add the command "show statement xxx /mnemonics", which produces the output file Mnemosyne.txt for use with the Mnemosyne project. The current Metamath program download incorporates this command. Instructions: Create the file mnemosyne.txt with e.g. "show statement ax-* /mnemonics". In the Mnemosyne program, load the file by choosing File->Import then file format "Q and A on separate lines". Notes: (1) Don't try to load all of set.mm, it will crash the program due to a bug in Mnemosyne. (2) On my computer, the arrows in ax-1 don't display. Stefan reports that they do on his computer. (Both are Windows XP.)

(3-May-2009) Steven Baldasty wrote a Metamath syntax highlighting file for the gedit editor. Screenshot.

(1-May-2009) Users on a gaming forum discuss our 2+2=4 proof. Notable comments include "Ew math!" and "Whoever wrote this has absolutely no life."

(12-Mar-2009) Chris Capel has created a Javascript theorem viewer demo that (1) shows substitutions and (2) allows expanding and collapsing proof steps. You are invited to take a look and give him feedback at his Metablog.

(28-Feb-2009) Chris Capel has written a Metamath proof verifier in C#, available at http://pdf23ds.net/bzr/MathEditor/Verifier/Verifier.cs and weighing in at 550 lines. Also, that same URL without the file on it is a Bazaar repository.

(2-Dec-2008) A new section was added to the Deduction Theorem page, called Logic, Metalogic, Metametalogic, and Metametametalogic.

(24-Aug-2008) (From ocat): The 1-Aug-2008 version of mmj2 is ready (mmj2.zip), size = 1,534,041 bytes. This version contains the Theorem Loader enhancement which provides a "sandboxing" capability for user theorems and dynamic update of new theorems to the Metamath database already loaded in memory by mmj2. Also, the new "mmj2 Service" feature enables calling mmj2 as a subroutine, or having mmj2 call your program, and provides access to the mmj2 data structures and objects loaded in memory (i.e. get started writing those Jython programs!) See also mmj2 on AsteroidMeta.

(23-May-2008) Gérard Lang pointed me to Bob Solovay's note on AC and strongly inaccessible cardinals. One of the eventual goals for set.mm is to prove the Axiom of Choice from Grothendieck's axiom, like Mizar does, and this note may be helpful for anyone wanting to attempt that. Separately, I also came across a history of the size reduction of grothprim (viewable in Firefox and some versions of Internet Explorer).

(14-Apr-2008) A "/join" qualifier was added to the "search" command in the metamath program (version 0.07.37). This qualifier will join the $e hypotheses to the $a or $p for searching, so that math tokens in the $e's can be matched as well. For example, "search *com* +v" produces no results, but "search *com* +v /join" yields commutative laws involving vector addition. Thanks to Stefan Allan for suggesting this idea.

(8-Apr-2008) The 8,000th theorem, hlrel, was added to the Metamath Proof Explorer part of the database.

(2-Mar-2008) I added a small section to the end of the Deduction Theorem page.

(17-Feb-2008) ocat has uploaded the "1-Mar-2008" mmj2: mmj2.zip. See the description.

(16-Jan-2008) O'Cat has written mmj2 Proof Assistant Quick Tips.

(30-Dec-2007) "How to build a library of formalized mathematics".

(22-Dec-2007) The Metamath Proof Explorer was included in the top 30 science resources for 2007 by the University at Albany Science Library.

(17-Dec-2007) Metamath's Wikipedia entry says, "This article may require cleanup to meet Wikipedia's quality standards" (see its discussion page). Volunteers are welcome. :) (In the interest of objectivity, I don't edit this entry.)

(20-Nov-2007) Jeff Hoffman created nicod.mm and posted it to the Google Metamath Group.

(19-Nov-2007) Reinder Verlinde suggested adding tooltips to the hyperlinks on the proof pages, which I did for proof step hyperlinks. Discussion.

(5-Nov-2007) A Usenet challenge. :)

(4-Aug-2007) I added a "Request for comments on proposed 'maps to' notation" at the bottom of the AsteroidMeta set.mm discussion page.

(21-Jun-2007) A preprint (PDF file) describing Kurt Maes' axiom of choice with 5 quantifiers, proved in set.mm as ackm.

(20-Jun-2007) The 7,000th theorem, ifpr, was added to the Metamath Proof Explorer part of the database.

(29-Apr-2007) Blog mentions of Metamath: here and here.

(21-Mar-2007) Paul Chapman is working on a new proof browser, which has highlighting that allows you to see the referenced theorem before and after the substitution was made. Here is a screenshot of theorem 0nn0 and a screenshot of theorem 2p2e4.

(15-Mar-2007) A picture of Penny the cat guarding the us.metamath.org server and making the rounds.

(16-Feb-2007) For convenience, the program "drule.c" (pronounced "D-rule", not "drool") mentioned in pmproofs.txt can now be downloaded (drule.c) without having to ask me for it. The same disclaimer applies: even though this program works and has no known bugs, it was not intended for general release. Read the comments at the top of the program for instructions.

(28-Jan-2007) Jason Orendorff set up a new mailing list for Metamath: http://groups.google.com/group/metamath.

(20-Jan-2007) Bob Solovay provided a revised version of his Metamath database for Peano arithmetic, peano.mm.

(2-Jan-2007) Raph Levien has set up a wiki called Barghest for the Ghilbert language and software.

(26-Dec-2006) I posted an explanation of theorem ecoprass on Usenet.

(2-Dec-2006) Berislav Žarnić translated the Metamath Solitaire applet to Croatian.

(26-Nov-2006) Dan Getz has created an RSS feed for new theorems as they appear on this page.

(6-Nov-2006) The first 3 paragraphs in Appendix 2: Note on the Axioms were rewritten to clarify the connection between Tarski's axiom system and Metamath.

(31-Oct-2006) ocat asked for a do-over due to a bug in mmj2 -- if you downloaded the mmj2.zip version dated 10/28/2006, then download the new version dated 10/30.

(29-Oct-2006) ocat has announced that the long-awaited 1-Nov-2006 release of mmj2 is available now.
     The new "Unify+Get Hints" is quite useful, and any proof can be generated as follows. With "?" in the Hyp field and Ref field blank, select "Unify+Get Hints". Select a hint from the list and put it in the Ref field. Edit any $n dummy variables to become the desired wffs. Rinse and repeat for the new proof steps generated, until the proof is done.
     The new tutorial, mmj2PATutorial.bat, explains this in detail. One way to reduce or avoid dummy $n's is to fill in the Hyp field with a comma-separated list of any known hypothesis matches to earlier proof steps, keeping a "?" in the list to indicate that the remaining hypotheses are unknown. Then "Unify+Get Hints" can be applied. The tutorial page \mmj2\data\mmp\PATutorial\Page405.mmp has an example.
     Don't forget that the eimm export/import program lets you go back and forth between the mmj2 and the metamath program proof assistants, without exiting from either one, to exploit the best features of each as required.

(21-Oct-2006) Martin Kiselkov has written a Metamath proof verifier in the Lua scripting language, called verify.lua. While it is not practical as an everyday verifier - he writes that it takes about 40 minutes to verify set.mm on a a Pentium 4 - it could be useful to someone learning Lua or Metamath, and importantly it provides another independent way of verifying the correctness of Metamath proofs. His code looks like it is nicely structured and very readable. He is currently working on a faster version in C++.

(19-Oct-2006) New AsteroidMeta page by Raph, Distinctors_vs_binders.

(13-Oct-2006) I put a simple Metamath browser on my PDA (Palm Tungsten E) so that I don't have to lug around my laptop. Here is a screenshot. It isn't polished, but I'll provide the file + instructions if anyone wants it.

(3-Oct-2006) A blog entry, Principia for Reverse Mathematics.

(28-Sep-2006) A blog entry, Metamath responds.

(26-Sep-2006) A blog entry, Metamath isn't hygienic.

(11-Aug-2006) A blog entry, Metamath and the Peano Induction Axiom.

(26-Jul-2006) A new open problem in predicate calculus was added.

(18-Jun-2006) The 6,000th theorem, mt4d, was added to the Metamath Proof Explorer part of the database.

(9-May-2006) Luca Ciciriello has upgraded the t2mf program, which is a C program used to create the MIDI files on the Metamath Music Page, so that it works on MacOS X. This is a nice accomplishment, since the original program was written before C was standardized by ANSI and will not compile on modern compilers.
Unfortunately, the original program source states no copyright terms. The main author, Tim Thompson, has kindly agreed to release his code to public domain, but two other authors have also contributed to the code, and so far I have been unable to contact them for copyright clearance. Therefore I cannot offer the MacOS X version for public download on this site until this is resolved. Update 10-May-2006: Another author, M. Czeiszperger, has released his contribution to public domain.
If you are interested in Luca's modified source code, please contact me directly.

(18-Apr-2006) Incomplete proofs in progress can now be interchanged between the Metamath program's CLI Proof Assistant and mmj2's GUI Proof Assistant, using a new export-import program called eimm. This can be done without exiting either proof assistant, so that the strengths of each approach can be exploited during proof development. See "Use Case 5a" and "Use Case 5b" at mmj2ProofAssistantFeedback.

(28-Mar-2006) Scott Fenton updated his second version of Metamath Solitaire (the one that uses external axioms). He writes: "I've switched to making it a standalone program, as it seems silly to have an applet that can't be run in a web browser. Check the README file for further info." The download is mmsol-0.5.tar.gz.

(27-Mar-2006) Scott Fenton has updated the Metamath Solitaire Java applet to Java 1.5: (1) QSort has been stripped out: its functionality is in the Collections class that Sun ships; (2) all Vectors have been replaced by ArrayLists; (3) generic types have been tossed in wherever they fit: this cuts back drastically on casting; and (4) any warnings Eclipse spouted out have been dealt with. I haven't yet updated it officially, because I don't know if it will work with Microsoft's JVM in older versions of Internet Explorer. The current official version is compiled with Java 1.3, because it won't work with Microsoft's JVM if it is compiled with Java 1.4. (As distasteful as that seems, I will get complaints from users if it doesn't work with Microsoft's JVM.) If anyone can verify that Scott's new version runs on Microsoft's JVM, I would be grateful. Scott's new version is mm.java-1.5.gz; after uncompressing it, rename it to mm.java, use it to replace the existing mm.java file in the Metamath Solitaire download, and recompile according to instructions in the mm.java comments.
Scott has also created a second version, mmsol-0.2.tar.gz, that reads the axioms from ASCII files, instead of having the axioms hard-coded in the program. This can be very useful if you want to play with custom axioms, and you can also add a collection of starting theorems as "axioms" to work from. However, it must be run from the local directory with appletviewer, since the default Java security model doesn't allow reading files from a browser. It works with the JDK 5 Update 6 Java download.
To compile (from Windows Command Prompt): C:\Program Files\Java\jdk1.5.0_06\bin\javac.exe mm.java
To run (from Windows Command Prompt): C:\Program Files\Java\jdk1.5.0_06\bin\appletviewer.exe mms.html

(21-Jan-2006) Juha Arpiainen proved the independence of axiom ax-11 from the others. This was published as an open problem in my 1995 paper (Remark 9.5 on PDF page 17). See Item 9a on the Workshop Miscellany for his seven-line proof. See also the Asteroid Meta metamathMathQuestions page under the heading "Axiom of variable substitution: ax-11". Congratulations, Juha!

(20-Oct-2005) Juha Arpiainen is working on a proof verifier in Common Lisp called Bourbaki. Its proof language has its roots in Metamath, with the goal of providing a more powerful syntax and definitional soundness checking. See its documentation and related discussion.

(17-Oct-2005) Marnix Klooster has written a Metamath proof verifier in Haskell, called Hmm. Also see his Announcement. The complete program (Hmm.hs, HmmImpl.hs, and HmmVerify.hs) has only 444 lines of code, excluding comments and blank lines. It verifies compressed as well as regular proofs; moreover, it transparently verifies both per-spec compressed proofs and the flawed format he uncovered (see comment below of 16-Oct-05).

(16-Oct-2005) Marnix Klooster noticed that for large proofs, the compressed proof format did not match the spec in the book. His algorithm to correct the problem has been put into the Metamath program (version 0.07.6). The program still verifies older proofs with the incorrect format, but the user will be nagged to update them with 'save proof *'. In set.mm, 285 out of 6376 proofs are affected. (The incorrect format did not affect proof correctness or verification, since the compression and decompression algorithms matched each other.)

(13-Sep-2005) Scott Fenton found an interesting axiom, ax46, which could be used to replace both ax-4 and ax-6.

(29-Jul-2005) Metamath was selected as site of the week by American Scientist Online.

(8-Jul-2005) Roy Longton has contributed 53 new theorems to the Quantum Logic Explorer. You can see them in the Theorem List starting at lem3.3.3lem1. He writes, "If you want, you can post an open challenge to see if anyone can find shorter proofs of the theorems I submitted."

(10-May-2005) A Usenet post I posted about the infinite prime proof; another one about indexed unions.

(3-May-2005) The theorem divexpt is the 5,000th theorem added to the Metamath Proof Explorer database.

(12-Apr-2005) Raph Levien solved the open problem in item 16 on the Workshop Miscellany page and as a corollary proved that axiom ax-9 is independent from the other axioms of predicate calculus and equality. This is the first such independence proof so far; a goal is to prove all of them independent (or to derive any redundant ones from the others).

(8-Mar-2005) I added a paragraph above our complex number axioms table, summarizing the construction and indicating where Dedekind cuts are defined. Thanks to Andrew Buhr for comments on this.

(16-Feb-2005) The Metamath Music Page is mentioned as a reference or resource for a university course called Math, Mind, and Music. .

(28-Jan-2005) Steven Cullinane parodied the Metamath Music Page in his blog.

(18-Jan-2005) Waldek Hebisch upgraded the Metamath program to run on the AMD64 64-bit processor.

(17-Jan-2005) A symbol list summary was added to the beginning of the Hilbert Space Explorer Home Page. Thanks to Mladen Pavicic for suggesting this.

(6-Jan-2005) Someone assembled an amazon.com list of some of the books in the Metamath Proof Explorer Bibliography.

(4-Jan-2005) The definition of ordinal exponentiation was decided on after this Usenet discussion.

(19-Dec-2004) A bit of trivia: my Erdös number is 2, as you can see from this list.

(20-Oct-2004) I started this Usenet discussion about the "reals are uncountable" proof (127 comments; last one on Nov. 12).

(12-Oct-2004) gch-kn shows the equivalence of the Generalized Continuum Hypothesis and Prof. Nambiar's Axiom of Combinatorial Sets. This proof answers his Open Problem 2 (PDF file).

(5-Aug-2004) I gave a talk on "Hilbert Lattice Equations" at the Argonne workshop.

(25-Jul-2004) The theorem nthruz is the 4,000th theorem added to the Metamath Proof Explorer database.

(27-May-2004) Josiah Burroughs contributed the proofs u1lemn1b, u1lem3var1, oi3oa3lem1, and oi3oa3 to the Quantum Logic Explorer database ql.mm.

(23-May-2004) Some minor typos found by Josh Purinton were corrected in the Metamath book. In addition, Josh simplified the definition of the closure of a pre-statement of a formal system in Appendix C.

(5-May-2004) Gregory Bush has found shorter proofs for 67 of the 193 propositional calculus theorems listed in Principia Mathematica, thus establishing 67 new records. (This was challenge #4 on the open problems page.)

W3C HTML validation [external]