Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
Authors: Alan Sorani, Ashvni Narayanan, Michael Shalyt, Tali Monderer, Rotem Kalisch, Hila Barkan, Elyasheev Leibtag, Shachar Weinbaum, Carsten Schneider, John Campbell, Ido Kaminer
Organizations: Ramanujan Machine Group, Technion, Haifa, Israel. · Department of Mathematics, Computer Science and Statistics, Ghent University, Ghent, Belgium. · Research Institute for Symbolic Computation, Johannes Kepler Universität Linz, Linz, Austria. · Department of Mathematics and Statistics, Toronto Metropolitan University, Toronto, Canada.
As AI's mathematical capabilities rapidly improve, meaningful benchmarks are shifting from university-level problems and math olympiads to research-level mathematics. The Ramanujan Challenge is a benchmark comprised of research-level problems in number theory, including unpublished results and open conjectures. It presented concrete formulas for mathematical constants whose correctness can be checked numerically, while their proofs may require non-obvious mathematics. Here, we analyze the Challenge submissions, measuring the relative success of different AI models, Computer Algebra Systems (CAS), and formal tools. We find correct submissions that are conceptually distinct from the official solutions, and a proof of one of the published open conjectures. Evaluating the submissions exposed a second challenge: judging complex proofs reliably at scale. We introduce an AI-assisted evaluation pipeline for natural language proofs, CAS code, and Lean formalizations that assesses semantic and logical correctness. Compared with the conventional one-shot LLM judgment, our pipeline reduces false-positive verdicts on natural language proofs from 23% to 6% and improves judgment accuracy on supporting code from 46% to 58%. This approach provides a methodology for evaluating research-level mathematics at scale, with potential applications across mathematics and AI for science.
Figures & tables
Figure 1: Overview of the evaluation pipeline.
Figure 2: The trust spectrum.
Table 1: Agreement of the LLM agent with human verdicts without using our pipeline (via one-shot prompting) and with the pipeline.
Figure 3: AI models used by the submissions, in percentages out of the total number of submissions, with data from the 61% of submissions which reported their AI tools.
Figure 5
Natural language proof
Computer Algebra System/Lean
Question
Number of submissions
Correct
Partial
Major issues
Correct
Partial
Major issues
No code
1
23
11
6
6
7
11
3
2
2
16
7
3
6
2
8
4
2
3
19
10
3
6
5
7
5
2
4
19
4
7
8
1
13
3
2
5
11
2
2
7
0
5
4
2
Table 2: Human evaluation of the submissions, with each submission receiving a trinary grade for its natural language proof, CAS and Lean code, when present.
Figure 6: Correctness of natural language proofs and CAS derivation or Lean proofs, according to human evaluation. CAS code was all found to be at most partial and did not include comprehensive verification or proof of the problem statements, explaining the 0% on the first column.
Figure 7: Correctness of natural language proofs and CAS/Lean code based on their level of formality. Code which did not include a Lean formalization did not make complete verification or proof and no such code was judged as correct.
Figure 8: Trust level in the solutions to the challenge questions, in percentages.
Figure 9: Correctness of natural-language proofs and code for the submissions that used Lean, split by whether their submitted Lean source contains axiom , constant , sorry , or admit .
Figure 10: Correct and Partial verdicts for submissions to the challenge questions, by tool combination, for combinations that appeared in at least 5 submissions.
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.
Jierui Zhang, Siyuan Tan, Xinhang Li +8
School of Computer Science Beijing University of Posts and Telecommunications Beijing, China · Graduate College for Engineers Beijing University of Posts and Telecommunications Beijing, China · School of Mathematical Sciences Fudan University Shanghai, China +6
As the mathematical capabilities of large language models (LLMs) improve, it becomes increasingly important to evaluate their performance on research-level tasks at the frontier of mathematical knowledge. However, existing benchmarks are limited, as they focus solely on final-answer questions or high-school competition problems. To address this gap, we introduce IMProofBench, a private benchmark consisting of 77 peer-reviewed problems developed by expert mathematicians. Each problem requires a detailed proof and is paired with subproblems that have final answers, supporting both an evaluation by human experts and a large-scale quantitative analysis through automated grading. Furthermore, unlike prior benchmarks, the evaluation setup simulates a realistic research environment: models operate in an agentic framework with tools like web search for literature review and mathematical software such as SageMath. Our results show that current LLMs can already solve a significant percentage of research-level questions. IMProofBench will continue to evolve as a dynamic benchmark in collaboration with the mathematical community, ensuring its relevance for evaluating the next generation of LLMs.
Johannes Schmitt, Gergely Bérczi, Jasper Dekoninck +57