Taming a 40-Minute Lean CI: Three Rounds, Three Wrong Suspects

Our Lean 4 + mathlib project used to take 41 minutes for every single PR in CI. Now, the worst-case scenario of rebuilding the heaviest files from scratch takes 12 minutes, while an ordinary PR finishes in just a few minutes with incremental building. The improvements came through three rounds, each following a similar structure: problem, hypothesis, verification, and fix.

Spoiler alert: all three times, the first hypothesis – the cause our intuition pointed to – turned out to be incorrect. The main solution lies in profiling, which systematically dismissed our hypotheses. To understand this story, you don't need to know Lean; I'll explain the key concepts as they come up. Most of the measurements and implementations came from AI agents, with my involvement mainly in approving numeric targets and accepting the results.

Background: The project involves AlgebraicArchitectureTheoryV2, a formal verification of a software architecture theory using Lean 4. The project relies on five key components: Term (a proof assistant), mathlib (Lean's extensive mathematics library), Lean's build tool (similar to cargo for Rust or npm for JS), Lean's build process (per-file elaboration emitting .olean artifacts), and the kernel axiom audit, which ensures every theorem is genuinely proved.

Round 1: The axiom audit, 7m 11s → 11s

Problem: Every theorem in Lean is derived from axioms and checked by the kernel (a trusted checker). However, Lean has an escape hatch called 'sorry' that allows users to plug in unproven propositions as axioms. To ensure every declaration is proved, the project runs an axiom audit for each declaration, checking that the set of axioms it reaches stays within three standard axioms.

Hypothesis: The audit's slow performance was due to a single giant file containing 5,000+ lines of audited declarations. Splitting this file should improve performance.

Verification: We measured where the time was spent. Contrary to our hypothesis, the time was not spent on the big file itself. It was primarily due to how the audit was called – the collectAxioms function performed the dependency graph walk from scratch for every declaration, even though they shared the same foundation (mathlib). This resulted in O(declarations × graph) complexity, making the audit slower than the build process.

Fix: We implemented a two-phase approach. The success path involved sharing a visited set across all declarations, allowing the graph to be traversed only once. If a non-standard axiom was found, we would fall back to the classic per-declaration walk to attribute responsibility.