PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics

Moritz Firsching, Paul Lezeau, Salvatore Mercuri, Miklós Z. Horváth, Yaël Dillies, Calle Sönne, Eric Wieser, Fred Zhang, Thomas Hubert, Blaise Agüera y Arcas, Pushmeet Kohli

arXiv:2605.13171v1cs.AI

TL;DR

Research-level formal mathematics needs benchmarks that avoid leakage and saturation while evaluating complete proofs. Formal Conjectures builds an evolving Lean 4 collection with open conjectures, solved problems, and kernel-verified evaluation. Its reported solve rates rise with increased search compute and a newer prover agent.

  • Problem

    Existing mathematical benchmarks face data leakage, restricted evaluation access, oversimplified answer-checking, and saturation, limiting evaluation of research-level proof discovery.

    Source: §1 · p. 1

  • Method

    The authors build an evolving Lean 4 benchmark and use kernel-accepted proofs, collaborative formalization audits, and frozen evaluation subsets.

    Source: §1 · p. 2, §3.3 · p. 5, §4.1 · p. 7

  • Results

    Solve rate rose from 45% to 50% on FC100SolvedSet1 as simulations increased from 1,000 to 16,000 per problem, and reached 66% with a newer development agent.

    Source: §4.2 · p. 9

  • Takeaways & Limitations

    Versioned, frozen evaluation subsets provide stable, reproducible comparisons alongside the evolving benchmark.

    Source: §6 · pp. 9–10

    Problem selection is constrained by Mathlib’s coverage and biased toward famous conjectures and Erdős problems, while open-problem formalization risks remain until a full proof is provided.

    Source: §5 · p. 9

Abstract

from arXiv · show

As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures, an evolving benchmark of currently 2615 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery, and 836 solved problems for proof autoformalization. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged to make new mathematical discoveries, including the resolution of open research conjectures. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.

1 Introduction

Existing mathematical benchmarks face data leakage, restricted evaluation access, oversimplified success criteria, and saturation. Formal Conjectures responds with an open, evolving Lean 4 benchmark centered on research conjectures and kernel-verified proofs.

1 Introduction

  • Existing benchmarks can leak solutions, restrict access to evaluation sets, reduce success to simple answers, or become saturated.The paper notes that MiniF2F is routinely solved with over 99%.Source: §1 · pp. 1–2
  • Formal Conjectures is an open-source, growing collection of mathematical problems formalized in Lean 4, with open conjectures as its primary challenge.Its solved problems provide a secondary challenge for auto-formalization, without the same zero-contamination guarantees.Source: §1 · p. 2
  • The benchmark uses Lean's kernel to verify proofs objectively and reports standardized evaluations on frozen subsets for reproducible comparisons.The paper also describes a collaborative formalization pipeline and a taxonomy of misformalizations.Source: §1 · p. 2
  • The Formal Conjectures Benchmark is an evolving dataset of 2,615 mathematical statements in Lean 4, including 1,029 open conjectures for zero-contamination proof discovery and 836 solved problems for auto-formalization.A repository interface connects mathematicians with an ecosystem of automated solvers to facilitate simultaneous statement auditing and rapid dissemination of problems to AI systems.Source: §1 · p. 2

2 Related Work

Prior mathematical benchmarks include informal answer-checked tasks and formal theorem-proving benchmarks, some of which have become saturated. Formal Conjectures addresses the demand for research-level evaluation and is already being used in mathematical discovery.

2 Related Work

  • Informal benchmarks such as FrontierMath and Humanity’s Last Exam use answer-checking, while MathArena assesses informal proof-writing.Formal benchmarks instead permit automatic verification of full reasoning or proofs.Source: §2 · p. 2
  • MiniF2F and later undergraduate-level benchmarks have faced saturation as systems improved, motivating evaluation on unsolved research-level mathematics.The discussion cites rising competition-level capabilities, including silver-medal performance at the 2024 IMO and gold-medal equivalents at the 2025 IMO.Source: §2 · pp. 2–3
  • Formal Conjectures formalizes Erdős Problem 124 with an unintended extra hypothesis, yet Aristotle proved it without relying on that hypothesis [Bloom, 2025].The paper presents such proof attempts as an auditing mechanism for formalization fidelity.Source: §2 · p. 3
  • The repository has also supported subsequent discoveries and systematic evaluation of open problems, prompting versioned snapshots for reproducible benchmarking.The paper cites [Alexeev and Mixon, 2025] and.Source: §2 · p. 3

