Every renamed Mathlib name in your project, with its replacement.

Paste a Lean project from GitHub. Leanbump reads its pin and lists every deprecated or renamed Mathlib name it uses, file and line, with the replacement. On the 7 pilot projects it found 45 of the 58 lines where the compiler printed a deprecation warning. No account, no build, a few seconds.

Scan your project

Public repositories. Try b-mehta/PrimeCert.

Look up a name

What a bump did to a real project

PrimeCert moved from Mathlib v4.31.0 to v4.35.0. The first lake build after the bump produced 8 errors in 2 files. After repair, lake build passes, and every change is labelled: signature change, rename or reproof. Two rebuilds. The diffs are published.

Read the PrimeCert repair See all 8 projects

Where the work really is

Across the 7 pilot projects that broke, 145 raw build errors followed the bump: changed lemma statements, new upstream names that clash with local ones, deleted simp lemmas. Those need a repair, not a rename, and the benchmark shows how each was repaired: 5 of the 7 pass lake build after repair. The renames are the part Leanbump hands you in one pass, before you open a single error.

Start free

The scan, the rename lookup (17,917 deprecated Mathlib names across v4.0.0 to v4.35.0) and the project history are free today. See the plans.