Top mathematicians grade AI’s ability to solve toughest problems

Less than a year ago, a Harvard math professor joined a handful of world-leading scholars on an ambitious experiment designed to better define the capabilities of AI systems and delineate the boundaries with human expertise.

They repeatedly challenged AI systems to crack 10 tough research math problems, which scholars had recently solved but not yet published. In the consortium’s latest round of test results, unveiled last week, AI systems collectively solved all 10 problems. But the models still lagged in the ability to clearly communicate and document their results.

“In the last months, AI has changed the ecosystem for research mathematics,” said Lauren K. Williams, Dwight Parker Robinson Professor of Mathematics and co-organizer of the consortium behind the testing. “Essentially all the media around AI and mathematics focuses on success stories. That makes it hard to get a more nuanced, objective view of the current state of public models. Can they just do everything? If not, where do they fall short?”

The tests were conducted by First Proof, an organization of research mathematicians seeking to establish more objective criteria for evaluating the rapidly expanding powers of AI systems — and promote a more nuanced understanding of how these technologies can help or hinder the basic mission of research math.

The latest results come on the heels of stunning advances in the ability of large language models to crack problems that have stumped the world’s top mathematicians.

In September, OpenAI announced that its models had solved the Navier–Stokes problem, one of the great unsolved Millennium Prize Problems. However, this claim set off a firestorm of controversy about whether the company had exploited unpublished work by scholars working on the problem.

Earlier this month, OpenAI released an avalanche of solutions to hundreds of other open math problems via a public website. 

With one disruptive event after another, the rapid advance of AI has sparked an existential crisis in university math departments. The First Proof effort seeks to more clearly illuminate where these systems provide useful help — and where they do not.

The project was initiated by mathematicians Mohammed Abouzaid of Stanford University and Rachel Ward of the University of Texas at Austin. They were joined by Williams and other mathematicians from institutions such as Columbia, Duke, Yale, and the University of Chicago. Represented in their ranks are one Fields medalist — considered the highest honor in mathematics — and two winners of “genius grants” from the MacArthur Foundation.

During the project’s first round of testing, in February, OpenAI and Google submitted solutions by their internal models. First Proof reviewers did not formally grade the solutions, but generally agreed that each model had solved five or six problems and together cracked seven.

Even so, reviewers found some of the proofs difficult to read and detected hints of “irregularities” that undermined their confidence in how the solutions were produced.

In the second round of tests, conducted in late May and early June, AI systems collectively solved seven of 10 problems.

For this latest round, First Proof released a new set of 10 problems in August. The challenges spanned a broad swath of mathematical topics including logarithmic geometry, statistics, symplectic geometry, and topology. Each AI system was given one shot to produce a proof no longer than 12 pages within 24 hours.

Five different AI models were tested. Four rested on so-called frontier models, the most advanced systems developed by private companies. They included GPT-6 Astra by OpenAI, two “harnesses” (software enhancements added to frontier AI systems) designed by academic teams, and a third harness by Anthropic.

For the first time, First Proof also included an “open-weight” AI model whose core components are publicly available: the Kimi K3, released by Moonshot AI earlier this year.

The AI systems’ solutions were evaluated by a pool of 30 human reviewers who gathered earlier this month at the Institute for Computer-Aided Reasoning in Mathematics at Carnegie Mellon University. Solutions were anonymized, graded by three different reviewers apiece, and scored for correctness (whether the solution was right or wrong), exposition (clarity of writing), and attribution (proper credit of existing scholarship).

The top-performing system, ProofCouncil (a “multi-agent” harness that draws upon GPT-6 Astra, Claude Fable 5.1, Claude Sonnet 5, and Gemini 3.1 Pro), solved nine of the problems. The second best, Astra, solved seven. Both models were tested during First Proof’s previous round and each solved two more problems than last time.

“It’s a very substantial improvement,” said Nikhil Srivastava, a mathematician at the University of California, Berkeley, who noted that AI systems are solving more problems even though each round has required longer, more challenging proofs. “As we’ve seen, there has been a big jump in capabilities this summer.”

Yet the top models were less impressive when it came to presenting results with proper exposition and citations. For example, solutions were often excessively wordy, poorly organized, needlessly complicated, or used improper notations.

“I don’t think exposition is getting better,” Ward noted. “It might be getting worse as the solutions become more complex and longer.”

Even when they devised correct solutions, the systems sometimes failed to provide proper attribution. In one case, reviewers found the lack of attribution “essentially constituted plagiarism.”

Williams said the team sought to expose capabilities and shortcomings so mathematicians can more efficiently evaluate AI tools. In one instance, she said an AI system mistakenly generated an answer based on a typo in an old version of a published paper. But reviewers had difficulty figuring out what had gone wrong, because the mistake had been corrected during subsequent revisions of the paper.

“Reading an AI-generated solution can be extremely painful and time-consuming,” Williams said. “If these models are producing mathematics that’s correct, but really hard to read — or sometimes false, but it takes you hours to determine that — that’s a waste of human time.”

In another key finding, the tests exposed a wide performance gap between frontier systems produced by AI companies and the “open-weight” models whose internal workings are made public. According to First Proof, every one of the open-weight submissions contained major errors.

In the next round of tests, scheduled for January, organizers plan to conduct separate tests with open-source systems. The goal is more clearly diagnosing problems and identifying how performance can be improved.

“Our testing is currently far too harsh for systems that are built on open-weight models,” Abouzaid said.

Williams said the gap between the private companies and open-source systems should be a matter of public concern — and perhaps the most important takeaway from the latest round of tests.

Many mathematicians worry about the concentration of information and power in the hands of private AI companies, Williams said. Colleagues have voiced concerns about data leakage and suspicions that the AI systems have not adhered to privacy standards.

“It seems very unhealthy for two companies to wield such a tremendous power in the world,” Williams said. “It would be good to have alternatives, but at present, mathematicians don’t have a feasible alternative.”