Circle configurations in classical plane geometry, formalized in Lean 4: Clifford's chain, Miquel's five circles, Lester, Sawayama–Thébault and Kosnita

We give machine-checked proofs, in Lean 4 with Mathlib, of a family of classical theoremsabout configurations of circles in the Euclidean plane. The centrepiece is the beginning ofClifford’s chain: for four circles through a common point in general position, the four circlesthrough triples of their second intersection points have a common point (the case n = 4); forfive such circles the five points so obtained lie on one circle or one line (the case n = 5); and,under a stated further non-degeneracy condition, for six circles the six circles so obtained have acommon point (the case n = 6). We also prove Miquel’s five-circles theorem for the pentagram(again with the conclusion “on a circle or on a line”), Lester’s theorem that the circumcentre, thenine-point centre and the two Fermat points of a scalene triangle are concyclic, the SawayamaThébault theorem on the centres of the two Thébault circles and the incentre, and Kosnita’sconcurrence theorem; and, as two short companions in the same style, Blundon’s inequalitiesand the Steiner–Lehmus theorem. Every degenerate configuration that a statement excludes isnamed, and for several exclusions we exhibit configurations showing that the hypothesis cannotsimply be dropped. All proofs use only Lean’s three standard axioms. In the sources and searchscope listed in Section 10 we found no previous complete formal proof of any of these theorems,with one partial exception: the algebraic core of Steiner–Lehmus (over side lengths, with thebisector length given by its formula) has a Lean proof, and we found no formal proof of thegeometric theorem. The formal proofs we found closest to the circle theorems are of the threecircle Miquel theorem, which is the base case of Clifford’s chain. We also show, with an explicitsix-circle configuration, that the natural finite-plane formalization of the chain is false for everyn ≥6: its Clifford point lies at infinity.