lean4-automation-debugging

Failed Lean proofs, classified and repaired. Each case starts from a defective attempt, names the failure, applies the smallest repair that still means the intended mathematics, and compiles against pinned Lean 4 and mathlib.

Broken candidates stay in comments so they do not enter executable declarations. No sorry, admit, or custom axiom in project sources.

A proof failure is a true statement whose candidate proof does not close (type mismatch, rewrite match failure, missing instance, wrong tactic class, …). A semantic failure is a statement that is false, weaker than the intent, quantified in the wrong order, or proved only after changing the domain. Closing a different goal is not a repair.

Debugging steps I actually use

1. Read the exact target and the local context.
2. Identify types, including coercions; check ℕ vs ℤ vs ℝ.
3. Test exact / apply candidates; inspect the expected lemma with #check (and #print when the definition matters).
4. Use exact?, apply?, simp? as search, then delete them from the reviewed proof.
5. Reduce automation: named lemma, or a problem-class tactic (ring, omega, linarith).
6. Introduce intermediate have statements when the gap is semantic.
7. Separate a false statement from a failed search.
8. Compile the module, then lake build.

Several cases spell this out in comments (C12, C29, C35, C36, C49, C50). Search tactics are diagnostic. Reviewed proofs record the lemma they found; CI does not run exact?.

Tactics shown

Class	Tools
Goal closing	exact, assumption, apply, refine, constructor, intro, rcases/obtain, cases, contradiction
Rewriting	rw, ← direction, multi-rw, local vs at *, calc, congrArg, funext/ext
Simplification	simp, simp only, simp at, simp_all (discussed), simpa (rejected when unnecessary)
Arithmetic	norm_num, ring, ring_nf, linarith, nlinarith, omega
Search	#check, #print, exact? / apply? / simp? as diagnostics
General automation	aesop, grind compared with explicit proofs

Toolchain

Pin	Value
Lean toolchain	leanprover/lean4:v4.33.0
Lean version string	4.33.0 (commit d8b18978322de05a8f3dba51ef03cf5461676c17)
mathlib input revision	v4.33.0
mathlib git revision	db584cd6d46c92f209a44c0f1c829460d327499d

Locked by lean-toolchain, lakefile.toml (rev = "v4.33.0"), and lake-manifest.json. mathlib cache: after lake update, lake exe cache get is run by mathlib's post-update hook.

Layout

AutomationDebugging.lean
AutomationDebugging/
  GoalMechanics.lean                     C01–C08
  Rewriting.lean                         C09–C16
  Simplification.lean                    C17–C22
  ArithmeticAutomation.lean              C23–C30
  Search.lean                            C31–C35
  Coercions.lean                         C36–C39
  Typeclasses.lean                       C40–C42
  InductionFailures.lean                 C43–C46
  PerformanceTraps.lean                  C47–C48
  ReviewerCases.lean                     C49–C54
CASE_INDEX.md
FAILURE_TAXONOMY.md
AUDIT_CHECKLIST.md
scripts/build_and_check.sh
scripts/check_no_sorry.sh

Build

Requires elan.

elan --version
lake update
lake exe cache get
lake build

Targeted: lake build AutomationDebugging.Rewriting.

bash scripts/check_no_sorry.sh
bash scripts/build_and_check.sh

CI runs the rejection script and leanprover/lean-action@v1 with build: true, mathlib cache enabled, and nanoda left off.

A rebuild on another machine should use the committed lean-toolchain and lake-manifest.json, not master of mathlib.

Limits

• Search tactics (exact?, apply?, simp?) are documented from #check of the lemmas they are expected to find. They are not left in reviewed proofs.
• #check and #print emit info traces during lake build. That is intentional.
• aesop and grind appear as comparisons, not as a default closer.
• Deprecated mathlib aliases still compile with warnings. C32 records the current name rather than using the alias.
• Lemma names are those of mathlib v4.33.0.
• CI status on GitHub is independent of a local lake build.