Formal Conjectures ships 1,029 open math problems in Lean 4

A quieter release than the usual model launch, but arguably the more interesting one for anyone tracking what "AI at math" actually means in practice. A team including Moritz Firsching, Eric Wieser, Blaise Agüera y Arcas, and Pushmeet Kohli has posted on arXiv a benchmark called Formal Conjectures: 2,615 problem statements written in Lean 4, of which 1,029 are open research conjectures and 836 are already solved.

The design idea is straightforward and worth naming. If your benchmark is a fixed pile of textbook exercises, models eventually see them in training data and your leaderboard slowly becomes a memorization test. If your benchmark is live, unresolved mathematics, that failure mode goes away by construction. The 1,029 open conjectures form the "zero-contamination" half of the set, and the 836 solved problems are there to test autoformalization, the mechanical step of translating a human-language theorem into machine-checkable Lean.

The authors frame the benchmark as a collaboration surface rather than a static file. They describe AI-generated proofs and disproofs as an auditing mechanism that iteratively improves the fidelity of the problem statements themselves, and they say the dataset has already enabled new mathematical discoveries, including the resolution of open research conjectures. Everything ships under Apache 2.0.

The honest caveat is that the abstract does not tell you which provers have posted results here, how the open set will be replenished as it gets picked off, or how the review process handles a formalization that turns out to be subtly wrong. Those are the questions the community will actually litigate over the next year, and none of them are answered by the paper on its own.

For prover teams, the shift is that the yardstick is no longer a bounded pile of competition-style exercises; it is a growing frontier that mathematicians themselves are curating. That is a different kind of eval, and if it holds up it changes what "beating the benchmark" is even supposed to mean.