Pierre de Fermat was a 17th-century mathematicianLebrecht Music& Arts, YAY Media AS/Alamy
In the lobby of a central London hotel, tourists are bracing themselves for a day of sightseeing in a heatwave. Meanwhile, staff are resetting the dining room after breakfast. And in a windowless meeting room, assembled academics are contemplating whether humans have a role to play in the future of mathematics, now that AI can prove theorems by itself.
The general mood in the room is one of bewilderment at the recent jump in computer intelligence and excitement about the potential it unlocks – and perhaps a slight unease about what the future holds for them personally.
Twenty-five researchers from diverse fields and countries are here to spend a week working on formalising Fermat’s last theorem with cutting-edge AI models.
Fermat’s last theorem puzzled mathematicians for centuries until it was proven in 1993 by Andrew Wiles. It states that there are no whole numbers a, b, and c that satisfy the equation aⁿ + bⁿ = cⁿ, where n is a whole number greater than 2. It is extremely easy to state, but fiendishly difficult to prove.
