Generated by scripts/mathlib_gaps.py from docs/1000.yaml (https://raw.githubusercontent.com/leanprover-community/mathlib4/master/docs/1000.yaml) — snapshot 2026-08-06. Do not hand-edit; regenerate.
Mathlib keeps docs/1000.yaml: the Wikipedia list of famous theorems, each entry tagged with the Lean declaration that proves it. An entry with no decl: field is the library stating, in its own tree, that the theorem is wanted and unbuilt. That is the contribution surface — not a guess about what would be welcome, but a written record of it.
| count | |
|---|---|
| entries tracked | 1179 |
formalized (decl: present) | 209 |
| unformalized | 970 |
| unformalized ∩ this lab's subject matter | 32 |
A caveat that matters before anyone starts typing: absence from this file is not absence from Mathlib. 1000.yaml tracks famous theorems only, and its decl: fields lag merges. Always confirm with a code search and an open-PR search before claiming a target.
Unformalized entries within this lab's reach
| Wikidata | theorem |
|---|---|
| Q2376918 (https://www.wikidata.org/wiki/Q2376918) | Abelian and Tauberian theorems |
| Q4751118 (https://www.wikidata.org/wiki/Q4751118) | Analytic Fredholm theorem |
| Q4783822 (https://www.wikidata.org/wiki/Q4783822) | Arithmetic Riemann–Roch theorem |
| Q4827308 (https://www.wikidata.org/wiki/Q4827308) | Auxiliary polynomial theorem |
| Q872088 (https://www.wikidata.org/wiki/Q872088) | Boolean prime ideal theorem |
| Q205966 (https://www.wikidata.org/wiki/Q205966) | Critical line theorem |
| Q1196538 (https://www.wikidata.org/wiki/Q1196538) | Descartes's theorem |
| Q2533936 (https://www.wikidata.org/wiki/Q2533936) | Descartes's theorem on total angular defect |
| Q3527091 (https://www.wikidata.org/wiki/Q3527091) | Gromov's theorem on groups of polynomial growth |
| Q1899432 (https://www.wikidata.org/wiki/Q1899432) | Grothendieck–Hirzebruch–Riemann–Roch theorem |
| Q4455037 (https://www.wikidata.org/wiki/Q4455037) | Hardy's theorem |
| Q3075250 (https://www.wikidata.org/wiki/Q3075250) | Hardy–Littlewood maximal theorem |
| Q5656673 (https://www.wikidata.org/wiki/Q5656673) | Hardy–Littlewood tauberian theorem |
| Q5656674 (https://www.wikidata.org/wiki/Q5656674) | Hardy–Ramanujan theorem |
| Q7512855 (https://www.wikidata.org/wiki/Q7512855) | Hirzebruch signature theorem |
| Q4663326 (https://www.wikidata.org/wiki/Q4663326) | Hirzebruch–Riemann–Roch theorem |
| Q5988409 (https://www.wikidata.org/wiki/Q5988409) | Identity theorem for Riemann surfaces |
| Q6484331 (https://www.wikidata.org/wiki/Q6484331) | Landau prime ideal theorem |
| Q380576 (https://www.wikidata.org/wiki/Q380576) | Measurable Riemann mapping theorem |
| Q1196729 (https://www.wikidata.org/wiki/Q1196729) | Mertens's theorems |
| Q649469 (https://www.wikidata.org/wiki/Q649469) | Modularity theorem |
| Q386292 (https://www.wikidata.org/wiki/Q386292) | Prime number theorem |
| Q927051 (https://www.wikidata.org/wiki/Q927051) | Riemann mapping theorem |
| Q1752516 (https://www.wikidata.org/wiki/Q1752516) | Riemann series theorem |
| Q17104025 (https://www.wikidata.org/wiki/Q17104025) | Riemann singularity theorem |
| Q1974087 (https://www.wikidata.org/wiki/Q1974087) | Riemann's theorem on removable singularities |
| Q379048 (https://www.wikidata.org/wiki/Q379048) | Riemann–Roch theorem |
| Q17102744 (https://www.wikidata.org/wiki/Q17102744) | Riemann–Roch theorem for smooth manifolds |
| Q7333126 (https://www.wikidata.org/wiki/Q7333126) | Riemann–Roch theorem for surfaces |
| Q1632301 (https://www.wikidata.org/wiki/Q1632301) | Sturm's theorem |
| Q3983968 (https://www.wikidata.org/wiki/Q3983968) | Sturm–Picone comparison theorem |
| Q3527279 (https://www.wikidata.org/wiki/Q3527279) | Wiener's tauberian theorem |