人工智能助力费马大定理的形式化证明

AI put to work on Fermat’s last theorem Mathematicians are making quick progress in formalising the famous problem after turning to AI for help, reports Matthew Sparkes IN A windowless meeting room of a central London hotel, 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 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. …