3 Formal Conjectures

Formal Conjectures combines problems from varied mathematical sources with open and solved statements, collaborative formalization, and multiple mechanisms for auditing fidelity. Its methods address statement ambiguity, proof verification, and iterative correction.

3.1 Problem Selection and Composition

  • Problems come from sources including Erdős and group-theory problem collections, quantum-problem lists, journals, arXiv, and MathOverflow.The repository has grown steadily since its open-source release.Source: §3.1 · p. 3
  • Open conjectures target proof discovery, while solved problems support auto-formalization and can provide related variations or checks on open statements.Simpler solved cases can help detect incorrect formalizations of open problems.Source: §3.1 · p. 4

3.2 Formalization Methodology

  • Statements pair Lean theorems with informal statements; open problems use proof placeholders, while solved-item proofs are kept short to keep the repository lightweight.Longer proofs may be hosted elsewhere and linked through the formal_proof mechanism.Source: §3.2 · p. 4
  • The answer(sorry) construct separates supplying a requested answer from proving it correct, and can encode a conjecture or refutation as True or False.It is implemented as a custom Lean term elaborator.Source: §3.2 · p. 5
  • Auxiliary results not yet in Mathlib are maintained for conjectures, while formal_proof links solutions in the repository or other systems without bundling long proofs.The attribute distinguishes repository proofs, equivalent Lean 4 proofs elsewhere, and proofs in other systems.Source: §3.2 · p. 5

3.3 Misformalizations

  • The taxonomy distinguishes Translation, Underspecified, and Source misformalizations according to where the error originates and how much the formalizer contributes.Underspecified and Source errors can help clarify informal statements, as illustrated by revisions to Erdős Problem 978.Source: §3.3 · p. 5
  • The repository fixed 291 misformalizations, with misrepresentation errors accounting for 48% and semantic errors for 35%.The taxonomy also groups six error types across its three levels.Source: §3.3 · pp. 5–6

3.4 Avoiding Misformalizations

  • Human Lean and domain review, test lemmas, AI proof and disproof attempts, and source-text cross-checks all help audit formalizations.The release includes 467 test statements and 155 API statements; custom linters enforce metadata standards, and discovered corrections can be upstreamed to original sources.Source: §3.4 · p. 6

4 Benchmark Evaluation

The benchmark separates zero-contamination proof discovery on open conjectures from auto-formalization of solved problems, using kernel-checked proofs and reproducible evaluation setups. Its frozen solved-problem results show a climbable signal across compute budgets and prover systems, while the living repository supports ongoing evaluation.

4.1 Evaluation Framework

  • The benchmark separates zero-contamination discovery of formal proofs for open problems from auto-formalization, measuring translation of established mathematics into formal code with Lean 4 and Mathlib.Its auto-formalization baseline is system-agnostic and tracks all formal proofs contributed to the repository, regardless of origin.Source: §4.1 · pp. 7–8
  • Frozen subsets of 100 open and 100 solved statements support stable comparisons, while versioned snapshots pin problem sets and Lean/Mathlib toolchains.Snapshots are immutable; fixes to misformalizations enter later versions rather than changing historical evaluations.Source: §4.1 · p. 7
  • Lean 4 kernel acceptance of a proof term replacing sorry provides the binary success criterion, with no forbidden axioms such as sorry.Open-problem results also require manual inspection because a proof may settle a misformalized statement rather than the intended problem.Source: §4.1 · p. 7
  • The living repository adjusts as conjectures are added, solved, or corrected, and its unified API exposes submissions to evaluating systems concurrently.The hardest problems remain open, pushing the frontier of automated reasoning.Source: §4.1 · pp. 7–8
  • Open-problem proof discovery starts at 0% because no formal proof exists for any research-open statement at tagging; later releases reclassify solved problems and add new conjectures.A proof that settles a misformalized statement triggers revision rather than counting as a solution to the intended problem.Source: §4.1 · p. 8
  • 17.3% of research_solved statements have a known formal proof: 5.3% internal and 12.1% linked externally.Table 1 summarizes proof coverage across statement categories, distinguishing repository proofs, linked proofs, and either kind of proof.Source: §4.1 · p. 8, Table 1 · p. 8

