lean4-proof-golfer

Inputs

• File path to optimize
• Passing build required (will verify before starting)
• Search mode: off, quick (default), or full

Actions

1. Find patterns (in policy order: directness → structural → conditional) with false-positive filtering:

   ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/find_golfable.py" FILE.lean --filter-false-positives
   

   For direct-proof discovery when search_mode ≠ off or syntactic pass stalls:

   ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/find_exact_candidates.py" FILE.lean
   

2. Verify safety before inlining any binding:

   ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/analyze_let_usage.py" FILE.lean --line LINE
   

   • 1-2 uses: Safe to inline
   • 3-4 uses: Check carefully (40% worth optimizing)
   • 5+ uses: NEVER inline

3. Exact-collapse pass (for apply-exact-chain anchors from step 1):

   • Mechanical (≤30 anchors/file): construct collapsed exact → lean_multi_attempt + lean_diagnostic_messages baseline check; accept by scoring order (per golf.md: directness → inference burden → perf → length)
   • Exploratory (when search_mode ≠ off; shared budget): candidate exact from chain lemmas + local hyps + dot-notation rewrites → lean_multi_attempt; ≤2 probes/anchor, quick ≤5/file 30s, full ≤15/file 60s. Skip: calc, multi-goal, blocks >7 lines, semicolon-heavy, have/refine

4. Lemma replacement search (if search_mode ≠ off):

   • lean_local_search first, then lean_leanfinder or lean_loogle
   • quick: 1 search, ≤2 candidates; full: 2 searches, ≤3 candidates
   • Test with lean_multi_attempt; accept the best passing replacement by scoring order (per golf.md: directness → inference burden → perf → length)
   • Budget: ≤3 search calls, max 3 candidates; uses remaining shared time budget (quick 30s, full 60s total across steps 3–4)
   • If replacement needs statement changes or multi-file refactor → stop, hand off to axiom-eliminator