Triangle centres in Lean 4 the Nagel line family and the symmedian and Brocard points

We give machine-checked proofs, in Lean 4 with Mathlib, of classical theorems about twofamilies of triangle centres. For the first family we define the Nagel and Gergonne points by theirbarycentric weights and prove that they are the common points of the cevians to the excircleand incircle contact points, where the contact points are Mathlib’s touchpoints. We prove theNagel line relation N − G = 2(G − I) with Mathlib’s incentre and centroid, that the Spiekercentre (the incentre of Mathlib’s medial triangle) is the midpoint of I and N, that the Nagelpoint of the medial triangle is I, that the incircle and excircle contact points on each side aresymmetric about its midpoint, that N is the incentre of the anticomplementary triangle, thatthe de Longchamps point lies on the Euler line and is the orthocentre of the anticomplementarytriangle, and that the Spieker centre has equal power with respect to the three excircles. For thesecond family we prove that the point with barycentrics a2 : b2 : c2 lies on the three symmedians(six angle equalities) and inside the triangle, that it is the centroid of its pedal triangle and, inthe plane, the only such point, that the two Brocard points satisfy their angle equalities, that theBrocard angle ω satisfies cotω = cotA+cotB +cotC = (a2 +b2 +c2)/(4∆) and 0 < ω ≤ π/6,that the Brocard points satisfy the three isogonality angle equalities and are equidistant from thecircumcentre, that O, K and both Brocard points lie on the circle with diameter OK (whichdegenerates exactly for equilateral triangles), that the six points of Lemoine’s first circle areconcyclic, and the Droz-Farny line theorem. Apart from the pedal-centroid converse and DrozFarny, no numbered theorem assumes that the ambient space is a plane. All proofs use onlyLean’s three standard axioms. In the sources we searched, subject to stated gaps, we foundno earlier formal proof of these statements; one earlier Lean file proves an algebraic form ofthe Nagel and Gergonne cevian statements, and an earlier Coq development verifies barycentricforms of the Nagel line, the Spieker centre’s position and two related facts.