Last week, a 23-year-old amateur with no advanced mathematical training did something many mathematicians never manage in a lifetime: he solved a 60-year-old problem posed by the spectacularly prolific Hungarian mathematician Paul Erdos. Liam Price, armed chiefly with curiosity and a ChatGPT-Pro subscription, found a solution to a long-standing Erdos conjecture that had resisted being solved for decades. Experts say the method appears genuinely new.

This would be a delightful one-off story on its own: the outsider beating the insiders. But it comes only weeks after another striking moment in mathematics. In March, the AI start-up Math, Inc. announced that its systems had formally verified Maryna Viazovska’s celebrated proof of the 24-dimensional sphere-packing problem. To do so, they translated one of the great mathematical achievements of recent years into ‘Lean’ – a programming language that allows a mathematical proof to be checked by a computer.

Put the two stories together and a larger picture begins to emerge. AI helps a newcomer find a proof. AI then helps turn a masterpiece of human reasoning into something a computer can certify line by line. The obvious next step is complete formal proofs produced by AI which can then be verified by a computer. We are not there yet and caution is needed. But the direction of travel is clear enough.

Price’s success is exciting........

© The Spectator