formal-conjectures: a benchmark of statements without proofs

Statements without proofs, on purpose

Formal Conjectures is a collection of formalised statements of conjectures in Lean, using mathlib. The description of the problem it addresses is precise. There is already a growing corpus of formalised theorems including proofs, but there is a lack of open conjectures where only the statement has been formalised. That gap is what this repository fills, and the project lists three reasons why it matters. It could become a great benchmark for automated theorem provers and automated formalisation tools, because a prover needs a well-posed statement to attack and a machine-checkable way to tell whether it succeeded. It could help clarify the precise meaning of conjectures through formalisation, since writing the statement forces every hypothesis and every quantifier to be pinned down. And it could encourage the expansion of mathlib by highlighting needed definitions, which is a practical effect: if a conjecture cannot be stated because a definition does not exist yet, that gap is visible. The stated hope is that this initiative will form the seed of a much richer dataset of formalised conjectures.

The accuracy problem, and the plan that addresses it

There is a section in the README devoted to a problem that has no technical solution, and it is the most important thing to read before using this data. Formalizing mathematical statements without proofs is inherently challenging, and subtle inaccuracies can arise where the formal statement might not perfectly capture the nuances of the original conjecture. A mistyped hypothesis or a slightly weakened quantifier turns a hard problem into a different, easier one, and any prover that solves it produces a result about the wrong statement. The stated mitigation is human review of contributions, careful rather than automated, with a plan to periodically leverage AlphaProof to help identify potential misformalisations. That is a sensible division of labour. A model that is good at finding counterexamples and short proofs is a good instrument for checking whether a statement is too weak, and a human is what catches a statement that is faithful to the prose but not to the intended mathematics. The repository also points to STATEMENTS.md and PROOFS.md at the root, and the contributing guide covers attribute usage and style, which is where the review process is spelled out in detail.

How to build it, and what the directory layout means

It is a Lean 4 project managed with lake, with mathlib as a dependency. The getting started requirement is to install elan, lake, lean and, if you want it, VS Code, and then run two commands:

lake exe cache get
lake build

The first fetches the prebuilt cache of compiled mathlib artefacts, and the second builds the project. The directory structure is organised by the type of source of the conjectures, and two directories are special. FormalConjecturesUtil contains utilities such as the category attribute, the question attribute and some linters, which is the machinery that keeps the dataset machine-readable. FormalConjecturesForMathlib contains code that is potentially suitable to be upstreamed to mathlib, and it follows mathlib's own directory structure. The reason for that split is explained under versioning: definitions that a conjecture needs but mathlib does not yet have can be added there, so adding a problem statement is not locked to the mathlib release cadence. The rest of the tree has the usual research-repository furniture, with FormalConjectures/ for the statements themselves, FormalConjecturesTest/ for tests, docbuild/ and site/ for the generated documentation, scripts/ for the automation, plus a devcontainer and a Gitpod configuration for a one-click environment.

Tags that separate the release from the benchmark

The versioning scheme is the part of this repository most likely to affect your work, and it handles two different timelines that are easy to confuse. The first is the library version. The repository tracks the monthly tagged releases of mathlib, which correspond to Lean releases, rather than tracking mathlib master, and when lean-toolchain is updated on main, a GitHub Actions workflow automatically adds a git tag of the form v4.{X}.{Y}, following mathlib's tagging convention. The second is the benchmark version, tagged bench-v{N}-lean4.{X}.{Y}, where v{N} identifies the set of problems included in the benchmark and lean4.{X}.{Y} identifies the Lean 4 toolchain used for that snapshot. The rule that matters is that tags are immutable: fixes to misformalizations are never patched into an existing benchmark version but instead go into v{N+1}. That is the correct choice for a benchmark, because a benchmark whose contents change under you is not a benchmark, and it means every result produced against bench-v1 is comparable with every other result produced against bench-v1. It also means the correction of a wrong statement is not visible to anyone pinning the old tag, which is a trap worth knowing about. The only release listed for this repository is bench-v1-lean4.27.0, and the last push was on 2026-10-15.

