Email Gateway (Jun 11 2026 at 15:56): Email Gateway (Jun 11 2026 at 15:56):From: Manuel Eberl <manuel@pruvisto.org>
Feuerbach's Theorem
by Lawrence C. Paulson
Feuerbach’s theorem is a classical result in Euclidean geometry about
certain circles associated with a triangle. It states that the
nine-point circle is tangent internally to the triangle’s incircle and
tangent externally to each of the three excircles, where the /incircle/
is the circle tangent to all three sides of the triangle; the
/excircles/ are circles tangent to one side and the extensions of the
other two; the /nine-point circle/ is the circle passing through nine
special points of the triangle. This development is an experiment in
automatic translation from one proof assistant to another using AI.
The file feuerbach.ml was given, one proof at a time, to Claude 4.6
using the Isabelle Assistant <https://github.com/awslabs/AutoCorrode>
plug-in. Despite coaxing and hints, the auto formalisation process
transformed a 214-line HOL Light file to nearly 1500 lines of
Isabelle/HOL, though one that could be processed in five seconds. Part
of the excess length comes from spelling out two transformations
(translation of a point to zero, followed by rotation of a side to the
vector (1,0)) that in HOL Light is done silently by WLOG tactics. The
current proof has been heavily simplified, in part using Claude but
mostly manually, and is now under 750 lines. It is notable that Claude
often relied on the algebra proof method, despite its relative obscurity.
https://isa-afp.org/entries/Feuerbach.html
That's another one of Freek's Top 100 theorems down!
Enjoy,
Manuel
Last updated: Jun 12 2026 at 04:13 UTC