/lean4

Sorry Filling Reference

Primary reference for sorry-filling tactics. The prove/autoprove work phase implements this workflow; see command-examples.md for session transcripts.

Quick reference for filling Lean 4 sorries systematically.

Core Workflow

1. Understand Context - lean_goal(file, line) first, then read surrounding code
2. Search Mathlib FIRST - Most proofs already exist
3. Generate Candidates - 2-3 proof approaches
4. Test Before Applying - Use lean_multi_attempt to test candidates, then lean_diagnostic_messages(file) to confirm no residual errors
5. Apply Working Solution - Shortest working proof wins

LSP-First Requirement

Always use LSP tools before scripts:

1. lean_goal(file, line) — understand the goal
2. lean_local_search("keyword") — search mathlib
3. lean_multi_attempt(file, line, snippets=[...]) — test candidates
4. lean_diagnostic_messages(file) — verify no residual errors; check for "Try this" suggestions
5. If diagnostics show "Try this" → lean_code_actions(file, line) to resolve to a concrete edit → lean_diagnostic_messages(file) to re-verify after applying
6. If initial searches/attempts are inconclusive: lean_hammer_premise(file, line, col) — premise suggestions for simp/aesop/grind (rate-limited 3/30s)

File ownership: One writer per owned file set. A subagent owns only the files it was dispatched to work on. Do not edit files outside the owned set without escalating to the caller. Never create scratch files in the repo root.

Parallel dispatch hazard: File ownership is file-granular, not theorem-granular — never dispatch multiple agents to edit the same file concurrently, even if they target different sorrys. See subagent-workflows.md § Same-File Parallel Dispatch.

Scratch-work preference order:

• Use the live file + lean_goal / lean_multi_attempt / lean_diagnostic_messages when the question depends on the actual file context.
• If you need an isolated experiment, prefer lean_run_code over creating temporary .lean files.
• Use /tmp scratch files only when lean_run_code is unavailable or insufficient and the experiment should not touch the live file.

Session-end reporting: Report files_touched (files edited) and scratch_files_created (any /tmp files used for experiments). The caller uses this for staging and cleanup.

Only fall back to scripts ($LEAN4_SCRIPTS/sorry_analyzer.py, $LEAN4_SCRIPTS/smart_search.sh) if: <!-- guardrails: compatibility-fallback -->

• LSP server unavailable
• LSP results inconclusive after 2-3 searches

When using sorry_analyzer.py:

• Default (text) already returns count + context in one call.
• Use --format=json for structured downstream parsing.
• Use --format=summary only when you need counts only.
• Keep stderr visible; do not redirect analyzer stderr to /dev/null.

Log which approach worked for each sorry.

Todo-Based Workflow (For Multiple Sorries)

Problem: When there are 10+ sorries, it's easy to get lost trying to work on all of them at once.

Solution: Enumerate sorries, add each to a TODO list, and work on ONE at a time.

Step 1: Enumerate

List all sorry's in the project, then add each as a single item to the TODO list.

Step 2: Focus on ONE

Fill in Sorry #01. DO NOT MOVE ON TO OTHER SORRY'S BEFORE THIS ONE IS FILLED.

Step 3: Verify compilation

lake env lean path/to/File.lean   # run from project root; checks against built imports only

