Formal Conjectures
Formal Conjectures, from Google DeepMind, states open and solved mathematical problems in Lean, with a site at https://google-deepmind.github.io/formal-conjectures/. This chapter maps it as read at commit 2055e5ad (2026-11-06), Lean toolchain v4.33.1: a part per source folder of FormalConjectures/, an article per problem file and, in it, a card per statement.
Every statement carries one category attribute: research open, research solved, textbook, API or test. The articles show the first three, 5,132 statements in 1,814 articles: 1,873 open and stated without proof; 3,012 research solved, 151 of them proved here and 1,099 of the rest with a formal_proof link to a proof elsewhere; 247 textbook results, 132 of them proved here. Besides these, 1 definition carries a category attribute; its card says it is not a statement. The 2,673 test and 630 API statements are counted in their problem's article, not shown. 14 problem files state none of the first three and have no article; their folder's page lists them.
A card's status line reads the statement's category, its formal_proof links and whether the text of its proof in the file contains sorry: “Open: stated without proof.”; “Solved: stated here; a Lean proof is at …” (or “a proof in another system is at …”) when a link gives one, and “Solved: stated here without proof.” when none does; “Textbook result, stated without proof.”; and “Proved here.” or “Textbook result, proved here.” when the proof's text holds no sorry, which, like Formal Conjectures' own hasSorryFreeProof, says nothing of the statements that proof uses. Formal Conjectures marks a link formal_conjectures when the proof fills this statement as written, and lean4 when the problem is solved in Lean elsewhere, perhaps as an equivalent statement.
No Lean is run for this chapter. Statements, docstrings and attributes are read from the source text: a statement is a named declaration with a category in the @[...] list right before it, its Lean statement runs to the := that starts its proof, and its name is read under the namespaces it sits in. A statement with no name, an example, or a private one is left out, as Formal Conjectures' own site leaves them out. The articles have no dependencies: edges between statements need Lean.
Two indexes link the articles: by subject, from the AMS attributes' top-level classes of the Mathematics Subject Classification (43 subjects), and the FC100 subsets, Formal Conjectures' benchmark lists.
The docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at commit 2055e5ad, under its Apache-2.0 license, with each article naming its file. Formal Conjectures asks that the Erdős problems' docstrings follow erdosproblems.com; the Erdős part says how, and each Erdős article links its problem's page there.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.