PaperlayerView exact revision on arXiv

Source-linked AI summary

Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs

Alan Sorani, Ashvni Narayanan, Michael Shalyt, Tali Monderer, Rotem Kalisch, Hila Barkan, Elyasheev Leibtag, Shachar Weinbaum, Carsten Schneider, John Campbell, Ido Kaminer

arXiv:2610.40551v1cs.AIcs.CLcs.SCmath.NT

TL;DR

Research-level mathematics is becoming a target for AI benchmarks, while large volumes of complex proof submissions are difficult to evaluate reliably. The paper analyzes the Ramanujan Challenge and presents a pipeline for natural-language proofs, CAS code, and Lean formalizations; it reports fewer false positives and improved code agreement with human evaluation. The authors argue that structured evaluation can improve judgment quality even when the underlying LLM is unchanged.

  • Problem

    Research-level AI mathematics benchmarks need frontier problems with unpublished solutions, while growing volumes of complex proof submissions make reliable evaluation difficult.

    Source: §1 · p. 1

  • Method

    The paper analyzes Ramanujan Challenge submissions and uses an AI-assisted pipeline to evaluate natural-language proofs, CAS code, and Lean formalizations.

    Source: §1 · pp. 1–2

  • Results

    The pipeline reduced false-positive grading by factors of 4 for natural language proofs and 11.5 for CAS/Lean code, and raised code agreement with human evaluation from 46% to 58%.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The authors conclude that structured evaluation can improve judgment quality even when the underlying LLM is unchanged.

    Source: §9 · p. 10

    Each natural-language proof and CAS or Lean submission was evaluated by a single human without cross-checking, leaving judgments prone to human error and evaluator-background bias.

    Source: §8 · p. 10

Abstract

from arXiv · show

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.

1 Introduction

The paper presents the Ramanujan Challenge as a research-level number theory benchmark and introduces a pipeline for evaluating complex proofs at scale. The authors report improved evaluation outcomes and submissions that broaden who can contribute to research mathematics.

1 Introduction

  • Research-level AI mathematics benchmarks followed school-level, university-level, and olympiad benchmarks, but require frontier problems whose solutions are unpublished yet privately known.The authors describe this as a way to avoid training-data contamination.Source: §1 · p. 1
  • The ten-problem Ramanujan Challenge comprised eight author-proved but unpublished results and two open conjectures, and submissions combining Lean with CAS outperformed those relying on either tool alone.The most successful natural language proofs used models from the Claude and GPT families.Source: §1 · p. 1
  • Some correct submissions came from people without higher mathematical education, and one open conjecture received multiple correct proofs.The authors also report a high-school student making significant progress toward proving a challenge conjecture.Source: §1 · pp. 1–2
  • The 228 submissions contained 4,802 pages of natural-language proofs and 1,079,380 lines of code, illustrating the scale of proof evaluation.The paper places this challenge amid a wider surge in mathematical claims and prior approaches to automated validation.Source: §1 · p. 2
  • False-positive grading fell by a factor of 4 for natural language proofs and 11.5 for CAS/Lean code, while code agreement with human evaluation rose from 46% to 58%.The comparison is against the same LLM without the pipeline.Source: §1 · p. 2

2 Related Work and Novelty

  • The authors describe their pipeline as a first for large-scale evaluation of research-level computational mathematics and report that combined CAS and Lean use accompanies correct proofs more often than either alone.They present this combination as a basis for further research on integrating CAS with formal theorem assistants.Source: §2 · p. 3

3 The Trust Spectrum

The paper organizes proof validation along a trust spectrum, from numerical checks through CAS to formal theorem proving. It applies that perspective to the Ramanujan Challenge and describes a multi-stage pipeline and format-specific evaluation criteria.

3 The Trust Spectrum

  • The trust spectrum orders verification from soft numerical or probabilistic checks, through intermediate CAS symbolic validation, to hard machine-checked theorem proving such as Lean.The paper places formal verification highest on the spectrum because ITPs enforce line-by-line proof checking.Source: §3 · p. 3

4 The Challenge

  • The Ramanujan Challenge comprised eight questions and two conjectures with previously unpublished solutions, and requested formal proofs, CAS derivations, and natural-language proofs in that priority order.At the time it was posted, prevalent LLMs could not solve any problem with one-shot prompts, while participants submitted successful solutions.Source: §4 · p. 4

