The complete quadrilateral in Lean 4: Newton–Gauss, Bodenmiller, the Miquel point, the Steiner circle and the Simson line

Four lines in general position form a complete quadrilateral: six vertices, three diagonals, andfour triangles, one for each line omitted. We give machine-checked proofs, in Lean 4 with Mathlib, of eight classical theorems about this configuration, all from the single hypothesis that thelines are in general position. On the side of the diagonals: the midpoints of the three diagonalsare collinear (the Newton–Gauss line); the orthocentres of the four triangles are collinear; everyorthocentre has equal power with respect to the three circles on the diagonals as diameters (theGauss–Bodenmiller theorem); and the line of the orthocentres is perpendicular to the NewtonGauss line. On the side of the circles: the circumcircles of the four triangles pass through acommon point M, given by an explicit formula (the Miquel point); the four circumcentres andM lie on one circle (the Steiner, or Miquel, circle); the feet of the perpendiculars from M to thefour lines are collinear (the Simson line of the quadrilateral); and that line is parallel to the lineof the four orthocentres, as Mathlib affine subspaces. The two halves are separate developmentsthat share one file of definitions. We also show that two of the four orthocentres can coincide ingeneral position (two of them coincide exactly when two of the lines are perpendicular), so theorthocentre line is determined only because the four are never all equal, which we prove. Thelocal definitions (line, intersection, circumcentre, orthocentre, foot of a perpendicular, powerof a point, general position) are proved equal to Mathlib’s. All proofs use only Lean’s threestandard axioms. In the sources we searched, the Newton–Gauss line and the four-line Miqueltheorem already have formal proofs (in HOL Light and Rocq); we found none of the other sixin any system, and none of the eight in Lean.