Five classical theorems on triangles and simplices, formalised in Lean 4 with Mathlib: Carnot, Viviani, De Gua, the Japanese theorem and Poncelet's porism

We report Lean 4 formalisations, built on Mathlib, of five classical results of elementarygeometry: Carnot’s theorem Pi di(O) = R + r for a triangle; Viviani’s theorem, generalised tosimplices of every positive dimension as the identityPi di(p)/hi = 1; De Gua’s theorem in everydimension, for simplices whose edges at one vertex are pairwise orthogonal, together with theprojection form obtained from a self-contained proof of the Cauchy–Binet formula; the Japanesetheorem for convex cyclic polygons, for all triangulations by maximal sets of non-crossing diagonals;and Poncelet’s porism for triangles, with its converse, in the “construction” form. Thedevelopments follow two strands. Viviani, Carnot and the Japanese theorem are statementsabout signed distances to the facets of a simplex, equivalently barycentric coordinates, andPoncelet’s porism rests on the same incentre and excentre vocabulary together with circle tangency;here Mathlib’s Affine.Simplex API (signedInfDist, height, incenter, excenter,circumcenter) supplies most of what is needed. De Gua’s theorem belongs to a second strand,Gram determinants of edge vectors. We state every hypothesis exactly, explain why each ispresent, and give lemmas that tie the formal definitions to the familiar informal ones. Togetherthe developments have about 3 200 lines of new Lean code (plus about 900 lines of verbatimcopies), with no sorry and only Lean’s standard axioms. As far as we could determine, the geometricsigned-distance formulation of Carnot’s theorem, the n-dimensional Viviani and De Guatheorems in this form, the Japanese theorem and Poncelet’s porism have no earlier completeLean formalisation; closely related Lean material does exist for the trigonometric identity underlyingCarnot’s theorem, for the three-dimensional De Gua theorem, for coordinate versionsof Viviani’s theorem and for the Cauchy–Binet formula, and we describe it in Section 9.