The Malfatti circles in Lean 4, with independent certificate proofs of Feuerbach, Miquel and Brahmagupta

We formalise four classical theorems about circles in Lean~4 with Mathlib. Only one of them,the Malfatti circle construction, is to our knowledge formalised here for the first time; the otherthree have earlier formal proofs and are offered as independent formalisations. \emph{Feuerbach'stheorem} (number~29 on Wiedijk's list of 100 theorems): the nine-point circle of a triangle isinternally tangent to the incircle and externally tangent to the three excircles, stated withMathlib's own \mdecl{Affine.Simplex.insphere}, \mdecl{Affine.Simplex.exsphere},\mdecl{Affine.Simplex.ninePointCircle} and tangency predicates, together with Euler's formula$OI^2=R(R-2r)$, its excentral analogue and Euler's inequality $2r\le R$. \emph{Miquel's theorem}:for points on the three (extended) sides of a triangle, none at a vertex, the three Miquel circlespass through a common point. \emph{Brahmagupta's formula}: a convex cyclic quadrilateral withsides $a,b,c,d$ has (shoelace) area $\sqrt{(s-a)(s-b)(s-c)(s-d)}$, the formal hypotheses alsoadmitting some collapsed configurations for which the formula holds trivially, derived from Mathlib's Ptolemy theoremthrough the diagonal form of Bretschneider's formula, which we prove for every quadrilateral.\emph{The Malfatti circles}: every triangle in the Euclidean plane has three circles of positiveradius, each tangent to the two sides through one vertex and any two externally tangent, withMalfatti's radius formula $\rho_A=\frac{r}{2(s-a)}\bigl(s-r-(IB+IC-IA)\bigr)$; this is theconstruction, \emph{not} Malfatti's conjecture that these circles maximise the total area, whichGoldberg disproved in 1967~\cite{Goldberg}.In each case the core is an explicit polynomial identity closed by \lean{ring} or\lean{linear\_combination}. The four libraries use no \lean{sorry} and depend only on Lean's threestandard axioms; each passes an axiom gate, a tamper test and a further battery of statement-levelchecks. All four libraries were also rebuilt on a second machine of a different architecture(arm64/macOS).\textbf{Feuerbach's theorem is not new to Lean:} Weiyi Wang has a sorry-free standalone Leanrepository (January 2026) and an open Mathlib pull request (\#44236, created 26 September 2026).Our Feuerbach development is an independent second formalisation, and we claim no priority forit. \textbf{Miquel's theorem is not new to formal mathematics either:} it was formalised inIsabelle/HOL in the Archive of Formal Proofs entry of Freitas Ramos, Barros Hulak and de~Queiroz(August 2026), and earlier in Coq's HighSchoolGeometry library. Our Miquel statement differs inassuming only the non-degeneracy conditions that make the three circles exist.\textbf{Brahmagupta's formula is not new to Lean:} a complete, sorry-free Lean~4 proof is in theShadowBench repository (\texttt{epfl-lara/icml-26-lean-challenges}, commit of 12 June 2026). Whatour Brahmagupta development adds is limited to statements we did not find there: theinequality $K^2\le(s-a)(s-b)(s-c)(s-d)$ and the equivalence of equality with Ptolemy's equality,both for arbitrary four points. For the Malfatti circle construction we found no earlierformalisation; our searches are not exhaustive, and three of the four searches missed existingwork. The new contributions are therefore the Malfatti formalisation, a second Lean proof ofFeuerbach's theorem, a Miquel statement with fewer hypotheses than the earlier ones, and theverification methodology with its limits.