DeepMind Unveils Formal Conjectures Dataset to Benchmark AI Theorem Provers

Google DeepMind has launched Formal Conjectures, an open-source repository dedicated to collecting formalised statements of mathematical conjectures using the Lean 4 theorem prover and its extensive mathlib library. This initiative addresses a critical gap in the landscape of formal mathematics: while there's a growing body of formally proven theorems, there's a distinct lack of openly available, formalised conjectures where only the statement, not the proof, has been captured.

The primary goal of Formal Conjectures is to serve as a robust benchmark for automated theorem provers and automated formalisation tools. By providing a curated dataset of unproven mathematical statements, the project aims to accelerate the development and evaluation of AI systems designed to tackle complex mathematical reasoning. Beyond benchmarking, the formalisation process itself helps clarify the precise meaning of conjectures, reducing ambiguity inherent in natural language mathematical descriptions. It also encourages the expansion of mathlib by highlighting definitions and theorems that are currently missing but necessary for formalising new conjectures.

The project is structured as a Lean 4 project managed with lake and depends on mathlib. Contributions are actively encouraged, with a detailed CONTRIBUTING.md guide outlining the process, file structure, and style guidelines. Acknowledging the inherent challenges in formalising statements without proofs, the project emphasizes careful human review of all contributions. Furthermore, DeepMind plans to periodically leverage its AlphaProof system to help identify potential misformalisations, ensuring the accuracy and reliability of the dataset.

The repository's structure includes FormalConjecturesUtil for general utilities and FormalConjecturesForMathlib for code that might eventually be upstreamed to mathlib. This allows for flexibility in adding new definitions required for conjectures without being strictly tied to mathlib's release cycle. Versioning tracks monthly mathlib releases, and stable benchmark snapshots are tagged using a specific format (bench-v{N}-lean4.{X}.{Y}). These tags are immutable, meaning any corrections to misformalisations result in a new benchmark version, ensuring consistency for evaluation purposes. The project is licensed under Apache 2.0 for software and CC-BY for other materials, with careful consideration for third-party content licensing.