Dandelin spheres and Marden's theorem, formalised in Lean 4

We formalise two classical theorems about conics in Lean 4 with Mathlib. The first isDandelin’s theorem. A plane that misses the apex of a right circular cone meets it in an ellipse,a parabola or a hyperbola. The spheres inscribed in the cone and tangent to the plane touch it atthe foci. In three-dimensional space we prove the classical picture: among the spheres centred onthe axis and touching the cone, exactly two are tangent to the plane in the ellipse and hyperbolacases and exactly one in the parabola case; the section is exactly the locus of constant focal sum(ellipse) or constant absolute focal difference (hyperbola, on the double cone); for non-circularsections the focus–directrix property holds with eccentricity e = cos β/ cos α, together with itsconverse; the section is non-empty; the three regimes are characterised geometrically; and theplanes through the apex give a point, a line or two lines. The focal identities and their converseshold in an arbitrary real inner product space; non-emptiness, the regime characterisations andthe two-line apex section are proved under explicit finite-dimension assumptions. The secondis Marden’s theorem. For a non-degenerate triangle a, b, c ∈ C, the ellipse whose foci are thecritical points of (z−a)(z−b)(z−c) passes through the midpoints of the sides, touches each sideonly there, and has the centroid as its centre. We also prove that it is the only ellipse, given byfoci and focal sum, with this property. Tangency is stated metrically, and we explain why thisis the right notion. The developments have about 2170 and 760 lines. They contain no sorry,and their main theorems depend only on Lean’s standard axioms. We found no earlier completeformalisation of either theorem in the sources we searched; Section 6 records the scope of thatsearch and one unresolved lead.