Ramanujan Challenge 发布 AI 辅助评审流水线，判定研究级数学证明
Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
数论基准 Ramanujan Challenge 的团队做了个评审流水线，自动判研究级数学证明，误判率从 23% 压到 6%，做数学 AI 评测的可以看看。
Ramanujan Challenge 是一个由数论研究级问题构成的基准，包含未发表结果和公开猜想。团队分析了各 AI 模型、计算机代数系统（CAS）和形式化工具的提交结果，发现出现了与官方解法概念不同的正确证明，其中一个公开猜想被证出。为解决大规模评判复杂证明的难题，他们引入了一套 AI 辅助评审流水线，覆盖自然语言证明、CAS 代码和 Lean 形式化。与单次 LLM 评判相比，该流水线把自然语言证明的误判率从 23% 降到 6%，代码评判准确率从 46% 提升到 58%。
Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
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.