Our Lean 4 + mathlib project used to spend 41 minutes in CI on every single PR. Today, the worst case — rebuilding the heaviest files from scratch — takes 12 minutes, and an ordinary PR finishes in a few minutes on an incremental build. What we fixed Before After Kernel axiom audit 7m 11s 11s An ordinary PR 41m (full rebuild, always) a few minutes (incremental) Worst case (heaviest files fully rebuilt) 41m (same) 12m This article re...