Column|LLM: Going the Way of Go

The experience of Go players and programmers hints at the future of mathematicians

Just two years ago, leading AI models were still making embarrassingly basic mistakes. They fumbled arithmetic and confidently told users that 9.11 was larger than 9.9. Today, mathematicians are examining whether AI-generated proofs settle problems that have resisted decades of human effort. It has been a short journey from the schoolroom to the research frontier.

Earlier this month, a rumor went around Silicon Valley that OpenAI was about to release some 400 mathematical proofs worthy of a Fields Medal, one of mathematics’ highest honors. On October 6, the papers arrived, and there were more of them than the rumor suggested: 722 manuscripts, grouped into 372 research families, all produced by an internal OpenAI model. The company says it put roughly 4,000 open problems to the model. The reported average compute per result was equivalent to roughly three hours of ChatGPT Pro thinking; a small number of results used different procedures.

Sam Altman, OpenAI’s chief executive, singled out four results as the most important: a proof of the quasi-Riemann hypothesis, a proof of the Unique Games Conjecture from theoretical computer science, the Hodge conjecture for CM abelian varieties (a special case of one of the seven Millennium Prize problems), and an answer to a question about “free group factors” that has been open since the 1940s. He was careful to call them claims that outside mathematicians have yet to confirm. Many of the proofs, though not all, come with versions written in Lean, a language that lets a computer check a formal proof step by step. The formal statement must still be checked against the original problem.