Kevin Buzzard Compiled Anthropic's FLT Proof and Confirms It Checks Out, While Saying It Adds 'Essentially Nothing' Mathematically

Xena Project (Kevin Buzzard) / Hacker News·high signalXBlueskyLinkedInCopy link

Imperial College's Kevin Buzzard, who runs the EPSRC-funded FLT formalization project, posted on September 4 that he compiled Anthropic's codebase and ran comparator on it, and it checks out. He also ran security checks, having an agent inspect the non-mathematical code and personally reviewing suspicious elements. His caveats matter for builders reading the announcement: the work uses the 1995 Darmon-Diamond-Taylor approach rather than modern methods, covers exponents p≥17 (sufficient, since smaller irregular primes were already formalized), and faithfully transcribes existing literature rather than proving anything new.