Math long resisted a digital disruption. AI is poised to change that

Modern formalization, supercharged by AI, could radically change the way people do mathematics

An animated GIF of a math equation.

Illustration by Melvin Galapon

This is a human-written story voiced by AI. Got feedback? Take our survey . (See our AI policy here .)

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.