Classical triangle inequalities and the Fermat–Napoleon configuration in Lean 4

We give machine-checked proofs, in Lean 4 with Mathlib, of a body of classical inequalitiesand extremal theorems for the triangle, together with the Fermat–Napoleon configuration. Foran arbitrary Affine.Triangle in a real inner product space of any dimension, using Mathlib’sown circumcentre, circumradius, incentre, inradius, excentres, exradii, centroid and orthocentre,we prove Euler’s relation OI2 = R2 − 2Rr, Euler’s inequality R ≥ 2r with its equality case(equality exactly for equilateral triangles) and the excircle relation OI2a = R2 + 2Rra; theformulas OG2 = R2−(a2+b2+c2)/9, OH2 = 9R2−(a2+b2+c2) and IG2 = (s2+5r2−16Rr)/9;Gerretsen’s inequalities 16Rr − 5r2 ≤ s2 ≤ 4R2 + 4Rr + 3r2 and Kooi’s sharper upper bound;the Weitzenböck, Hadwiger–Finsler and triangle isoperimetric inequalities with their equalitycases; the Leibniz relation and the minimality of |XAi|2 at the centroid; and the NeubergPedoe inequality for two triangles with equality exactly for similar triangles. We characterisethe equality case of Ptolemy’s inequality in any real inner product space (concyclic points inseparated order, or collinear points in one of eight orders). For a point X of the closed trianglewe prove the Erdős–Mordell inequality, its key lemma and its equality case (equilateral triangle,X the centre), and, for interior points, Barrow’s inequality. If every angle is less than 2π/3,the Fermat–Torricelli point exists and minimises XA+XB +XC over the whole space. In theoriented plane we prove that the segments AA′, BB′, CC′ to the apexes of the outer equilateraltriangles have equal lengths and lie on concurrent lines meeting pairwise at angle π/3, that ifevery angle is less than 2π/3 the common point is the Fermat point F and AA′ = FA+FB+FC,and Napoleon’s theorem with the centroid statement. All proofs use only Lean’s three standardaxioms. Several of these results were formalised before us, and we reprove them independently:Euler’s relation, Euler’s inequality and the excircle relation (two Lean developments, one ofthem an open Mathlib pull request), Ptolemy’s inequality (in Mathlib since 2022), the ErdősMordell inequality and its key lemma (two Lean developments, for interior points in the plane),algebraic forms of Weitzenböck and Hadwiger–Finsler, and Napoleon’s theorem (Isabelle andseveral Lean developments, including our own earlier one). For the remaining statements wefound no earlier formal proof in the sources we searched, subject to stated gaps.