{
  "abstract": "We formalise five classical theorems of plane geometry in Lean 4 with Mathlib: Desargues’s\n\ntheorem in the projective plane, together with its converse; Monge’s theorem that the three\n\nexternal centres of similitude of three circles are collinear; the Wallace–Simson theorem on\n\nthe pedal triangle of a point of the circumcircle; Napoleon’s theorem for the outer and the\n\ninner Napoleon triangles; and Lami’s theorem for three forces in equilibrium. Every proof\n\nhas the same core. The theorem is reduced to an explicit polynomial or rational identity in\n\ncoordinates, which we call a certificate, and the identity is closed by ring, field_simp or\n\nlinear_combination with a stated multiplier. Around this core, each development makes\n\nprecise which non-degeneracy conditions are needed, which are not, and why. Desargues’s\n\ntheorem and Monge’s theorem are proved over an arbitrary field, and the Desargues identity\n\nover an arbitrary commutative ring. The Simson line and Napoleon’s theorem are proved in the\n\nEuclidean plane, modelled as C. Lami’s theorem is proved through the oriented area form of a\n\ntwo-dimensional oriented real inner product space, and in unoriented form in every real inner\n\nproduct space. The five libraries, without the version-2 files described next, have about 1,430\n\nlines of Lean, use no sorry, and depend only on Lean’s three standard axioms. Version 2 adds\n\nto each library a file giving Mathlib-only formulations of the main theorems (for Napoleon’s\n\ntheorem, of its non-degenerate configurations), each with a non-degenerate witness, and a file\n\nproving from the libraries textbook statements written in Lean by an AI model that saw neither\n\nour code nor this paper; these include the geometric converse of the Wallace–Simson theorem,\n\nwhich the first version did not prove. The mathematics is classical and the method is old,\n\nand several of the results are not new to formal mathematics (Section 9). Monge’s three-circle\n\ntheorem has two earlier, independent and complete Lean proofs, one of which predates ours by\n\nfour months; Napoleon’s theorem has earlier formalisations in Lean, Isabelle and Rocq, and a\n\nlater independent one in Lean; the Wallace–Simson theorem and its converse are formalised in\n\nIsabelle and in Rocq; Desargues’s theorem is formalised in at least five other systems, including a\n\ncoordinate (bracket) proof in HOL Light; and an open, unmerged Mathlib pull request proves the\n\naffine (parallel) form of Desargues’s theorem. We found no earlier Lean proof of the projective\n\nplane form of Desargues’s theorem, of the Wallace–Simson theorem, or of Lami’s theorem; these\n\nsearches are not exhaustive.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": null,
  "author_total": 1,
  "authors": [
    {
      "name": "Joshua Bald",
      "orcid": "0009-0002-1317-6489"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/6q9215zaa5ygc.bib",
  "cited_by": 0,
  "doi": "10.5281/zenodo.23653175",
  "fulltext_url": null,
  "id": "6q9215zaa5ygc",
  "issns": [],
  "landing_url": "https://zenodo.org/records/23653175",
  "language": "eng",
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": null,
  "native_subjects": [],
  "openalex": null,
  "pdf_url": "https://zenodo.org/api/records/23653175/files/Classical%20plane%20geometry%20by%20coordinate%20certificates%20%20Desargues,%20Monge,%20Simson,%20Napoleon%20and%20Lami%20in%20Lean%204.pdf/content",
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-26",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/6q9215zaa5ygc.ris",
  "sources": [
    {
      "first_seen": "2026-11-09T12:20:35Z",
      "native_id": "23653175",
      "source": "zenodo",
      "url": "https://zenodo.org/records/23653175"
    }
  ],
  "subjects": [],
  "title": "Classical plane geometry by coordinate certificates: Desargues, Monge, Simson, Napoleon and Lami in Lean 4",
  "title_text": "Classical plane geometry by coordinate certificates: Desargues, Monge, Simson, Napoleon and Lami in Lean 4",
  "type": "preprint",
  "updated_at": "2026-11-09T12:20:35Z",
  "url": "https://research.draconitic.com/paper/6q9215zaa5ygc",
  "venue": "Zenodo",
  "versions": []
}