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

Summary (Overview)

• Formal Conjectures is a large-scale, evolving benchmark of 2,615 mathematical problem statements formalized in Lean 4 using Mathlib, comprising 1,029 open research conjectures for zero-contamination proof discovery and 836 solved problems for proof auto-formalization.

• The benchmark addresses critical limitations of existing evaluation frameworks: data leakage, secretive evaluation, oversimplified success criteria, and saturation (e.g., MiniF2F is now solved at over 99%).

• The repository provides a unified API connecting mathematicians who formalize problems with AI systems, enabling simultaneous statement auditing and rapid dissemination to automated solvers.

• A three-level taxonomy of misformalizations (Translation, Underspecified, Source) with 291 fixed cases ensures formalization fidelity, with AI-generated proofs serving as a vital auditing mechanism.

• The benchmark includes frozen evaluation subsets (FC100OpenSet1 and FC100SolvedSet1) with baseline results demonstrating a climbable signal: AlphaProof achieves 45–50% and a DeepMind prover agent achieves 66% on FC100SolvedSet1.

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses the rapid advancement of automated reasoning systems and the corresponding need for research-level formal mathematical problems to evaluate their capabilities. The authors identify four key challenges with existing benchmarks:

1. Data leakage: Solutions appearing online make it difficult to distinguish genuine reasoning from memorization (affecting benchmarks like MiniF2F, PutnamBench, and FATE).

