# Anthropic Formalized Fermat's Last Theorem in Lean, Shifting the Verification Challenge

DevFeed: [Anthropic Formalized Fermat's Last Theorem in Lean, Shifting the Verification Challenge](<https://devfeed.tech/articles/the-question-was-already-written-40147.md>)

Original publisher: [Read original article](<https://korbonits.com/blog/2026-09-06-the-question-was-already-written/>)

Published: 2026-09-06T00:00:00Z

Content type: opinion

Language: en

Sources: [Alex Korbonits](<https://devfeed.tech/sources/alex-korbonits.md>)

Topics: [Lean](<https://devfeed.tech/topics/lean.md>), [anthropic](<https://devfeed.tech/topics/anthropic.md>), [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>)

Tags: [anthropic](<https://devfeed.tech/tags/anthropic.md>), [compiler](<https://devfeed.tech/tags/compiler.md>), [formalized](<https://devfeed.tech/tags/formalized.md>), [research](<https://devfeed.tech/tags/research.md>), [statement](<https://devfeed.tech/tags/statement.md>), [trust](<https://devfeed.tech/tags/trust.md>)

## AI overview

The article argues that Anthropic's machine-generated Lean proof of Fermat's Last Theorem changes the challenge from formalizing the theorem's statement to checking a very large proof artifact. It describes public build checks and an independent Rust-based Lean kernel re-check, while noting that the author has not read the patches used to complete that re-check.

## Source excerpt

Anthropic formalized Fermat's Last Theorem in Lean in eleven days. It is the frontier I said in May was untouched, and the first result in this series where nobody had to trust the statement. The problem that replaced it is that 13 million lines is more than anyone can read.