Technical Summary: Formal Conjectures

Problem Statement

As automated reasoning systems, particularly Large Language Models (LLMs), advance, existing benchmarks for mathematical reasoning face critical limitations:

1. Data Leakage: Solutions to benchmark problems often appear online, making it difficult to distinguish genuine reasoning from memorization.
2. Secretive Evaluation: To prevent leakage, some benchmarks keep evaluation sets private, hindering open and reproducible research.
3. Oversimplified Criteria: Many benchmarks rely on verifying simple, machine-checkable final answers (e.g., numbers) rather than complex, multi-step proofs.
4. Saturation: Existing formal benchmarks (e.g., MiniF2F, PutnamBench) are becoming saturated, with models routinely solving over 99% of problems, failing to measure progress on research-level mathematics.

There is a pressing need for a zero-contamination, evolving benchmark of research-level mathematical problems formalized in a machine-checkable language to accurately evaluate the capabilities of AI systems in formal mathematical discovery.

Methodology

The authors introduce Formal Conjectures, an open-source, evolving benchmark consisting of 2,615 mathematical problem statements formalized in Lean 4 using the Mathlib library.

Dataset Composition

The benchmark is divided into two primary categories:

• Research Open (1,029 problems): Unsolved conjectures sourced from active research areas (e.g., Erdős problems, Kourovka Notebook, arXiv, MathOverflow). These serve as a zero-contamination testbed for proof discovery, as no solutions exist in training data.
• Research Solved (836 problems): Established theorems with known informal proofs, used to benchmark auto-formalization capabilities.
• Other Statements (750 problems): Includes textbook-level problems, API definitions, and test lemmas to validate formalization correctness.

Formalization Pipeline and Quality Control

To ensure fidelity and minimize misformalization, the project employs a rigorous collaborative pipeline:

• Human-in-the-Loop Review: Every contribution undergoes code review by humans with both Lean expertise and domain-specific mathematical knowledge.
• AI-Assisted Auditing: Automated theorem provers (e.g., AlphaProof) and LLMs are used to attempt proofs and disproofs. Successful disproofs of "solved" problems or failures to prove open problems often reveal misformalizations.
• Misformalization Taxonomy: The authors define a three-level taxonomy for errors:
  1. Translation: Errors in translating an accurate informal statement to Lean.
  2. Underspecified: Errors where the informal statement lacks necessary detail.
  3. Source: Errors where the informal source text itself is incorrect or ambiguous.
     To date, 291 misformalizations have been identified and fixed.
• answer(sorry) Mechanism: A custom Lean elaborator separates the discovery of a specific answer (e.g., a number or truth value) from the proof of its correctness. This allows solvers to replace answer(sorry) with a concrete value (e.g., True, False, or a number) before attempting the proof, decoupling value discovery from verification.
• @[formal_proof] Attribute: To keep the repository lightweight, proofs for solved problems are often linked externally rather than stored directly, using attributes to track proof status (internal, linked Lean 4, or other systems).

Evaluation Framework

The benchmark utilizes the Lean 4 kernel for objective, rigorous verification. A solution is correct if and only if the kernel accepts the proof term without relying on forbidden axioms (like sorry).

• Frozen Subsets: To enable stable, reproducible comparisons despite the repository's evolving nature, the authors provide frozen subsets: FC100OpenSet1 (100 open problems) and FC100SolvedSet1 (100 solved problems).
• Versioning: Releases are tagged with a two-part naming scheme (e.g., bench-v1-lean4.27.0) to pin specific problem sets against specific Mathlib/Lean toolchains.

Key Results

The paper reports baseline results on the frozen subsets using state-of-the-art systems:

• FC100OpenSet1 (Proof Discovery): As of the first tagged release, the baseline for all systems is 0%, confirming the zero-contamination nature of the set.
• FC100SolvedSet1 (Auto-formalization):
  • AlphaProof (1k simulations): 45.0% solve rate.
  • AlphaProof (16k simulations): 50.0% solve rate, demonstrating a clear scaling signal with increased compute.
  • DeepMind Prover Agent (dev version): 66.0% solve rate, illustrating improvements in model architecture and methodology.

The authors note that the benchmark has already facilitated real-world mathematical discoveries, including the resolution of specific open conjectures (e.g., Erdős Problem 124), where AI-generated proofs served as an auditing mechanism to refine the formal statements.

Significance and Claims

The paper positions Formal Conjectures as a necessary evolution in AI evaluation for mathematics:

1. Zero-Contamination Benchmark: It provides the first large-scale, open, and rigorous testbed for genuine mathematical discovery on research-level problems, eliminating data leakage concerns.
2. Unified Interface: It acts as a central hub connecting mathematicians who formalize problems with AI systems attempting to solve them, facilitating simultaneous auditing and rapid dissemination.
3. Iterative Improvement: The framework uses AI-generated proofs and disproofs as a feedback loop to iteratively improve the fidelity of the benchmark itself, correcting misformalizations in both the repository and the original informal literature.
4. Climbable Signal: By providing frozen subsets and versioned snapshots, it offers a standardized, reproducible way to measure the "climbable signal" of automated reasoning capabilities as models improve.
5. Expansion of Formalized Math: The project contributes to the broader formal mathematics ecosystem by upstreaming necessary definitions and lemmas to Mathlib via the FormalConjecturesForMathlib directory.

The authors conclude that this resource aims not only to measure current progress but to accelerate the frontier of formal mathematical discovery by bridging human expertise and automated reasoning.