Mathematician Kevin Buzzard of Imperial College London is training computers how to prove one of the most famous problems in math history: Fermat’s last theorem.
Resolving the problem isn’t the point. There’s already an accepted proof that was finalized in 1998. That work is a tortuous maze of mathematics that fills about 130 pages over two papers. It spans mathematical fields and unites abstract ideas that previously seemed to have little to say to one another. To know the proof is to know a wide swath of mathematics. In the future, Buzzard says, a computer program that can verify something so sprawling will be able to help mathematicians find,