golf

Lean4 Golf

Improve Lean proofs that already compile. Score candidates by: correctness → directness → clarity/inference burden → performance/determinism → length. Length is still a core goal, but a tiebreaker among acceptable proofs.

Prerequisite: Code must compile. Verify code compiles first (lean_diagnostic_messages(file) or lake env lean <path/to/File.lean> from project root; lake build for project-wide).

Usage

/lean4:golf                     # Golf entire project
/lean4:golf File.lean           # Golf specific file
/lean4:golf File.lean:42        # Golf proof at specific line
/lean4:golf --dry-run           # Show opportunities without applying
/lean4:golf --search=full          # Include lemma replacement pass
/lean4:golf --max-delegates=3    # Override default 2 concurrent subagents

Inputs

Arg	Required	Description
target	No	File or file:line to golf
--dry-run	No	Preview only, no changes
--search	No	off, quick (default), or full — LSP lemma replacement pass
--max-delegates	No	2 — max concurrent golfer subagents (preflight must pass first)

Actions

1. Verify Build - Ensure code compiles before optimizing
2. Find Patterns - Detect golfable patterns (in policy order: directness → structural → conditional):

   ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/find_golfable.py" [file] --filter-false-positives
   

   For direct-proof discovery when --search is enabled or syntactic pass stalls:

   ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/find_exact_candidates.py" [file]
   

3. Exact-Collapse Pass (bounded) — For apply/exact chain anchors from $LEAN4_SCRIPTS/find_golfable.py:
   • Mechanical (≤30 anchors/file): Construct collapsed exact from tactic structure → lean_multi_attempt + lean_diagnostic_messages baseline check (no new diagnostics, no sorry increase). Accept if the replacement is more direct or clearer. Reject if it introduces heavier automation (simpa, rwa, broad simp) to replace an explicit proof, if term length exceeds ~80 chars, if dot-chain depth > 2, or if it removes meaningful intermediate names. A 1-line saving that raises inference burden is not a win.
   • Exploratory (when --search≠off; consumes --search budget): On remaining single-goal anchors, build candidate exact terms from chain lemmas + local hypotheses + dot-notation rewrites → lean_multi_attempt + diagnostics check. Probe caps are phase-local: quick ≤5 probes/file; full ≤15 probes/file; ≤2 probes/anchor. Time budget is shared with lemma replacement (step 4): quick 30s total, full 60s total across both phases.
   • Skip: calc, cases/induction, multi-goal branches, blocks >7 lines, semicolon-heavy (>3), blocks with have/refine. constructor chains are handled by the existing instant-win rule, not this pass.
4. Lemma Replacement (if --search=quick or full):
   • Run LSP searches per candidate; test with lean_multi_attempt
   • quick: 1 search, ≤2 candidates; full: 2 searches, ≤3 candidates; ≤3 search calls; uses remaining shared time budget
   • Accept the best passing replacement by the scoring order below
   • Hand off to axiom-eliminator if replacement needs statement changes or multi-file refactor
5. Verify Safety - Check usage before inlining:

   ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/analyze_let_usage.py" [file] --line [line]
   

6. Apply - Make changes with lean_diagnostic_messages after each; lake build for final verification
7. Report - Show savings and saturation status