What a Mathlib bump breaks in real projects

5 of 7 projects that broke on a Mathlib bump now pass lake build after repair; 2 of those 5 needed a statement changed. Every diff is published, and every number comes from the compiler.

The renames are the cheap part. Across the 7 failing projects, none of the 145 raw errors named a deprecated alias with a replacement: they were a new Mathlib declaration clashing with a local one, a lemma that gained a hypothesis, a changed simp normal form, a coercion that no longer unfolds. Each row below shows what changed in Mathlib for that project and the labelled repair: rename, signature change or reproof.

How to read this

• Repair arm A was the session that also diagnosed each case, so it is not blind. Blind agent runs (a fresh agent given only the compiler output) were 2 of 2, on the two smallest cases (PrimeCert and DirichletProblem).
• Passing means the last lake build exits 0. A passing project can still differ from yours in what it proves: 2 of the 5 passing repairs added a hypothesis to a statement (PrimeCert, LML) or lost a declaration Mathlib does not have (0 declarations); 2 only removed 11 local copies that Mathlib now provides (each checked at the target tag). Those rows say so.
• The scan on these projects. On the 7 failing projects the scan flags 0 of 145 error lines and 45 of 58 deprecation-warning lines; in the files the build reached, 11 of 56 flagged lines carry neither (the likely false positives). The 12 warning lines it does not flag are deprecations in Lean core (if_pos, dif_neg, Bool.and'), outside the Mathlib name map; 1 was a Mathlib name it missed. Error lines are mostly not names: the scan does not claim to predict them.
• How the projects were chosen. Projects the Mathlib downstream dashboard lists as incompatible with a newer Mathlib, so the break rate is higher than for a random Lean project.
• Time to bump. The projects split in two. Maintainers who track Mathlib weekly (LML 2, DynamicalSystems 2.5 days median from a Mathlib release to their own pin commit) stay current. PrimeCert (24), BrauerGroup (21) and ClassFieldTheory (18.5) wait weeks.
• Raw error counts are a lower bound. Lean stops a failing module, so its dependents appear only after it is fixed.
• Agent minutes are wall-clock estimates of the repair session, not a maintainer's hours.
• Eight projects is a pilot: results are stated as "N of M", never as a rate. BrauerGroup is only partly repaired and ClassFieldTheory was not attempted; both are shown.

Re-run it yourself

Each project page lists the exact commands. The whole benchmark, with a Lean toolchain installed through elan:

git clone https://github.com/leanprover-community/mathlib4  # a local mirror speeds up every case
source bench/env.sh
python3 bench/lbbench.py setup primecert
python3 bench/lbbench.py build primecert
python3 -I bench/results.py

The scripts and every recorded run are in the benchmark archive: README, results.json.

Is your project in here, and is a row wrong?

Every project here is a public repository. If a row is wrong, send the correction. If you would like your project taken off this page, say so and it is removed.

Correct a row Remove my project

Check your own project

Paste a GitHub address and get every deprecated or renamed Mathlib name in it, file and line, with the replacement. Scan a project