Simple quality indicators for Lean libraries
Kim Morrison and Remy Degenne did an audit of a few formalization quality indicators across several Lean libraries. Our purpose was to see if we could quantify the common assumption that Mathlib is a high-quality library, while AI-generated formalizations perhaps less so, and to see if efforts to improve the quality of AI-generated formalizations could be measured.
There are many aspects of quality, and some are captured by mechanical checks like linters, or by community norms like Comparator challenges and formalization.yaml, or more diffuse social factors (is the repository maintained? Are people engaging with it?). We focused on a set of simple questions about individual theorems or files that can be assessed by AI judges. The indicators we used include:
-
does a theorem have hypotheses that could be removed? (not weakened, but completely removed)
-
is a theorem a duplicate or one-line consequence of something in Mathlib?
-
are there parts of proofs that appear several times in a file and could be turned into lemmas?
We evaluated Mathlib, Tau Ceti, Formal Frontier, Lean Pool, Anthropic's FLT, OpenAI's mathematical corpus and Axiom's CFSG proof (with more partial results for the last two).
Edit (2026-11-05): we've extended the audits to include Axiom's Stacks library.
For each of the indicators, we sample randomly theorems (for the first two) or files (for the third one) from the library, and ask an AI judge to answer the question. We then compute the percentage of theorems/files that are flagged by the AI judge, and also report 95% confidence intervals for the true rate. We found that the exact percentages depend on the AI model used (more expensive models report more issues), but that the groups and relative gaps are consistent across models.
The results in the tables below confirm the assumption that Mathlib is high-quality, show that Tau Ceti and Formal Frontier are not far behind on those metrics, and that the other libraries have generally higher percentages of flagged entries (although the OpenAI corpus has a very low rate of Mathlib duplicates). Tau Ceti and Formal Frontier are actively trying to take the lessons learned in Mathlib to guide the AI formalization process, and our takeaway from the results is that those efforts, while not perfect, are paying off.
The indicators we looked at are very partial (they do not measure anything about the quality of definitions, for a start), but they are easy to compute and give a preliminary signal. We would love to turn this into a more systematic audit. We have inference to run the evaluations but little time to further develop the methodology. If you are interested in helping, please reach out to us.
Results
Note: the OpenAI Math and AxiomMath CFSG results have higher uncertainty because of smaller sample sizes. Those results will be updated.
-
Unnecessary hypotheses:
Sample theorems uniformly at random, and ask whether any of the hypotheses could be removed without changing the statement of the theorem. Assumptions that can be weakened do not count: they need to be entirely removed.
| Library | Opus | Sonnet |
|---|---|---|
| Mathlib | 31/1,000 · 3.1% [2.2%, 4.4%] | 6/300 · 2.0% [0.9%, 4.3%] |
| Tau Ceti | 68/1,000 · 6.8% [5.4%, 8.5%] | 12/300 · 4.0% [2.3%, 6.9%] |
| Formal Frontier | 34/1,000 · 3.4% [2.4%, 4.7%] | 12/300 · 4.0% [2.3%, 6.9%] |
| Lean Pool | 150/1,000 · 15.0% [12.9%, 17.3%] | 39/300 · 13.0% [9.7%, 17.3%] |
| Anthropic FLT | 203/1,000 · 20.3% [17.9%, 22.9%] | 52/300 · 17.3% [13.5%, 22.0%] |
| OpenAI Math | 17/100 · 17.0% [10.9%, 25.5%] | 48/300 · 16.0% [12.3%, 20.6%] |
| AxiomMath CFSG | — | 70/300 · 23.3% [18.9%, 28.4%] |
| AxiomMath Stacks | 103/1,000 · 10.3% [8.6%, 12.3%] | — |
Mathlib, Formal Frontier and Tau Ceti have low rates of unnecessary hypotheses, while other libraries have a higher rates.
-
Results already available in Mathlib:
Sample theorems uniformly at random, and ask whether the theorem is already in Mathlib, or is a one-line consequence of a theorem in Mathlib.
| Library | Opus | Sonnet |
|---|---|---|
| Tau Ceti | 50/1,000 · 5.0% [3.8%, 6.5%] | 35/1,000 · 3.5% [2.5%, 4.8%] |
| Formal Frontier | 46/1,000 · 4.6% [3.5%, 6.1%] | 45/1,000 · 4.5% [3.4%, 6.0%] |
| Lean Pool | 68/1,000 · 6.8% [5.4%, 8.5%] | 58/1,000 · 5.8% [4.5%, 7.4%] |
| Anthropic FLT | 137/1,000 · 13.7% [11.7%, 16.0%] | 118/1,000 · 11.8% [9.9%, 13.9%] |
| OpenAI Math | 1/100 · 1.0% [0.2%, 5.4%] | 8/300 · 2.7% [1.4%, 5.2%] |
| AxiomMath CFSG | — | 15/300 · 5.0% [3.1%, 8.1%] |
| AxiomMath Stacks | 64/1,000 · 6.4% [5.0%, 8.1%] | — |
OpenAI Math did a very good job of avoiding duplicates with Mathlib, while Anthropic FLT has a notably high rate of duplicates which seems mostly due to a frequent use of abbreviations for special cases of Mathlib declarations, about which lemmas are then re-proven. The other libraries are in between.
-
Repeated proof machinery in a file:
Sample files uniformly at random, and ask whether there are parts of proofs that appear several times in the file and could be turned into lemmas.
| Library | Sonnet |
|---|---|
| Mathlib | 60/372 · 16.1% [12.7%, 20.2%] |
| Tau Ceti | 64/372 · 17.2% [13.7%, 21.4%] |
| Formal Frontier | 128/372 · 34.4% [29.8%, 39.4%] |
| Lean Pool | 180/372 · 48.4% [43.4%, 53.5%] |
| Anthropic FLT | 189/372 · 50.8% [45.7%, 55.9%] |
| OpenAI Math | 154/372 · 41.4% [36.5%, 46.5%] |
| AxiomMath CFSG | 162/300 · 54.0% [48.3%, 59.6%] |
| AxiomMath Stacks | 118/372 · 31.7% [27.2%, 36.6%] |
Mathlib and Tau Ceti have the lowest duplication rates, AxiomMath Stacks and Formal Frontier are in the middle, and the other libraries have higher rates.
We started testing other models, and did a few second passes to check the flags, but lots of work remains. All the results, prompts and other details are available in the lean-quality-indicators repository.