Classical plane geometry by coordinate certificates: Desargues, Monge, Simson, Napoleon and Lami in Lean 4

We formalise five classical theorems of plane geometry in Lean 4 with Mathlib: Desargues’stheorem in the projective plane, together with its converse; Monge’s theorem that the threeexternal centres of similitude of three circles are collinear; the Wallace–Simson theorem on thepedal triangle of a point of the circumcircle; Napoleon’s theorem for the outer and the innerNapoleon triangles; and Lami’s theorem for three forces in equilibrium. Every proof has the samecore. The theorem is reduced to an explicit polynomial or rational identity in coordinates, whichwe call a certificate, and the identity is closed by ring, field_simp or linear_combination witha stated multiplier. Around this core, each development makes precise which non-degeneracyconditions are needed, which are not, and why. Desargues’s theorem and Monge’s theorem areproved 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 realinner product space, and in unoriented form in every real inner product space. The five librarieshave about 1,430 lines of Lean, use no sorry, and depend only on Lean’s three standard axioms.The mathematics is classical and the method is old, and several of the results are not new toformal mathematics (Section 9). Napoleon’s theorem has earlier formalisations in Lean, Isabelleand Rocq; 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 ofDesargues’s theorem, of the Wallace–Simson theorem, of Monge’s three-circle theorem, or ofLami’s theorem.