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

TL;DR

The paper introduces Formal Conjectures, a dynamic benchmark of formalized mathematical problems in Lean 4, aimed at evaluating and advancing automated reasoning systems in research-level mathematics.

Contribution

It presents a large, evolving dataset of formalized conjectures and solved problems, with a structured interface connecting mathematicians and AI systems, and provides baseline evaluation results.

Findings

Benchmark includes 2615 problems with 1029 open conjectures.

Demonstrated utility by solving open research conjectures.

Provides a standardized evaluation setup with baseline results.

Abstract

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.