4.2 Illustrative Evaluation

  • 45% with 1,000 simulations, 50% with 16,000 simulations, and 66% with a development prover agent were achieved on FC100SolvedSet1.The AlphaProof evaluations use tree-search inference without test-time reinforcement learning; the development agent is a different system.Source: Table 2 · p. 8, §4.2 · p. 9

5 Discussion

Formal Conjectures also makes mathematical statements precise through stable file and commit references, while formalization can reveal gaps in Mathlib. Its scope remains shaped by Mathlib coverage and selection biases, and the project plans to extend the repository and its features.

Broader Benefits

  • Unique file names and commit hashes fix the intended meaning of conjectures, while formalization can reveal Mathlib gaps addressed through continuously upstreamed results.The repository also benchmarks reasoning and expands formalized mathematics by identifying hard-to-state concepts.Source: §5 · p. 9

Limitations

  • Problem selection is constrained by Mathlib coverage and favors famous conjectures and Erdős problems, concentrating the collection in number theory and combinatorics.The authors plan to broaden sourcing to areas including computer science and physics.Source: §5 · p. 9
  • Open-problem statements risk misformalization until proved, solved-problem arguments may be retrieved from training data, and future solutions can contaminate the open set.The repository tracks developments and reclassifies problems; frozen, versioned subsets support stable evaluation despite revisions.Source: §5 · p. 9

Future Work

  • The project plans to maintain and extend its problem collection, improve existing problems, and add platform features.The authors report steady repository growth since its initial release.Source: §5 · p. 9

6 Conclusion

Formal Conjectures is an evolving Lean 4 collection of open research problems and solved statements, paired with frozen evaluation subsets for stable comparisons. The appendix describes its statement-counting conventions, answer placeholders, staging library, misformalization taxonomy, and examples of implicit conventions.

6 Conclusion

  • Formal Conjectures combines broad coverage, open conjectures for zero-contamination evaluation, solved problems for auto-formalization, and frozen subsets for stable model comparisons.The conclusion presents the repository as an evolving resource alongside versioned evaluation subsets.Source: §6 · pp. 9–10

A.1 Source and AMS Classification Tables

  • Tables count formal statements by source collection and category, not distinct source problems; notable AMS areas include quantum theory, linear algebra, and algebraic geometry.One source problem may yield variants, special cases, solved subproblems, and test lemmas.Source: Table 3 · p. 13, §A.1 · p. 13, Table 4 · p. 13

A.2 The answer(sorry) Mechanism in Detail

  • The answer(sorry) mechanism separates finding a computational answer from proving it, and postpones elaboration so the statement’s type is fixed before the answer is supplied.It also marks which part of a formalization is the solution and can prevent statements from presupposing that solution.Source: §A.2 · p. 14

A.2.1 Propositional Solutions

  • For propositions with unknown truth value, replacing answer(sorry) with True asks for a proof of P, while False asks for a disproof.The default elaboration permits proof-only systems to decide the proposition by proving or disproving it.Source: §A.2.1 · p. 14

A.3 The “for Mathlib” Pattern

  • FormalConjecturesForMathlib stages results that may be specialized or awaiting Mathlib abstractions and review, with contributions later moving upstream asynchronously.The staging approach bypasses the dependency chain of review, monthly release, and repository upgrade.Source: §A.3 · pp. 14–15

A.4 Misformalization Taxonomy

  • The taxonomy distinguishes Lean syntax and semantic errors, translation misrepresentations, implicit conventions, reporting changes, and mathematical errors in source material.The categories range from formalization-level issues to errors or changes in the source text.Source: §A.4 · p. 15