This gate elaborates the file against the .oleans already built for its imports and does not rebuild them. If you edited an imported module in this session, first run lake build <path/to/ChangedImport.lean> (or lake lean <path/to/File.lean> for this file's module) — otherwise the gate can pass code that fails to build. See cycle-engine: File Gate Scope.

Step 4: Repeat Continue with the next sorry in the TODO list.

Search Strategies

By name pattern:

bash $LEAN4_SCRIPTS/search_mathlib.sh "continuous compact" name   # guardrails: compatibility-fallback

Multi-source smart search:

bash $LEAN4_SCRIPTS/smart_search.sh "property description" --source=leansearch   # guardrails: compatibility-fallback

Get tactic suggestions: See tactic-patterns.md for goal-based tactic recommendations.

Common Sorry Types

Type 1: "Forgot to search mathlib" (most common)

Solution: Search thoroughly, apply existing lemma

Type 2: "Just needs right tactic" (common)

Solution: Try rfl, simp, ring, or domain automation

Type 3: "Missing intermediate step" (less common)

Solution: Add have with connecting lemma

Type 4: "Complex structural proof" (rare)

Solution: Break into sub-sorries with clear strategy

Type 5: "Actually needs new lemma" (very rare)

Solution: Extract as helper lemma, prove separately

Proof Candidate Generation

Always generate 2-3 approaches:

Candidate A - Direct:

exact lemma_from_mathlib arg1 arg2

Candidate B - Tactics:

intro x
have h1 := lemma_1 x
simp [h1]
apply lemma_2

Candidate C - Automation:

simp [lemma_1, lemma_2, *]

Candidate D - Premise-based (from lean_hammer_premise):

simp only [premise_1, premise_2, premise_3]
-- or: grind [premise_1, premise_2]
-- or: aesop

Tactic Suggestions by Goal Pattern

Testing Candidates

With LSP server (preferred):

lean_multi_attempt(
  file = "path/to/file.lean",
  line = line_number,
  snippets = [
    "candidate_A_code",
    "candidate_B_code",
    "candidate_C_code"
  ]
)

Without LSP:

• Apply candidate
• Run lean_diagnostic_messages(file) per-edit; lake env lean path/to/File.lean (from project root) for file gate
• If fails, try next candidate

Common Errors

Type mismatch:

• Add coercion: (x : ℝ) or ↑x
• Try different lemma form
• Check implicit arguments

Tactic failure:

• Add specific lemmas: simp [lemma1, lemma2]
• Try manual steps instead of automation
• Check hypothesis availability

Import missing:

• Add import detected from search results
• Use #check LemmaName to verify

Best Practices

⚠️ Critical: Verify compilation before moving on LSP tools can sometimes show success when problems remain. After a sequence of changes, before moving on to something else entirely, verify with:

• Per-edit: lean_diagnostic_messages(file)
• File gate: lake env lean path/to/File.lean (run from project root)
• Project gate: lake build (checkpoint/final only)

This catches issues that per-edit LSP may miss.

• Follow mathlib 100-char line width — do not wrap lines at 80 when they fit within 100

💡 Cache after clean or in a fresh worktree If you run lake clean, or start from a fresh clone/worktree, hydrate the cache before the first full build:

lake cache get
# or, in projects that use the older mathlib cache executable:
lake exe cache get

Otherwise you may recompile large dependencies from scratch.

Do this in the current worktree. Do not symlink another worktree's .lake/build; separate worktrees may be on different commits and should keep separate local build directories.

✅ Do:

• Search mathlib exhaustively before proving
• Test all candidates if possible
• Use shortest working proof
• Verify: lean_diagnostic_messages(file) per-edit; lake env lean <path/to/File.lean> for file gate (from project root; after a cross-file edit, lake lean <path/to/File.lean> instead — see File Gate Scope)
• Add necessary imports

❌ Don't:

• Skip mathlib search
• Apply without testing
• Use overly complex proofs when simple ones work
• Forget imports
• Leave sorries undocumented if you can't fill them

Blocked-Goal Triage

When one goal or tactic dead end resists the candidate workflow above, run this short loop before escalating. It is a decision process, not a tactic catalog — the cascades live in the skill's Automation Tactics and tactics-reference.

1. Make the blocker concrete. Inspect the exact goal and diagnostics (lean_goal, lean_term_goal, lean_hover_info, lean_diagnostic_messages). If you cannot justify the next tactic from the goal state, inspect more instead of guessing.
2. Classify the blocker before trying anything:
   • definitional equality / simplification
   • missing intro / constructor / cases step
   • missing rewrite
   • arithmetic / inequalities
   • missing library lemma
   • typeclass / coercion / elaboration issue (see compilation-errors)
   • proof too large — needs a helper lemma (see proof-simplification)
3. Test at most 3 low-cost candidates with lean_multi_attempt, chosen for the blocker class — including suggestion tactics (exact?, apply?, rw?, simp?, try?; hint when Mathlib.Tactic.Hint or the umbrella Mathlib module is imported). A suggestion-tactic result is only a probe until its explicit suggested code is installed and reverified.
4. Search before adding structure. When direct attempts stall, use the search ladder above rather than piling on tactics or new have scaffolding.
5. If the same blocker repeats, stop guessing. Hand off to a stuck review (review in stuck mode) or a prove workflow rather than continuing.

As a working heuristic, 2–3 failed direct attempts on the same blocker means switch strategy — change class, search, or restructure. (The enforced stuck definition — triggers, blocker signature, and required handoff evidence — is owned by cycle-engine; this loop is advisory and does not redefine it.)

Suggestion tactics are discovery tools: replace their output with explicit proof code and re-run diagnostics before considering the goal solved.

Structural escape hatches when the issue is shape, not the next tactic: shrink the goal with have/suffices/refine, normalize one side before searching for the key rewrite, destructure hypotheses early, or extract a helper lemma — see proof-simplification.

When to Escalate

Give up and escalate if:

• All 3 candidates fail with same error
• Goal requires domain knowledge you don't have
• Needs multi-file refactoring
• Missing foundational lemmas
• Time spent > 15 minutes on single sorry

Escalation options:

• Break into smaller sub-sorries
• Extract as helper lemma
• Document as TODO with strategy
• Use /lean4:prove --deep=stuck for deep sorry-filling workflow

If statement may be false:

• Run preflight falsification (decide, small enumeration)
• If counterexample found, create T_counterexample
• Create T_salvaged with weaker/corrected statement
• See prove/autoprove stuck → salvage workflow

Output Size Limits

For fast path:

• Max 3 candidates per sorry
• Each diff ≤80 lines
• If 0/3 compile, skip and continue (or escalate with --deep)