Ten problems, 4,802 pages of answers
The Ramanujan Challenge put ten research-level number theory problems in public. Eight had been proved by the organisers but never published, which keeps them out of any training set; two were open conjectures. Each problem was a concrete formula for a mathematical constant, so correctness could be checked numerically even where the proof needed non-obvious mathematics.
Participants sent back 228 submissions. Between them they contained 4,802 pages of natural language proofs and 1,079,380 lines of code across Lean, Python, Mathematica and Sage. The results paper, posted on 29 October by the Ramanujan Machine group at the Technion in Haifa with co-authors at Ghent University, the Research Institute for Symbolic Computation in Linz and Toronto Metropolitan University, is as much about reading that pile as about what is in it.
Who solved them
Submissions that produced correct natural language proofs most often used models from the Claude and GPT families. Submissions that combined Lean with a computer algebra system outperformed those relying on a single tool, which the authors read as a benefit of diversified supporting evidence rather than of any one prover.
One of the two published open conjectures received multiple correct proofs. Some of the complete proofs came from amateur mathematicians. One submitter had no higher mathematical education, and their solution to one of the problems was found to be simpler than the organisers’ own. A high-school student made significant progress towards proving one of the conjectures.
That is the result worth separating from the benchmark score. The challenge was designed to measure models, and what it measured was a change in who can reach research-level number theory at all.
The second problem the challenge created
Judging the submissions turned out to be the harder task. The authors describe a boom in AI-assisted mathematics producing “an avalanche of mathematical claims”, a problem that extends well past their own benchmark: 4,802 pages cannot be refereed the way ten papers can.
Existing benchmarks handle this in different ways — a single LLM as judge, an LLM checking equivalence against known ground truth, or deterministic code verifying a model’s answer. The team built an AI-assisted pipeline instead, one that assesses semantic and logical correctness across all three submission formats: natural language, computer algebra code and Lean formalisations.
Against conventional one-shot LLM judgment, the pipeline cut false-positive verdicts on natural language proofs from 23% to 6%. Judgment accuracy on supporting code went from 46% to 58%.
Read in the other direction, those are the numbers that matter. A one-shot LLM judge waved through roughly one in four wrong natural language proofs, and was right on supporting code less than half the time. Any leaderboard scored that way is reporting its judge as much as its models.
What to watch
Whether research-level maths benchmarks publish their judging error rate alongside their scores. The 6% residual is still a false positive in one submission in sixteen, and the pipeline’s 58% on code is an improvement on a low base rather than a solved problem. The organisers propose their method as a methodology for evaluating research-level mathematics at scale, with applications across AI for science. The paper is a preprint and has not been peer reviewed; it is released under CC BY-SA 4.0.
