scottnarmstrong/leanautoformalizationskills/lean-elaboration

Lean Elaboration Improvement

This guidance distills repeated A/B measurements from large Lean 4 and Mathlib repositories. The examples preserve useful magnitudes and negative results without carrying private project history into the workflow. Full evidence: references/evidence.md.

Companion skills: lean-elaboration-test (the repo-level measurement snapshot — run it first to find candidates), lean-learnings (ambient-space and reusable Mathlib guidance).

Rule zero

Improve elaboration by measurement, not by taste. A proof that looks cleaner can be slower; a verbose proof can be much faster. The measured studies' costliest mistakes were interventions rolled out by analogy or aesthetics: a "cleanup" file-split added +360s wall-clock in one afternoon; a cache rolled out to a sibling file regressed it. Every intervention gets a profile before and an A/B after, and speculative edits that don't move the numbers are reverted before commit.

The loop

1. Find candidates at repo level — run the lean-elaboration-test snapshot;

take the heavy tail (files ≥10s/≥20s/≥30s build wall-clock) from the build log.

1. Confirm each candidate with a warm own-file profile — build wall-clock

includes upstream rebuilds, olean writes, and contention; it overstates own-file cost by ~2.5× routinely. The ground truth is: ``bash <repo-approved-lean-command> --profile <Root>/<Path>/File.lean 2>&1 | tail -25 ` Read the cumulative profiling times block. A "50s file" usually has 1–3s of fixable cost. If import` dominates, the file is not fixable locally — the lever is upstream, or in what this file imports; do not touch its proofs.

1. Route by dominant phase (dominant = >5s AND >25% of total):

3b. Before touching any proof, ask whether the cost is even in the proof. Replace the suspect declaration's body with sorry and re-profile. If the phase total is unchanged, the cost is in elaborating the statement, and no tactic, simp, cache, or import lever can touch it — go to lever 8. This one-minute test prevents whole afternoons of proof tuning against a signature problem. (Measured: a file at 9.55s elaboration read 9.57s with both proof bodies sorryd.) A sibling declaration with the same hypotheses but a cheaper conclusion is the control that confirms it.

Locating anonymous events. --profile often reports statement cost as bare elaboration took 5.3s with no declaration name. Bisect by inserting #exit at successive line numbers in an untracked copy and re-profile. A short bisection usually pins the cost to one declaration without editing tracked source.

1. Apply ONE intervention — never stack changes before measuring.
2. A/B and keep-or-revert — compare a baseline and one edited variant of

the same file; use at least three runs if relying on wall-clock. Profile deltas are wall-clock-noise-immune and win when they disagree. Keep the edit only if the relevant phase drops ≥2s (or ≥10%) without moving cost somewhere worse. Three consecutive failures of one technique on a file family = stop applying that technique to the family.

The levers, ranked by reliability

1. Import-load reduction in consumers (the biggest structural lever)

Remove/narrow imports in the files that consume a heavy module; never "quarantine" by splitting the upstream file while re-exporting everything (that failed: same content, 2.5× cost across three files). Verify symbol-level: enumerate the imported module's public API by grep and check usage — naive candidate lists have a ~50% false-positive rate (load-bearing instances/tactics), so build-verify each removal in the first pass, not a follow-up. Avoid umbrella imports: import the precise provider file, not the namespace facade. Measured: one consumer-side sweep cut whole consumer groups 22–46% and a single file −59% with zero content change.

2. nlinarith/linarith elimination from arithmetic closers

Once nonlinear facts are named hypotheses, close with monotonicity lemmas (add_le_add, sub_le_sub_right, mul_nonpos_of_nonpos_of_nonneg) and calc; use positivity for pure sign goals; prefer linarith only [...]. Measured: interpretation 14.6s → 3.15s; a file's nlinarith count 7 → 0 with own-file cost halved. Near `Real.rpow`/`Real.exp`: extract the pure-algebra core as a standalone lemma over abstract reals so numeric tactics never enter transcendental terms (set-bound exp-lets unfold inside nlinarith and cause expensive weak-head normalization; use clear_value or opaque variables).

3. Targeted simp narrowing — bimodal, so check the precondition

simp/simpa → simp only, or better exact/rfl/dsimp [defs]; rw [law] for definitional bridges. Works spectacularly on files where individual simp calls exceed ~1s (18.8s → 0.3s). Null result as a blanket file-scope sweep where peaks are <1s (−0.2s against ±3s noise — reverted). Screen with the profile's per-call simp took Nms lines; skip calls under ~200ms. Commit only on >3s sustained file-level A/B.

4. Head-class instance caches (private instance ... := inferInstance)

