Classical plane geometry by coordinate certificates: Desargues, Monge, Simson, Napoleon and Lami in Lean 4
Abstract
We formalise five classical theorems of plane geometry in Lean 4 with Mathlib: Desargues’s
theorem in the projective plane, together with its converse; Monge’s theorem that the three
external centres of similitude of three circles are collinear; the Wallace–Simson theorem on
the pedal triangle of a point of the circumcircle; Napoleon’s theorem for the outer and the
inner Napoleon triangles; and Lami’s theorem for three forces in equilibrium. Every proof
has the same core. The theorem is reduced to an explicit polynomial or rational identity in
coordinates, which we call a certificate, and the identity is closed by ring, field_simp or
linear_combination with a stated multiplier. Around this core, each development makes
precise which non-degeneracy conditions are needed, which are not, and why. Desargues’s
theorem and Monge’s theorem are proved over an arbitrary field, and the Desargues identity
over an arbitrary commutative ring. The Simson line and Napoleon’s theorem are proved in the
Euclidean plane, modelled as C. Lami’s theorem is proved through the oriented area form of a
two-dimensional oriented real inner product space, and in unoriented form in every real inner
product space. The five libraries, without the version-2 files described next, have about 1,430
lines of Lean, use no sorry, and depend only on Lean’s three standard axioms. Version 2 adds
to each library a file giving Mathlib-only formulations of the main theorems (for Napoleon’s
theorem, of its non-degenerate configurations), each with a non-degenerate witness, and a file
proving from the libraries textbook statements written in Lean by an AI model that saw neither
our code nor this paper; these include the geometric converse of the Wallace–Simson theorem,
which the first version did not prove. The mathematics is classical and the method is old,
and several of the results are not new to formal mathematics (Section 9). Monge’s three-circle
theorem has two earlier, independent and complete Lean proofs, one of which predates ours by
four months; Napoleon’s theorem has earlier formalisations in Lean, Isabelle and Rocq, and a
later independent one in Lean; the Wallace–Simson theorem and its converse are formalised in
Isabelle and in Rocq; Desargues’s theorem is formalised in at least five other systems, including a
coordinate (bracket) proof in HOL Light; and an open, unmerged Mathlib pull request proves the
affine (parallel) form of Desargues’s theorem. We found no earlier Lean proof of the projective
plane form of Desargues’s theorem, of the Wallace–Simson theorem, or of Lami’s theorem; these
searches are not exhaustive.
Related
- τ8: an Angle-Based Geometry Index for 8-Coordinate Complexes
- Cell geometry and mechanical stress coordinate stomatal division orientation
- Recovery Witnesses for Suzuki's Screw Function: Service-Clock Geometry and Episode-Minimum Certificates — Part 4
- Boundary Geometry and Global Rates of Cyclic Coordinate Descent for SVM Duals
- Physics-informed coordinate-mapping categorizations for deciphering pore geometry and seepage capacity in oil shales
BibTeX
@misc{bald2026classical,
title = {{Classical plane geometry by coordinate certificates: Desargues, Monge, Simson, Napoleon and Lami in Lean 4}},
author = {Joshua Bald},
howpublished = {Zenodo},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23653175},
url = {https://zenodo.org/records/23653175},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Classical plane geometry by coordinate certificates: Desargues, Monge, Simson, Napoleon and Lami in Lean 4
AU - Joshua Bald
PY - 2026
DA - 2026/10/26
PB - Zenodo
DO - 10.5281/zenodo.23653175
UR - https://zenodo.org/records/23653175
AB - We formalise five classical theorems of plane geometry in Lean 4 with Mathlib: Desargues’s theorem in the projective plane, together with its converse; Monge’s theorem that the three external centres of similitude of three circles are collinear; the Wallace–Simson theorem on the pedal triangle of a point of the circumcircle; Napoleon’s theorem for the outer and the inner Napoleon triangles; and Lami’s theorem for three forces in equilibrium. Every proof has the same core. The theorem is reduced to an explicit polynomial or rational identity in coordinates, which we call a certificate, and the identity is closed by ring, field_simp or linear_combination with a stated multiplier. Around this core, each development makes precise which non-degeneracy conditions are needed, which are not, and why. Desargues’s theorem and Monge’s theorem are proved over an arbitrary field, and the Desargues identity over an arbitrary commutative ring. The Simson line and Napoleon’s theorem are proved in the Euclidean plane, modelled as C. Lami’s theorem is proved through the oriented area form of a two-dimensional oriented real inner product space, and in unoriented form in every real inner product space. The five libraries, without the version-2 files described next, have about 1,430 lines of Lean, use no sorry, and depend only on Lean’s three standard axioms. Version 2 adds to each library a file giving Mathlib-only formulations of the main theorems (for Napoleon’s theorem, of its non-degenerate configurations), each with a non-degenerate witness, and a file proving from the libraries textbook statements written in Lean by an AI model that saw neither our code nor this paper; these include the geometric converse of the Wallace–Simson theorem, which the first version did not prove. The mathematics is classical and the method is old, and several of the results are not new to formal mathematics (Section 9). Monge’s three-circle theorem has two earlier, independent and complete Lean proofs, one of which predates ours by four months; Napoleon’s theorem has earlier formalisations in Lean, Isabelle and Rocq, and a later independent one in Lean; the Wallace–Simson theorem and its converse are formalised in Isabelle and in Rocq; Desargues’s theorem is formalised in at least five other systems, including a coordinate (bracket) proof in HOL Light; and an open, unmerged Mathlib pull request proves the affine (parallel) form of Desargues’s theorem. We found no earlier Lean proof of the projective plane form of Desargues’s theorem, of the Wallace–Simson theorem, or of Lami’s theorem; these searches are not exhaustive.
ER -