5 Methodology

  • The pipeline aims to reduce human grading effort by giving reviewers AI-generated summaries of submission files and a review connecting them.Python scripts receive basic grades; separate summaries are compared for similarities, conflicts, and common issues before human review.Source: §5 · p. 4, §5.1 · p. 4

5.1 Evaluation Pipeline

  • For natural-language proofs, the pipeline summarizes proof files; for code, it summarizes CAS/Lean files and basic grades when available, presenting only relevant files to limit idea contamination.Separate proof and code summaries are compared for similarities, conflicts, and common issues.Source: §5.1 · p. 4

5.2 Evaluation Criteria

  • Natural-language proofs must include the necessary mathematical steps; CAS code must reproduce proof steps, while Lean is checked for compilation, matching definitions, and absence of unverified sorry or axiom statements.Partial classifications cover meaningful proof progress or limited verification; code with major errors or noncompilation receives major-issues status.Source: §5.2 · p. 5

6 Dataset

The dataset comprises 207 submissions tied to specific challenge problems, with older near-duplicate versions excluded from analysis. Submissions included natural-language proofs, CAS or Lean code, and reported AI-tool use, while participants also submitted solutions to both conjectures.

6 Dataset

  • 39 older versions of later submissions by the same submitter were excluded to avoid skew from solutions with little variation.The challenge received 228 submissions, of which 207 clearly related to a specific problem: 167 addressed questions and 40 addressed conjectures.Source: §6 · p. 6
  • Participants used AI models, CAS, and ITPs, with Lean the only ITP reported.Submissions that did not specify AI tools were still included in the analysis, with specific mention where they were excluded.Source: §6 · p. 6
  • 88% of submissions answering challenge questions included CAS or Lean code alongside a natural-language proof.All submissions answering questions supplied a natural-language proof.Source: §6 · p. 6, Figure 4 · p. 6
  • The two conjectures received 20 and 11 solutions, respectively, with 10 participants submitting to both.Source: §6 · p. 6
  • Only 61% of submissions reported their AI tools; Figure 3 presents model percentages using that reported-tool data.Its percentages are out of the total number of submissions.Source: Figure 3 · p. 6
  • Solutions were classified by the lowest formality type they relied on, except “Human,” reserved for solutions containing only a natural-language proof.Natural-language proofs received a separate verdict from code.Source: §6 · p. 6

7 Results

The results compare correctness across submission tools, report evaluated outcomes for both conjectures, and assess an AI-assisted evaluation pipeline against human judgments. The pipeline reduced false positives and improved agreement on code.

7.1 Analysis of the Solutions to the Questions

  • GPT/Codex led AI-tool natural-language-proof correctness, while Claude with GPT or Codex led CAS/Lean-code correctness; CAS+Lean submissions led proof correctness and Lean-only submissions led code correctness.Lean formalizations containing unproved statements coincided with 0% correct code versus 58% without them, and 11% versus 49% correct accompanying natural-language proofs.Source: §7.1 · pp. 7–8
  • First correct solutions lacked Lean formalizations for questions 3, 6, and 7, while first correct solutions to five questions included correct Lean formalizations.Despite those first solutions, the overall percentage of correct Lean solutions was lower.Source: §7.1 · p. 8

7.2 Solutions to the Conjectures

  • Conjecture 1 had one correct, complete Lean proof and multiple other proofs judged likely correct after discussion; Conjecture 2 remains open with only partial solutions among evaluated submissions.Two of three other evaluated Lean solutions to Conjecture 1 had major issues, and one proved only partial results.Source: §7.2 · p. 9
  • Conjecture solutions had not yet been fully evaluated because of scope and time constraints.The authors stated that their evaluation would be included in the coming weeks.Source: §7.2 · p. 9

7.3 Analysis of the Evaluation Pipeline

  • The evaluation compared one-shot and pipeline-assisted Claude Opus 5 classifications against human verdicts used as reference labels.The classifications covered correct, partial, and major-issues judgments.Source: §7.3 · p. 9
  • False positives fell from 23.4% to 5.8% for natural-language proofs and 38.3% to 3.3% for code; code agreement rose from 45.8% to 58.3%.The pipeline also reduced overly lax judgments from 31.4% to 18.2% for natural-language proofs and from 50.0% to 12.5% for code.Source: §7.3 · p. 9