Attributes are how a statement declares what it is

The metadata that makes the collection machine-readable lives in attributes rather than in prose, and the README points at CONTRIBUTING.md for the full meaning of the four that matter. A statement can carry a category attribute, a formal_proof attribute, an AMS attribute and a question attribute. The category and question attributes are defined in FormalConjecturesUtil/Attributes/Basic.lean, and the linters in the same directory exist to enforce the conventions. For someone building a prover, a filter over categories and the question attribute is the difference between a training set with useful labels and a pile of Lean files. The reference implementation is the associated paper, Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics, and the README gives a BibTeX entry for it along with one for the repository itself, so citing the data is a matter of copying a block rather than writing a reference from scratch:

@misc{FormalConjectures,
  author       = {{The Formal Conjectures Authors}},
  title        = {{T}he {F}ormal {C}onjectures {R}epository},
  year         = {2025},
  url          = {https://github.com/google-deepmind/formal-conjectures},
}

The description of the corpus as open and evolving is accurate in both words. It is open because the contributions go through a public process with a contribution guide, and evolving because the benchmark version is designed to move forward as problems are added, removed, or corrected.

Licensing is layered, because the sources are

The licensing section is more involved than a single file, and that is deliberate. The software is under the Apache License 2.0, and all other materials are under Creative Commons Attribution 4.0 International. On top of that, the content may be based on third party sources and may include third party content, with the original source for each conjecture indicated by a URL within the source file. The specific cases are listed. Material from Wikipedia articles, MathOverflow and the OEIS is released under Creative Commons Attribution-Share-Alike 4.0, which is the most restrictive of the set because share-alike propagates. Material from bbchallenge.org is used under CC-BY 4.0, and material from the Equational Theories Project is used under Apache-2.0. Material from arXiv is used under the licence applicable to the relevant paper, as indicated at the URL in the source file. The practical consequence for a user building a dataset is that a statement derived from an arXiv paper under a non-commercial or restricted licence may constrain what you can do with it, and the per-file URL is where you find out which case applies. The repository also states that the material is distributed as is, without warranties.

Where formal-conjectures is the wrong tool

The obvious misreading is to treat the repository as a library of results. These are statements without proofs, so nothing here has been verified in the sense a theorem has, and a solved file from an automated prover proves that particular formal statement, which is not the same as the original conjecture unless the formalisation is exact, and the project says it may not be. The second limit is the corpus size and its churn. The benchmark is seeded rather than complete, the stated hope is that it grows, and the immutable tag scheme means you have to pick a version and re-run when the next one lands. The third is the dependency weight. A Lean project with mathlib means a toolchain, an artefact cache download, and a build that can take a while, which is a heavy price for a team that just wants a list of problems in JSON. The fourth is the domain. A conjecture corpus is a benchmark for automated mathematical reasoning, so if your goal is to test a code completion model on functions, this is the wrong dataset. The fifth is the accuracy risk, which the project states openly: a statement that subtly differs from its source is a wrong answer waiting to be reported, and no amount of tooling removes that without human review.

Editorial conclusion

Adopt formal-conjectures if you are building or evaluating an automated theorem prover, an LLM-based formalisation tool, or a dataset of mathematics problems, and if you can tolerate statements that may not mean exactly what the original conjecture meant. Do not treat the repository as a source of proved mathematics, because a conjecture here is a statement with no proof, and the project itself warns that subtle misformalisations can occur. Before you use a snapshot, read the version tags carefully, since a bench-v tag is immutable and fixes only appear in the next version, and check the per-file source URL and licence before redistributing any statement.

Frequently asked questions

Official sources

1. google-deepmind/formal-conjectures on GitHub
2. License: Apache-2.0
3. Project website
4. README
5. Releases