Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
Abstract
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.
Related
- Ramanujan-Type Series of Signature 2: Analytical Evaluation via Degree-2 Transformations and Associated Harmonic Expansions
- Analytical Evaluation of Ramanujan Series for 1/π via Degree-2, Degree-3, Degree-7, and Degree-19 Modular Transformations
- A Four-Genus Kronecker-Limit Evaluation of the Alternating Rogers-Ramanujan Continued Fraction
- Computer-Assisted Results for n-Sided Non-Transitive Dice Taking Face Values in [n]
- How to Run Statistics over LLM Judges and Trust the Results: Calibrated Inference for Small-Sample AI Evaluation with evalstats
BibTeX
@misc{sorani2026ramanujan,
title = {{Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs}},
author = {Alan Sorani and Ashvni Narayanan and Michael Shalyt and Tali Monderer and Rotem Kalisch and Hila Barkan and Elyasheev Leibtag and Shachar Weinbaum and Carsten Schneider and John Campbell and Ido Kaminer},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.40551},
eprint = {2610.40551},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.40551},
note = {CC BY-SA 4.0},
}
RIS
TY - UNPB
TI - Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
AU - Alan Sorani
AU - Ashvni Narayanan
AU - Michael Shalyt
AU - Tali Monderer
AU - Rotem Kalisch
AU - Hila Barkan
AU - Elyasheev Leibtag
AU - Shachar Weinbaum
AU - Carsten Schneider
AU - John Campbell
AU - Ido Kaminer
PY - 2026
DA - 2026/10/29
PB - arXiv
DO - 10.48550/arxiv.2610.40551
UR - https://arxiv.org/abs/2610.40551
AB - 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.
ER -