8 Limitations

The results are uncertain because of variation and potential bias in participant submissions and tools, as well as reliance on single-reviewer human judgments without cross-checking.

8 Limitations

  • Participants answered between one and all ten questions, and self-admitted to the challenge and self-reported their tool use, potentially skewing results.The authors identify these factors as sources of potential bias and uncertainty.Source: §8 · p. 10
  • Each natural-language proof and CAS or Lean submission was evaluated by one human without cross-checking, leaving verdicts prone to error and evaluator-background bias.The authors cite time and monetary constraints as the reason for single-evaluator review.Source: §8 · p. 10

9 Discussion and Outlook

The discussion connects research-level benchmark design with the need for scalable proof validation, and describes broader uses and practical details of the work.

9 Discussion and Outlook

  • Open conjectures could provide renewable benchmark problems, but their use depends on evaluation methods that work without known proofs.The authors also argue that research-level benchmarks may saturate as AI solvers advance.Source: §9 · p. 10
  • Lean and CAS evidence was more successful on average than single-tool submissions, with the authors identifying complementary strengths as one plausible explanation.Lean checks the logical validity of the formalized statement, while CAS can check symbolic and numerical computations that are difficult to formalize.Source: §9 · p. 10
  • The authors see potential applications for claim-and-code validation beyond number theory, including mathematics and AI for science.Generated claims in those settings may be supported by code, simulations, or data analyses.Source: §9 · p. 10

10 AI Use; 11 Ethics Statement; 12 Reproducibility Statement

  • AI tools were used across solution generation, evaluation, graphing, literature survey, and language editing; submitter identities were kept anonymous and supplemental results randomized.The authors report extensive Claude and Codex token use, and say anonymized submission results are included in supplemental materials.Source: §10 · p. 11, §11 · p. 11, §12 · p. 11

A The Challenge Questions

The challenge questions ask for proofs of explicit formulas involving mathematical constants, using limits, recurrences, series, and rational approximations.

Question 1; Question 2; Question 3

  • Questions 1–3 concern a polynomial continued fraction for π and Apéry limits for Euler’s constant γ and π + e.The statements give recurrence initial values for the π and π + e limits.Source: A The Challenge Questions · p. 15

Question 4

  • Question 4 asks for an identity involving harmonic numbers, a polylogarithm, and zeta values.The statement specifies that H_0 = 0 and H_k is the k-th harmonic number for k ≥ 1.Source: A The Challenge Questions · p. 15

Question 5

  • Question 5 asks for efficient rational approximations of Catalan’s constant using a matrix recurrence and specified initial conditions.The statement gives recurrence entries and initial conditions for four indexed cases.Source: A The Challenge Questions · p. 16

Question 6; Question 7

  • Questions 6 and 7 target ζ(2) + ζ(3), respectively through a defined sequence’s series and an efficient four-term recurrence.Question 6 supplies a recurrence for u_n; Question 7 gives recurrence coefficients.Source: A The Challenge Questions · pp. 16–17

Question 8

  • Question 8 asks for a very fast rational approximation, specifying parameters, a matrix convention, and initial conditions.The supplied statement includes R and definitions for u and w.Source: A The Challenge Questions · pp. 17–18

B The Challenge Conjectures

The challenge presents open conjectures as explicit formulas that can be checked numerically, including claims about a knot polynomial and Apéry’s bound for ζ(3).

Overview

Conjecture 1

  • Conjecture 1 asks for a formula involving an integral over roots of the A-polynomial for knot 72 that expresses π².It specifies a real solution β and a positive decreasing curve y(x) satisfying conditions on the polynomial.Source: B The Challenge Conjectures · p. 18

Conjecture 2

  • Conjecture 2 concerns the optimality of Apéry’s irrationality-measure bound for ζ(3), using sequences that solve Apéry’s recurrence.The surrounding text says the conjecture would make the bound tight for Apéry’s particular formula.Source: B The Challenge Conjectures · p. 18

Related papers

Loading 2610.40551v1…