Plan used by Anthropic’s Claude to formalize Fermat’s Last Theorem; source: Anthropic
Introduction
In 1637, French mathematician Pierre de Fermat, while perusing a copy of Arithmetica, an ancient mathematical text by the Greek mathematician Diophantus, wrote in the margin (English translation): “It is impossible to separate a cube into two cubes, or a fourth power into two fourth powers, or in general, any power higher than the second, into two like powers. I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.” In modern mathematical parlance, “No positive integers a, b, c
Continue reading AI software completes a formal proof of Fermat’s Last Theorem