lean4

Autonomous multi-cycle theorem proving with hard stop rules

Save progress with a safe commit checkpoint

Diagnostics, cleanup, and migration help

Optimize Lean proofs for brevity and clarity

Interactive teaching, mathlib exploration, and autoformalization

Guided cycle-by-cycle theorem proving with explicit checkpoints

Read-only code review of Lean proofs

Remove nonconstructive axioms by refactoring proofs to structure (kernels, measurability, etc.). Use after checking axiom hygiene to systematically eliminate custom axioms.

Golf Lean 4 proofs after they compile; reduce tactics/lines without changing semantics. Use after successful compilation to achieve 30-40% size reduction.

Compiler-guided iterative proof repair with two-stage model escalation (Haiku → Opus). Use for error-driven proof fixing with small sampling budgets (K=1).

Strategic resolution of stubborn sorries; may refactor statements and move lemmas across files. Use when fast pass fails or for complex proofs.

Use when editing .lean files, seeing type mismatch/sorry/failed to synthesize instance/axiom warnings, lake build errors, or searching mathlib for theorem proofs.

2 hooks across 2 events