Casey's theorem and Fuss's theorem, formalised in Lean 4 with Mathlib

We report two small Lean 4 formalisations, built on Mathlib, of classical theorems aboutcircles. The first is Casey’s theorem (1866), the generalisation of Ptolemy’s theorem in which thefour points on a circle Γ are replaced by four circles tangent to Γ and distances are replaced bylengths of common tangents. We prove it in every real inner product space, for circles internallytangent to Γ and, through a signed radius, for any mixture of internally and externally tangentcircles; with all radii zero it specialises to Mathlib’s Ptolemy theorem, which the proof reuses.The second is Fuss’s theorem (1798): if a quadrilateral is inscribed in a circle of radius R andits four side lines are tangent to a circle of radius r whose centre is at distance d̸ = R from thefirst centre, with r > 0, then (R2 − d2)2 = 2r2(R2 + d2). We prove it in a Euclidean plane,together with the converse in the form of Poncelet’s porism for quadrilaterals: under Fuss’srelation every non-stalling four-step chain of the tangent construction (with the hypotheses ofTheorem 9) closes, and if the inner circle lies inside the outer one, every point of the outer circleis a vertex of such a quadrilateral. Both developments are short (about 200 and 870 lines),contain no sorry and use only Lean’s standard axioms. As far as we could determine, neithertheorem had a formal proof before