For files with big variable/include blocks (≥50 lines, referencing things like [NeZero d], [IsProbabilityMeasure P], or project-type-indexed instances): cache each recurring head-class once so resolution happens once per file and propagates via olean to importers. Guards, all mandatory — learned from a rollout in which 4 of 6 planned caches were inapplicable and 1 of the remaining 2 was null:

• Only above the 5s floor: below 5s cumulative typeclass inference, caches

typically hurt (disambiguation overhead).

• Only for CLOSED instance searches. A cache cannot terminate an open

search whose goal head is still a metavariable (e.g. SMul ℝ ?α from elaborating • before the type family is known) — it only lengthens the candidate list. Diagnose with trace.Meta.synthInstance before choosing: closed search → cache; open search → type ascriptions at the elaboration-order pinch (measured: 8→0 SMul events, −91% typeclass, where the prescribed cache was refuted by A/B).

• Placement is load-bearing: top-level / namespace-level, **outside any

section ... variable block** — section scoping hides the cache and it silently does nothing (the operative distinction is top-level vs section-scoped, not namespace membership).

• Leaf-first: in an import chain, cache the leaf only; a redundant cache

upstream of an already-cached file regressed +1.2s.

• Cache only head-classes the file actually uses; never derived classes.
• Never roll out by analogy: identical brackets gave PASS on one file and

FAIL on its direct sibling. A/B each file.

• Propagation check: if downstream consumers improve <0.5s, the cache didn't

propagate — placement is wrong.

• When creating a structurally similar file, check whether it should import a

cached provider or needs its own measured cache. Several cacheless variants once added more than 1,000 seconds of CPU in one build.

5. Leaf splitting with DAG-shaped imports

Splitting pays only when it changes what gets loaded or unblocks parallelism: push the parent's heavy imports down to only the sub-modules that need them (grep symbol counts per line range), make sub-module edges a DAG not a chain, and let independent halves be siblings. Splitting a file while consumers still transitively need all parts is a pure loss (import preamble + olean overhead ×N). File-size discipline (~1,000–1,500-line ceiling) is about edit-iteration latency and parallelism, not cumulative CPU.

6. Standalone lemma extraction / clean-context elaboration

Extract an expensive mathlib call or a heavy algebraic step into a private lemma with a minimal signature: instances resolve once, the call site is a cheap application, and each lemma gets its own heartbeat budget. This is also the escape from single-expensive-unification walls. Related: keep membership/proof arguments out of heavy dependent surfaces; avoid partially-applied heavy theorems with pinned late implicits; prefer small constructor lemmas over monolithic wired-up abbrevs.

7. Statement hygiene that doubles as perf

• >10 named hypotheses on a theorem → compress (structure bundle, typeclass

instances, caller-side norm_num, definitional lets). LLM agents don't feel signature pain — one theorem reached 85 hypotheses / 539-line signature before anyone flagged it.

• Unused section variables / auto-bound instances are per-declaration

instance-search cost; keep the linter at zero.

• rfl _def lemmas instead of simp only [thedef] unfolding of heavy

definitions.

8. Fold a hypothesis type to the abbrev its consumer expects

The single highest-yield statement-level fix found so far (−98% elaboration, three times). Precondition: a hypothesis is written in fully unfolded form, and the conclusion feeds it into a dependent term whose own signature declares that argument through an abbrev. Lean then discharges the unfolded-vs-abbrev defeq for the entire binder block, repeatedly.

-- costly: hypothesis unfolded, but `perturb` declares its arg as `FluxIntegrable U a u`
theorem foo (hu : ∀ φ : Test U, IntegrableOn (fun x => ⟪A x (u.grad x), φ.grad x⟫) U) :
    P (perturb u w hu) = ...
-- cheap: same proposition, stated the way the consumer expects
theorem foo (hu : FluxIntegrable U a u) : P (perturb u w hu) = ...

Because the abbrev is definitionally the term, this is notation, not semantics: the statement is unchanged and no consumer needs touching. Verify with a full build anyway. The tell is verbosity plus dependent use — a sibling with the identical unfolded block but no dependent consumer costs ~0 ms, so do not "clean up" verbose binders that nothing consumes; you will gain nothing.

Sweeping for it: grep is too weak (the unfolded text varies with binder names and formatting). Parse instead — for each declaration, split the signature at the top-level : with a paren-depth counter, then flag any explicit binder whose type is long (>90 chars) and contains fun/∀ and whose name occurs in the conclusion. On a 600k-line repo that yielded 42 candidates in 22 files; profiling showed all but three had elaboration <450 ms. Expect a low hit rate and profile before editing — the detector finds the shape, not the cost.

9. Name the function in congr

congr/congr 1 searches for a congruence decomposition. When you already know which function is being peeled, name it: refine congrArg f ?_. Same subgoals, no search.

congr 1                                  -- 5.6s
refine congrArg (· ^ (1 / p.toReal)) ?_  -- ~0s, goal `X = Y` as before