2. Secretive evaluation: Some benchmarks keep evaluation sets private to combat leakage, hindering open and reproducible research (e.g., FrontierMath, Humanity's Last Exam).

3. Oversimplified success criteria: Many benchmarks rely on verifying simple machine-checkable final answers rather than capturing complex multi-step reasoning.

4. Saturation: As models improve, benchmarks become saturated—MiniF2F is now routinely solved with over 99% accuracy.

Theoretical Foundation

The benchmark leverages Lean 4 [Moura and Ullrich, 2021] and Mathlib [The mathlib Community, 2020] as its formal foundation. The choice is pragmatic: Mathlib is the largest formal mathematics library available, essential for stating advanced conjectures. The core principle is that a proposed solution is definitively correct if and only if its corresponding proof is accepted by the kernel without relying on forbidden axioms like sorry.

Methodology

Problem Selection and Composition

Problems are sourced from diverse mathematical literature:

• Erdős problems (erdosproblems.com)
• Kourovka Notebook (unsolved problems in group theory)
• IQOQI Vienna (open quantum problems)
• Wikipedia conjectures
• Recent publications in journals and on arXiv
• MathOverflow questions

Problem Categories

Each statement is labeled with category tags:

• research open: open research-level problem
• research solved: solved research-level problem
• textbook: textbook-level problem
• API: foundational theory for new definitions
• test: sanity check statements

Statements are also tagged with AMS Mathematics Subject Classification codes, spanning over 10 subjects with number theory and combinatorics accounting for over half.

Key Mechanisms

The answer(sorry) construct: A custom Lean term elaborator that separates discovering a computable answer from proving it correct. For example, a question like "What is the smallest n such that P(n)?" is formalized with answer(sorry) as a placeholder that solvers replace with a concrete value.

The @[formal_proof] attribute: Decouples problem statements from solutions, supporting three modes:

1. formal_conjectures: proofs solving exactly the statement type in the repository
2. lean4: equivalent problems solved in Lean 4 elsewhere
3. other_system: problems solved in other systems (Lean 3, Isabelle, Rocq)

The "for Mathlib" pattern: A FormalConjecturesForMathlib directory containing 88 files of auxiliary definitions and lemmas not yet in Mathlib but needed for conjectures, asynchronously contributed upstream.

Misformalization Taxonomy

The paper introduces a three-level taxonomy of misformalizations:

1. Translation: informal statement is accurate and explicitly phrased (formalizer's error)
2. Underspecified: informal statement is accurate but lacks detail
3. Source: informal statement is not as intended (source's error)

These are further categorized into six types: syntactic, semantic, and misrepresentation errors (translation level); implicit conventions (underspecified level); and reporting and mathematical errors (source level). Across the repository, 291 misformalizations have been fixed, with misrepresentation (48%) and semantic (35%) errors being most common.

Quality Assurance

• Mandatory human code review with Lean expertise and domain knowledge
• Test-based design: new definitions accompanied by proven test lemmas and API statements (467 test statements and 155 API statements, 23.8% of repository)
• Automated theorem provers (AlphaProof) regularly attempt proofs and disproofs to reveal misformalizations
• Custom Lean linters enforcing metadata and documentation standards
• Community engagement with corrections upstreamed to original sources

Empirical Validation / Results

Repository Statistics

Table 1: Proof coverage across all statement categories

Frozen Evaluation Subsets

Two frozen subsets of 100 problems each are provided:

• FC100OpenSet1: 100 research open statements (0% baseline by definition)
• FC100SolvedSet1: 100 research solved statements for proof auto-formalization

Baseline Results on FC100SolvedSet1

Table 2: Results on the frozen FC100SolvedSet1

Key findings:

• AlphaProof achieves 45% with 1,000 simulations per problem, improving to 50% with 16,000 simulations—demonstrating a clear scaling signal
• The DeepMind prover agent achieves 66%, illustrating the benchmark's ability to measure advancements across improved architectures
• Evaluations use tree-search inference only (no test-time reinforcement learning)
• FC100OpenSet1 remains at a definitive 0% baseline, highlighting its status as a rigorous frontier

Real-World Adoption

Since its open-source release in May 2025, the repository has been used for actual mathematical discovery:

• Boris Alexeev used a repository formalization to prove Erdős Problem 124 with Aristotle
• A DeepMind prover agent solved several open problems in a systematic evaluation
• Misformalizations discovered through AI attempts led to refinements of informal problem statements (e.g., Erdős Problem 978)

Theoretical and Practical Implications

Benefits

1. Precise mathematics: Enforces formal precision, clarifying exact meanings of statements and creating unambiguous references via unique file names and commit hashes.

2. Compass for Mathlib development: Formalizing advanced conjectures reveals gaps in the existing library, addressed via the FormalConjecturesForMathlib directory.

3. Zero-contamination testbed: Open problems provide definitive success signals without requiring secretive evaluation sets.

4. Graduate-level challenge: The benchmark measures the current frontier of automated reasoning on research-level mathematics, avoiding the saturation problem of earlier benchmarks.

Limitations

• Scope bias: Constrained by Mathlib's current coverage, though mitigated by the ForMathlib directory
• Selection bias: Concentration in number theory and combinatorics due to famous conjectures and Erdős problems
• Misformalization risk: Subtle statement errors may persist until full proofs are provided
• Contamination challenges: Solved problems may allow retrieval rather than reasoning; open problems may eventually enter training data
• Kernel integrity: Verification relies on the Lean 4 kernel's integrity, though this remains the highest standard for rigor

Conclusion

Formal Conjectures establishes a rigorous, evolving benchmark for evaluating AI systems in formal mathematical research. By providing a zero-contamination testbed of research-level open problems alongside a substantial set for proof auto-formalization, it bridges the gap between human mathematical expertise and automated formal reasoning.

Key takeaways:

• The benchmark is publicly available under Apache 2.0 and has already enabled real-world mathematical discoveries
• Versioned, frozen subsets ensure stable and reproducible model comparisons
• The living repository continues to grow, with contributions from an active community
• Future work includes expanding coverage to computer science and physics, improving metadata, and automating misformalization detection in GitHub CI

The authors hope the work will drive the expansion of formalized mathematics through its living repository and continuous upstreaming of new definitions to Mathlib, ultimately helping accelerate the frontier of formal mathematical discovery.