This dashboard answers these questions about projects that depend on mathlib4:
- How far behind is the dependency revision? A scheduled workflow builds each registered downstream against the most recent mathlib commit (the target). The age column shows how many commits your pinned revision lags behind it.
- Which commit introduced the incompatibility? When the downstream is incompatible with the target, we run hopscotch to scan the mathlib history between the pinned revision and the target, to identify the first known bad commit — the earliest Mathlib revision incompatible with the downstream — and the last known good commit just before it.
- How much can I safely advance the dependency? The last known good commit is a safe upgrade target. The bump column shows the distance between it and the currently pinned revision.
Glossary
DownstreamProject tested updating the Mathlib dependency
TargetMathlib revision targeted in the latest validation run
CompatibilityCompatibility of the downstream with the target Mathlib revision
(based on the result of the latest validation run)
Last known goodLatest Mathlib revision compatible with the downstream
Last good releaseLatest Mathlib semver release tag compatible with the downstream
First known badEarliest Mathlib revision incompatible with the downstream
PinnedMathlib revision in the downstream's lake manifest
AgeDays between 'pinned' and 'target' (commit count below)
BumpCommits that can be safely advanced ('pinned' -> 'last known good')
Each run attempts to build the downstream project after updating its Mathlib dependency to the target revision. A failure in this build means something conflicts between the dependency and the dependent at that revision (an API change, namespace conflict, ...)
compatibleCompatible with the target Mathlib commit
incompatibleIncompatible with the target Mathlib commit
errorValidation job encountered an unexpected error
9
compatible
12
incompatible
0
errors
Tips:
Hover any badge or commit SHA to see details. Click on column headers to sort. Use the filter box to quickly find your project or filter by compatibility.
| Downstream | Pinned to | Age | Target | Compatibility | Last known good | First known bad | Bump | Last good release | Links |
|---|---|---|---|---|---|---|---|---|---|
leanprover-community/add-combi @ 67cdb70 | 1b6d405 | 1d (+39) | 1c1dadb | compatible | 1c1dadb | — | +39 | v4.30.0-rc2 (-761) | |
Whysoserioushah/BrauerGroup_new @ de83afa | 024965e | 168d (+5694) | 1c1dadb | incompatible | 024965e | ea3d89c | — | v4.26.0-rc2 (-136) | |
YaelDillies/cam-combi @ 13206c9 | v4.29.0 | 43d (+1396) | 1c1dadb | compatible | 1c1dadb | — | +1396 | v4.30.0-rc2 (+596) | |
fpvandoorn/carleson @ a3e427d | 1a4917a | 11d (+380) | 1c1dadb | incompatible | e6a5fb0 | a18abbe | +4 | v4.30.0-rc2 (-420) | |
YaelDillies/chandra-furst-lipton @ 56c75e4 | v4.29.0 | 43d (+1396) | 1c1dadb | compatible | 1c1dadb | — | +1396 | v4.30.0-rc2 (+596) | |
kbuzzard/ClassFieldTheory @ 6135bcb | 3bd2603 | 41d (+1303) | 1c1dadb | incompatible | 35bf175 | f51efbe | +80 | v4.29.0 (-93) | |
dwrensha/compfiles @ b2f588e | 53f8a93 | 0d (+26) | 1c1dadb | compatible | 1c1dadb | — | +26 | v4.30.0-rc2 (-774) | |
leanprover/cslib @ 608cbe1 | 6cf3ab1 | 13d (+424) | 1c1dadb | compatible | 1c1dadb | — | +424 | v4.30.0-rc2 (-376) | |
ImperialCollegeLondon/FLT @ 1b7fe98 | 229580e | 1d (+50) | 1c1dadb | compatible | 1c1dadb | — | +50 | v4.30.0-rc2 (-750) | |
leanprover-community/flt-regular @ 709a431 | master-2026-05-12 | 0d (+32) | 1c1dadb | compatible | 1c1dadb | — | +32 | v4.30.0-rc2 (-768) | |
YaelDillies/forbidden-matrix @ 98e3856 | v4.29.0 | 43d (+1396) | 1c1dadb | incompatible | 32df576 | f884e9d | +989 | v4.30.0-rc2 (+596) | |
google-deepmind/formal-conjectures @ 874f803 | v4.27.0 | 109d (+3783) | 1c1dadb | incompatible | v4.27.0 | 052a7e0 | — | v4.27.0 | |
YaelDillies/gibbs-measure @ 5630a66 | v4.29.0 | 43d (+1396) | 1c1dadb | compatible | 1c1dadb | — | +1396 | v4.30.0-rc2 (+596) | |
emilyriehl/infinity-cosmos @ 990f05c | ef921c9 | 170d (+5801) | 1c1dadb | incompatible | ef921c9 | 1543752 | — | v4.26.0-rc2 (-29) | |
marcelolynch/LeanDownstreamPlayground @ 45fa753 | v4.30.0-rc2 | 24d (+800) | 1c1dadb | incompatible | 1ec8620 | 4049cbf | +396 | v4.30.0-rc2 | |
YaelDillies/misc-yd @ d87cd76 | v4.29.0 | 43d (+1396) | 1c1dadb | incompatible | 8a623d7 | c6cdc1b | +105 | v4.29.0 | |
Paul-Lez/PersistentDecomp @ 4a5843f | v4.29.0 | 43d (+1396) | 1c1dadb | incompatible | 1692ef2 | 438f134 | +479 | v4.30.0-rc1 (+176) | |
leanprover-community/physlib @ caa62e0 | detached | 25d (+1396) | 1c1dadb | incompatible | — | a3fde50 | — | — | |
AlexKontorovich/PrimeNumberTheoremAnd @ 50c130a | v4.28.0 | 85d (+2981) | 1c1dadb | incompatible | 19564be | v4.29.0-rc1 | +36 | v4.28.0 | |
thefundamentaltheor3m/Sphere-Packing-Lean @ 4a74f24 | v4.29.0 | 43d (+1396) | 1c1dadb | incompatible | 08becba | 053a003 | +215 | v4.30.0-rc1 (+176) | |
YaelDillies/toric @ 41c4704 | 53f8a93 | 0d (+26) | 1c1dadb | compatible | 1c1dadb | — | +26 | v4.30.0-rc2 (-774) |