Anthropic uses Claude to formalize proof of Fermat’s Last Theorem
Anthropic PBC has used Claude to create a computer-verifiable version of a famous, highly complicated mathematical proof.
The company detailed the project in a blog post published today.
A proof is a series of arguments that proves a mathematical hypothesis is correct. The proof that Anthropic tackled verifies a hypothesis called Fermat’s Last Theorem. Originally floated in 1637, the hypothesis focuses on the properties of positive whole numbers.
The proof of Fermat’s Last Theorem was developed in 1995 by mathematician Andrew Wiles. It runs for 129 pages and took months of work to verify. Anthropic’s research project formalized Wiles’ proof, which means that the company turned it into a form that can be automatically verified by computers. Formalizing proofs is useful because it rules out the possibility of human error and eases information sharing among mathematicians.
