A new development in mathematics has emerged, thanks to an advanced version of the artificial intelligence (AI) model called Claude, developed by the company Anthropic. On September 4, the company announced that a team of AI agents, working together, had completed a formalized demonstration of Fermat's Last Theorem in just 11 days. This achievement confirms the correctness of the proof originally provided by mathematician Andrew Wiles in the 1990s. The work was reported on by New Scientist, highlighting the growing role of AI in tackling complex mathematical problems. Fermat's Last Theorem, proposed by French mathematician Pierre de Fermat in 1637, states that no three positive integers a, b, and c can satisfy the equation aⁿ + bⁿ = cⁿ when n is an integer greater than 2. Although Wiles' proof, completed in 1995, was groundbreaking, it was also highly complex and required years of development. Translating such proofs into computer-verifiable code has long been a challenge, as mathematical arguments are often expressed in natural language rather than in a form that computers can easily process. Recent advances in AI have enabled machines to "formalize" mathematical proofs, meaning they can convert human-written arguments into precise lines of code that can be checked by computers. This process typically uses the programming language Lean, which allows for rigorous verification of mathematical statements. The achievement by Claude, therefore, lies not in proving Fermat’s Last Theorem itself, but in translating Wiles' proof into a format that can be verified by computer systems. Kevin Buzzard, a mathematician at Imperial College London, has been working on formalizing Fermat's Last Theorem since 2024, but had not yet succeeded. Anthropic shared its results with Buzzard, who then compiled the code and submitted it for verification. Buzzard later shared the news on his blog, noting that Anthropic had achieved this milestone before his own team. The accomplishment has stunned many in the mathematical community, including Alex Kontorovich, a number theorist at Rutgers University, who described the AI's ability to produce an irrefutable proof in 13 million lines of code as astonishing.