A.5.4 Implicit Conventions

  • Examples include assuming an inequality holds for sufficiently large N and using “subgraph” where “induced subgraph” is intended [Erdős, 1993, p. 344].The latter distinction matters because the problem is trivial without the induced-subgraph restriction.Source: §A.5.4 · p. 18, Figure 11 · p. 18, Figure 12 · p. 19

A.5.1 Syntactical Errors

The appendix illustrates a syntactical error corrected by changing the parentheses.

A.5.1 Syntactical Errors

A.5.2 Semantic Errors

The examples show semantic errors arising from subtle differences in Lean’s representation of mathematical objects and operations.

A.5.2 Semantic Errors

A.5.3 Misrepresentation Errors

The appendix illustrates misrepresentation errors introduced when translating informal statements into formal ones.

A.5.3 Misrepresentation Errors

A.5.5 Reporting Errors

Reporting errors can arise from ambiguities in historical sources, as Figure 13 illustrates. Frozen evaluation subsets preserve membership across releases while requiring both the set name and release tag for reproducibility.

A.5.5 Reporting Errors

  • Figure 13 shows a reporting error rooted in historical-source ambiguity over whether the conjecture concerns induced subgraphs and whether ≤ℵ0 is explicit.The ambiguity was clarified after draft formalization through website comments and AlphaProof discoveries.Source: §A.5.5 · p. 19, Figure 13 · p. 19

B.1 Frozen Subsets

  • Frozen subsets contain 100 uniformly sampled problems each from the research-solved and research-open categories, and their files are compiled in every tagged release.The files import the corresponding theorem statements and ensure the sets remain well-defined and compile across supported Lean versions.Source: §B.1 · p. 19
  • Problem membership remains stable across bench-version updates, although statements may be corrected or reclassified; Lean-version updates alone preserve the same statements.Reproducible results should specify both subset name and release tag, such as FC100SolvedSet1@bench-v1-lean4.27.0.Source: §B.1 · p. 20
  • Planned additional subsets may contain different problems to support evaluations at varied scales or difficulty levels while preserving existing sets.Examples include FC100SolvedSet2 and FC500OpenSet1.Source: §B.1 · p. 20

B.2 Illustrative Evaluation Details

The illustrative evaluations count a solution only when the Lean 4 kernel accepts its proof term without forbidden axioms. AlphaProof is tested at two search budgets, while the DeepMind prover agent results use an experimental development method.

B.2 Illustrative Evaluation Details

  • A solution is correct only if the Lean 4 kernel accepts its proof term without forbidden axioms.Source: §B.2 · p. 20
  • AlphaProof is evaluated with 1k or 16k simulations and two attempts per problem, using approximately 0.1 or 1.6 TPUh, respectively.The evaluated version uses tree-search inference without the test-time reinforcement-learning loop.Source: §B.2 · p. 20
  • DeepMind prover-agent results use a development method under active experimentation, with evaluation costing up to $100 per problem at current API pricing.Source: §B.2 · p. 20

C.1 Future Work

Future work will expand Formal Conjectures, broaden its language and metadata support, and develop community features through the accompanying website. Planned repository improvements also include centralized reference management.

C.1 Future Work

  • The benchmark will grow through problems enabled by new Mathlib definitions and community contributions, while its methodology is intended to transfer to Isabelle or Rocq with comparable library support.The project also plans to track future Lean updates for ecosystem compatibility.Source: §C.1 · p. 20
  • Planned metadata will record when conjectures were first proposed, helping users distinguish long-standing open problems from contemporary questions.Source: §C.1 · p. 20
  • A planned interactive interface will let the community share views on conjecture difficulty, mathematical significance, and conviction about truth value.The listed conviction options include True, False, or independent of ZFC.Source: §C.1 · p. 20
  • Future repository iterations aim to centralize mathematical-literature references, which currently are handled inconsistently and often duplicated across files.Source: §C.1 · p. 20
  • The accompanying website already supports browsing, source-code access, rendered docstrings, and searching, sorting, or filtering; future work will make status changes more prominent.Its metadata records when open problems are solved or solved problems receive formal proofs.Source: §C.1 · p. 20
  • The authors plan a public leaderboard to track successful AI-based solutions and recognize groups working on the problems.Source: §C.1 · p. 21

Related papers

Loading 2605.13171v1…