LeanMarathon

https://github.com/yuanhez/leanmarathon
Admin
End-to-end Lean blueprint generation and proof orchestration.
Tokens:49,327
Snippets:617
Trust Score:7.3
Update:4 months ago
Show doc for...
Tokens:
Raw
### Full Helper Lemma Documentation Example in Lean

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

A complete example of documenting a private helper lemma in Lean, including a docstring that explains its mathematical statement, the key insight, and its usage.

```Lean
/--
Helper lemma: The length of the domain is bounded by the maximum value plus one.

For a strictly monotone function `k : Fin m → ℕ`, we have `m ≤ k(m-1) + 1`.
This uses the fact that strictly monotone functions satisfy `i ≤ k(i)` for all `i`.
-/ 
private lemma strictMono_length_le_max_succ ...
```

--------------------------------

### Install LeanMarathon CLI

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Clone the repository, set up a Python virtual environment, activate it, and install the LeanMarathon package using pip.

```bash
git clone <LeanMarathon repo URL> LeanMarathon
cd LeanMarathon

python3 -m venv .venv
. .venv/bin/activate
pip install -e .
```

--------------------------------

### Example of a Well-Factored Lean Proof

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

This example demonstrates a clean and well-structured Lean proof where refactoring is not recommended. The induction structure is central to the proof's content, and comments clearly delineate logical steps.

```lean
theorem foo : Result := by
  -- Step 1: Base case
  have base : P 0 := by simp

  -- Step 2: Inductive step
  suffices ∀ n, P n → P (n + 1) by
    intro n; induction n <;> assumption

  -- Main induction argument (this IS the proof)
  intro n hn
  cases n with
  | zero => exact base
  | succ n' ->
    have ih := hn n' (Nat.lt_succ_self n')
    calc P (n' + 1) = ... := by ...
                  _ = ... := by ih

  -- Conclusion follows immediately
  exact result
```

--------------------------------

### Create Local Configuration File

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Copy the example TOML configuration file to create a local configuration file for LeanMarathon.

```bash
cp config/local.example.toml .leanmarathon.local.toml
```

--------------------------------

### System of Record Example

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Target-Reviewer/AGENTS.md

Defines the sources for key information, specifying where to find runtime inputs and details on Mathlib retrieval.

```markdown
Runtime inputs | docs/inputs.yml
Mathlib retrieval | docs/grounding/SKILL.md
```

--------------------------------

### Workflow Map Example

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Target-Reviewer/AGENTS.md

Illustrates the agent's workflow from initial launch through input processing and task execution, potentially leading to issue creation or a clean exit.

```markdown
Fresh launch
  -> docs/inputs.yml
  -> docs/exec-phase/TASK.md
       -> issue: docs/deliver/issue.md
       -> pass: clean exit
```

--------------------------------

### Placeholder Proof with 'sorry_using'

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/contracts/blueprint-format.md

Example of a multiline placeholder proof using 'sorry_using' with a list of dependencies for lemmas and theorems.

```lean
:= by
  sorry_using [name₁, name₂, …]
```

--------------------------------

### Documenting Helper Lemma: Usage Context in Lean

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Example of documenting a helper lemma in Lean by explaining how it is used in the larger proof context. This clarifies its role and relevance.

```Lean
-- Used to bound the domain length in the permutation construction
```

--------------------------------

### Placeholder Proof with 'sorry'

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/contracts/blueprint-format.md

Example of a multiline placeholder proof using 'sorry' for lemmas and theorems.

```lean
:= by
  sorry
```

--------------------------------

### Dag-Tracker MCP Server Configuration

Source: https://github.com/yuanhez/leanmarathon/blob/main/mcp-servers/dag-tracker/README.md

Example TOML configuration for registering the dag-tracker MCP server within LeanArchitect.

```toml
[mcp_servers.dag-tracker]
command = "python3"
args = ["mcp-servers/dag-tracker/dag_tracker_mcp.py"]
startup_timeout_sec = 120
tool_timeout_sec = 600
enabled_tools = [
  "admissible_external_nodes",
  "parent_nodes",
  "child_nodes",
  "global_definitional_context",
]

[mcp_servers.dag-tracker.env]
DAG_PROJECT_ROOT = "<absolute path to LeanMarathon>"
DAG_TARGET_FILE = "<path to LeanMarathon/Main.lean, relative to DAG_PROJECT_ROOT>"
PATH = "<Lean bin path>:/usr/local/bin:/usr/bin:/bin"
PYTHONUTF8 = "1"
```

--------------------------------

### Example Output of Lean Profile Proof

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

The output of `lean_profile_proof` provides a JSON object detailing the total time spent and a breakdown of time spent on individual lines, including the tactic used.

```json
{
  "total_time_ms": 2450,
  "lines": [
    {"line": 12, "tactic": "simp [add_comm, add_assoc]", "time_ms": 1200},
    {"line": 13, "tactic": "ring", "time_ms": 850}
  ]
}
```

--------------------------------

### Documenting Helper Lemma: Key Insight in Lean

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Example of documenting a helper lemma in Lean by explaining the key insight or technique used to prove it. This helps understand the 'why' behind the lemma.

```Lean
-- This uses the fact that strictly monotone functions satisfy i ≤ k(i) for all i
```

--------------------------------

### Progressive Simplification Metrics for Monomorphization

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

Track these metrics to validate the success of monomorphization. This example shows typical values before and after applying the optimization.

```lean
-- Before monomorphization:
-- Parameters: 25 (20 type classes + 5 concrete)
-- Compilation: Timeout (>1000s) or >400k heartbeats
-- Lines: 1146 with ~300 lines of parametric machinery
-- Sorries: 13 (scattered, poorly documented)

-- After monomorphization:
-- Parameters: 12 (all concrete points + hypotheses)
-- Compilation: 15 seconds
-- Lines: 850 (296 lines removed = -20%)
-- Sorries: 11 (categorized, documented with strategies)
```

--------------------------------

### Refactored Lemma Application Without Timeout

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

This example shows the recommended pattern of breaking down nested lemma applications into separate, focused helper functions. This avoids timeouts and improves clarity.

```lean
-- ✅ NO TIMEOUT: Break into focused helpers
have helper1 : intermediate_fact1 := by
  exact geometric_lemma ...  -- One application

have helper2 : intermediate_fact2 := by
  exact geometric_lemma ...  -- One application

have helper3 : intermediate_fact3 := by
  exact geometric_lemma ...  -- One application

have result : complex_property := by
  calc ...
    _ = ... := by rw [helper1]
    _ = ... := by rw [helper2, helper3]
```

--------------------------------

### Theorem Declaration Timing Out

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

This example demonstrates a Lean theorem declaration that times out due to excessive instance synthesis triggered by numerous type parameters and constraints. It is not intended to be compiled.

```lean
-- ❌ TIMEOUT: Theorem declaration never completes
theorem angle_AGH_eq_110_of_D
    {V : Type*} {P : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MetricSpace P] [NormedAddTorsor V P]
    [FiniteDimensional ℝ V] [Module.Oriented ℝ V (Fin 2)]
    (h_dim : Module.finrank ℝ V = 2)
    (A B C G H D : P)
    (h_AB_ne : A ≠ B) (h_AC_ne : A ≠ C) (h_BC_ne : B ≠ C)
    -- ... 20+ more parameters
```

--------------------------------

### Documenting Helper Lemma: Mathematical Statement in Lean

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Example of documenting a helper lemma in Lean by stating its mathematical purpose clearly. This focuses on what the lemma proves.

```Lean
-- For a strictly monotone function k : Fin m → ℕ, we have m ≤ k(m-1) + 1
private lemma strictMono_length_le_max_succ ...
```

--------------------------------

### Profile Slow Lines in Lean 4 Theorem

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

Use `lean_profile_proof` to identify performance bottlenecks within a specific theorem. This function requires the file path and the starting line number of the theorem to analyze.

```lean
lean_profile_proof(file_path="/path/to/file.lean", line=10)
```

--------------------------------

### Original Timeout-Prone Code for `hblockAvg_memLp`

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

This is the 'Before' example, illustrating the original code that leads to timeouts when proving `hblockAvg_memLp`. It directly uses `blockAvg` without the irreducible wrapper, causing the type checker to struggle with unfolding.

```lean
have hblockAvg_memLp : ∀ n, n > 0 → MemLp (blockAvg f X 0 n) 2 μ := by
  intro n hn_pos
  apply memLp_two_of_bounded
  · -- Measurable: blockAvg is a finite sum of measurable functions
    show Measurable (fun ω => (n : ℝ)⁻¹ * (Finset.range n).sum (fun k => f (X (0 + k) ω)))
    exact Measurable.const_mul (Finset.measurable_sum _ fun k _ =>
      hf_meas.comp (hX_meas (0 + k))) _
  intro ω
  -- 20+ line calc proof
  -- WHNF TIMEOUT HERE AT 500k+ HEARTBEATS

```

--------------------------------

### Initialize a Public Target Repository with Options

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Initialize a public target repository with advanced configurations for resources, orchestrators, batch size, and review rounds.

```bash
leanmarathon init \
  --owner MyGitHubName \
  --repo MyTargetRepo \
  --problem-file /absolute/path/to/problem.txt \
  --proof-file /absolute/path/to/proof-source \
  --public \
  --lean-file LeanMarathon/Main.lean \
  --auto-resource cpu \
  --auto-cpus 1 \
  --auto-time 48:00:00 \
  --stage1-orchestrator-resource cpu \
  --stage1-orchestrator-cpus 1 \
  --stage1-orchestrator-time 48:00:00 \
  --orchestrator-resource gpu \
  --orchestrator-cpus 42 \
  --orchestrator-time 48:00:00 \
  --agent-resource gpu \
  --agent-cpus 42 \
  --agent-time 4:00:00 \
  --batch-size 16 \
  --max-review-rounds 20 \
  --max-rounds 100
```

--------------------------------

### Numerical Falsification Attempt - Verifiable

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/exec-phases/numeric/TASK.md

If the Lean statement is numerically verifiable, attempt to falsify it with numerical simulations. Ask 'how could this Lean statement fail?' to guide simulation setup.

```markdown
how could this Lean statement fail?
```

--------------------------------

### Check Installed Codex Version

Source: https://github.com/yuanhez/leanmarathon/blob/main/mcp-servers/apply-patch/README.md

Use this command to determine the currently installed global version of the Codex npm package.

```bash
npm list -g @openai/codex --depth=0
```

--------------------------------

### Example of Code That Times Out

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

This example demonstrates a scenario where Lean's type checker times out due to the deep unfolding of complex functions like `blockAvg` within polymorphic goals. It hits the heartbeat limit during elaboration.

```lean
have : eLpNorm (fun ω => blockAvg f X 0 n ω - blockAvg f X 0 n' ω) 2 μ < ⊤ := by
  -- Lean unfolds blockAvg → (n:ℝ)⁻¹ * Finset.sum ...
  -- Then chases typeclass instances through every layer
  -- WHNF TIMEOUT!

```

--------------------------------

### Initialize a Private Target Repository

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Command to create and initialize a private GitHub target repository with essential files and project root.

```bash
leanmarathon init \
  --owner MyGitHubName \
  --repo MyTargetRepo \
  --problem-file /absolute/path/to/problem.txt \
  --proof-file /absolute/path/to/proof-source \
  --lean-project-root /absolute/path/to/lean-project
```

--------------------------------

### Get Source Code for Polynomial.isNoetherianRing

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/grounding/examples/discovery-example.md

Retrieves the Lean source code for the `Polynomial.isNoetherianRing` theorem using `get_source_code`.

```python
get_source_code(Polynomial.isNoetherianRing)
```

--------------------------------

### Run Stage 2

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Execute Stage 2 of LeanMarathon directly. This command starts the DAG-orchestrated loop for processing.

```bash
leanmarathon stage2 run --owner MyGitHubName --repo MyTargetRepo
```

--------------------------------

### Slurm Resource Configuration

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Example TOML configuration for Slurm resources in LeanMarathon. This defines settings for different job types.

```toml
[hpc.auto]
resource = "cpu"
cpus = 1
time = "48:00:00"

[hpc.stage1_orchestrator]
resource = "cpu"
cpus = 1
time = "48:00:00"

[hpc.stage2_orchestrator]
resource = "gpu"
cpus = 42
time = "48:00:00"

[hpc.agent]
resource = "gpu"
cpus = 42
time = "4:00:00"
batch_size = 16
```

--------------------------------

### Files Created by `leanmarathon init`

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

These are the files and directories created in the target GitHub repository by the `leanmarathon init` command.

```text
.gitignore
lakefile.toml
lake-manifest.json
lean-toolchain
LeanMarathon/Main.lean
.github/workflows/verify-blueprint.yml
.github/workflows/warmup-cache.yml
.scripts/verify_blueprint.py
```

--------------------------------

### Fast Verification with LSP in Python

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Demonstrates how to perform quick verification checks using Language Server Protocol (LSP) tools after each code edit. This is useful for rapid feedback during refactoring.

```Python
# After each edit
lean_diagnostic_messages(file_path)
lean_goal(file_path, line)
```

--------------------------------

### Avoiding Let Bindings in Helper Signatures

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Illustrates how to handle potential definitional inequality issues caused by let bindings in helper signatures. Option A uses explicit parameters with equality proofs for perfect unification.

```Lean
private lemma helper (μX : Measure α) (hμX : μX = pathLaw μ X) ...
-- Call site: helper μX rfl  -- ✓ Unifies perfectly
```

--------------------------------

### Providing Intermediate Steps for Omega

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Illustrates how to resolve failures with the 'omega' tactic by providing intermediate steps using 'calc' or explicit equalities as hypotheses when arithmetic goals are complex.

```Lean
-- ❌ Fails
have : m ≤ k last + 1 := by omega

-- ✅ Works
have (h_last_eq : last.val + 1 = m) : m ≤ k last + 1 := by
  calc m = last.val + 1 := h_last_eq.symm
       _ ≤ k last + 1 := Nat.add_le_add_right h_mono 1
```

--------------------------------

### Forbidden Mutual Declaration Block

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/contracts/blueprint-format.md

Shows an example of a forbidden 'mutual ... end' block, which groups mutually recursive declarations and is not allowed in blueprint files.

```lean
mutual
  @[blueprint "def:even" ...] def even : Nat → Bool | 0 => true | n+1 => odd n
  @[blueprint "def:odd"  ...] def odd  : Nat → Bool | 0 => false | n+1 => even n
end
```

--------------------------------

### Configure Local Paths and Lean Project

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Edit the local TOML configuration file to set paths for virtual environment binaries, node binaries, elan binaries, and the Lean project root.

```toml
[paths]
venv_bin = "/absolute/path/to/LeanMarathon/.venv/bin"
node_bin = "/absolute/path/to/node/bin"
elan_bin = "/absolute/path/to/elan/bin"
# Optional full overrides when the composed PATH is not enough.
# agent_path = "/absolute/path/to/venv/bin:/absolute/path/to/node/bin:/absolute/path/to/elan/bin:/usr/local/bin:/usr/bin:/bin"
# orchestrator_path = "/absolute/path/to/venv/bin:/absolute/path/to/node/bin:/absolute/path/to/elan/bin:/usr/local/bin:/usr/bin:/bin"

[lean]
project_root = "/absolute/path/to/lean-project"
```

--------------------------------

### Run LeanMarathon Doctor for Troubleshooting

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Execute the `doctor` command to diagnose and identify common issues with your LeanMarathon setup. It can be run with or without specifying the owner and repository.

```bash
leanmarathon doctor
```

```bash
leanmarathon doctor --owner MyGitHubName --repo MyTargetRepo
```

--------------------------------

### Examining Goal States at Key Points in Python

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Shows how to use the `lean_goal` function at strategic locations within a Lean file to examine intermediate goal states. This helps in understanding the proof's progression.

```Python
lean_goal(file, line=15)   # After initial setup
lean_goal(file, line=45)   # After first major step
lean_goal(file, line=78)   # After second major step
lean_goal(file, line=120)  # After third major step
lean_goal(file, line=155)  # Near end
```

--------------------------------

### Refactoring a Monolithic Proof into Helpers

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Demonstrates the transformation from a long, monolithic proof to a more modular structure using extracted helper lemmas. This improves readability and maintainability.

```lean
-- BEFORE: Monolithic proof
theorem big_result : Conclusion := by
  intro x hx
  have h1 : IntermediateGoal1 := by
    [30 lines of tactics...]
  have h2 : IntermediateGoal2 := by
    [40 lines of tactics...]
  [30 more lines...]

-- AFTER: Extracted helpers
lemma helper1 (x : α) (hx : Property x) : IntermediateGoal1 := by
  [30 lines - extracted from h1]

lemma helper2 (x : α) (h1 : IntermediateGoal1) : IntermediateGoal2 := by
  [40 lines - extracted from h2]

theorem big_result : Conclusion := by
  intro x hx
  have h1 := helper1 x hx
  have h2 := helper2 x h1
  [30 lines - much clearer now]
```

--------------------------------

### Nested Lemma Application Causing Timeout

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/performance-optimization.md

This example demonstrates a nested application of `geometric_lemma` that leads to a deterministic elaboration timeout in Lean. Avoid this pattern when dealing with complex lemmas.

```lean
-- ❌ TIMEOUT: Nested applications of geometric_lemma
have result : complex_property := by
  have h1 := geometric_lemma ...
  have h2 := geometric_lemma ...  -- Uses h1
  have h3 := geometric_lemma ...  -- Uses h2
  calc ...  -- Combines h1, h2, h3
    -- Deterministic timeout at 200k heartbeats!
```

--------------------------------

### Codex Configuration File

Source: https://github.com/yuanhez/leanmarathon/blob/main/mcp-servers/apply-patch/README.md

The server is registered in Codex's project config file.

```text
.codex/config.toml
```

--------------------------------

### Get Source Code for iteratedDerivWithin and taylorWithinEval

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Target-Reviewer/docs/grounding/example/api-example.md

These definitions show the `s : Set` parameter, which distinguishes the `Within` API from its non-`Within` counterparts. This is crucial for formalizing theorems on closed intervals.

```lean
def iteratedDerivWithin (n : ℕ) (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜) : F :=
  (iteratedFDerivWithin 𝕜 n f s x : (Fin n 𝕜) → F) fun _ : Fin n => 1

noncomputable def taylorWithinEval (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ) : E :=
  PolynomialModule.eval x (taylorWithin f n s x₀)
```

--------------------------------

### Generic Sequential Steps in Lean

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

When meaningful names aren't obvious, use generic sequence names like 'step1', 'step2' for intermediate results in Lean proofs. This is suitable for exploratory or linear proofs.

```Lean
theorem main_result ... := by
  -- Step 1: E(∑cᵢξᵢ)² = E(∑cᵢ(ξᵢ-m))² using ∑cⱼ = 0
  have step1 : ... := by ...

  -- Step 2: = ∑ᵢⱼ cᵢcⱼ cov(ξᵢ, ξⱼ) by expanding square
  have step2 : ... := by ...

  -- Final: Combine steps
  calc ...
```

--------------------------------

### Authenticate with GitHub CLI

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Use this command to log in to GitHub via the command-line interface.

```bash
gh auth login
```

--------------------------------

### Pattern 2: Optimization / Extremal Value Reframing

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/references/reframing.md

Apply this template for problems asking for maximum or minimum values. It involves defining the extremal configuration, proving it achieves the value, and demonstrating it's an upper/lower bound.

```lean
@[blueprint "thm:maximum-value"
  (statement := /-- The maximum of $\sum_{i=1}^n a_i b_i$ subject to
    «constraints» is $M$, achieved when «conditions». -/)
  (latexEnv := "theorem")]
theorem maximum_value : «IsGreatest or sSup formulation» := by
  /-- We show the upper bound in \cref{lem:upper-bound} and
      achievability in \cref{lem:achieves-value}. -/
  sorry_using [upper_bound, achieves_value]
```

--------------------------------

### Refactoring Decision Tree

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

This tree guides the decision-making process for refactoring long proofs in Lean. It helps identify when a proof is a good candidate for refactoring and suggests specific patterns for extracting reusable lemmas.

```markdown
Is the proof 60-200 lines? (sweet spot for refactoring)
├─ Yes: Look for natural boundaries (use lean_goal at 4-5 key points)
│   ├─ Repetitive structure (lhs/rhs, symmetric args, or repeated case splits)?
│   │   └─ Extract common pattern to helper (Pattern 1.3)
│   ├─ Single large case split (30+ lines proving reusable fact)?
│   │   └─ Extract even if not repeated (Pattern 1.3 - single large case split)
│   ├─ Multiple properties proven separately, used together?
│   │   └─ Bundle with ∧, use obtain (Pattern 1.5)
│   ├─ Mixes multiple mathematical domains (combinatorics + analysis)?
│   │   └─ Extract each domain's logic separately (Pattern 1.2)
│   ├─ Starts with 50+ line preliminary calculation?
│   │   └─ Extract preliminary fact to helper (Pattern 1.1)
│   ├─ Same 5-10 line notation conversion repeated?
│   │   └─ Extract conversion helper (Pattern 1.6)
│   ├─ Found witness extraction (choose/obtain)?
│   │   └─ Extract to helper (Pattern 1.4 - clear input/output contract)
│   ├─ Found arithmetic bounds?
│   │   ├─ Can extract without `let` bindings? → Extract to private helper (Pattern 3.1)
│   │   └─ Uses complex `let` bindings? → Consider inlining (Pattern 2.3)
│   ├─ Found permutation construction?
│   │   └─ Reusable pattern? → Extract (ensure parameter clarity, Pattern 2.1)
│   ├─ Found "all equal, pick one" pattern?
│   │   ├─ Equality proof → Extract to helper (Pattern 2.4 - mathematical content)
│   │   └─ Choice of representative → Keep in main (proof engineering)
│   └─ Found measure manipulations?
│       └─ Uses `let` bindings? → Prefer inlining (Pattern 3.4 - definitional issues)
├─ > 200 lines? → Multiple refactorings needed (start with largest prelims, Pattern 1.1)
└─ < 60 lines? → Probably fine as-is (unless heavily repetitive)

When extracting:
1. Make helper `private` if proof-specific (Pattern 3.1: use regular -- comments, not /-- -/)
2. **Generic is better** (Pattern 2.1): Remove proof-specific constraints
3. Avoid `let` bindings in helper signatures (Pattern 2.3)
4. If omega fails, add explicit intermediate steps (Pattern 3.3: use calc)
5. Prefix unused but required parameters with underscore (Pattern 3.2: _hS)
6. Add structural comments that explain "why", not "what" (Pattern 4.2)
7. Test compilation after each extraction (Pattern 5.1: lean_diagnostic_messages)
```

--------------------------------

### Generic vs. Specific Helper Lemma

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

Demonstrates generalizing a helper lemma by relaxing equality to inequality and removing specific values. Use the generic version when the exact value is not critical to the proof.

```Lean
-- ❌ Too specific
private lemma helper (n : ℕ) (hn : n = 42) : Property n

-- ✅ Generic
private lemma helper (n : ℕ) (hn : 1 ≤ n) : Property n
```

--------------------------------

### Configure SLURM Settings

Source: https://github.com/yuanhez/leanmarathon/blob/main/README.md

Configure SLURM-related settings in the local TOML file, including CPU and GPU accounts, GPU partition, GPU GRES, and memory per CPU.

```toml
[slurm]
cpu_account = ""
gpu_account = ""
gpu_partition = "gpu"
gpu_gres = "gpu:lovelace_l40:1"
mem_per_cpu = 3850
```

--------------------------------

### Get Compilation Diagnostics for a Lean File

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/lean-lsp-tools.md

Use this function to retrieve compiler diagnostics (errors, warnings, infos) for a Lean file. It can filter diagnostics by line range, declaration name, severity, or return interactive TaggedText objects.

```python
lean_diagnostic_messages(file_path=<lean_file_abs>)
```

```python
lean_diagnostic_messages(file_path=<lean_file_abs>, start_line=120, end_line=180)
```

```python
lean_diagnostic_messages(file_path=<lean_file_abs>, severity="error")
```

--------------------------------

### Retrieve Lebesgue Dominated Convergence Theorem Source Code

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/references/discovery-example.md

Retrieves the Lean source code for the Lebesgue Dominated Convergence Theorem. This is useful for proving convergence of integrals under certain conditions.

```lean
theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → G} {f : α → G} (bound : α → ℝ)
    (F_measurable : ∀ n, AEStronglyMeasurable (F n) μ)
    (bound_integrable : Integrable bound μ)
    (h_bound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
    Tendsto (fun n => ∫ a, F n a ∂μ) atTop (𝓝 <| ∫ a, f a ∂μ)
```

--------------------------------

### Lean Proof Formalization Decision Tree

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Refiner/AGENTS.md

This tree outlines the decision process for handling Lean tactic proofs, distinguishing between new and existing code, and specifying actions for placeholder or complete tactic proofs. It guides whether to preserve, align, or wholesale-replace proof bodies based on compilation status and statement edits.

```markdown
Is the node NEW (inserted) or EXISTING (inherited from `$2`)?
├── NEW: body is `by sorry` or `by sorry_using [deps]`
└── EXISTING: current body shape?
    ├── placeholder (`by sorry` / `by sorry_using`): keep it; align `sorry_using` with new `
cref` set if prose changed
    └── complete tactic proof: still compiles after your statement/type edits?
        ├── YES: preserve byte-identical to input blueprint
        └── NO: wholesale-replace with `by sorry` or `by sorry_using [deps]`
```

--------------------------------

### SAV Algorithm for Existing Result Discovery

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/exec-phases/grounding/TASK.md

The Search-and-Verify (SAV) pipeline discovers existing Mathlib results by describing a proof step, searching summaries, and verifying the type signature of the top results.

```python
query ← describe(proof_step)
results ← search_summary(query, limit=k)
for r in top-n results:
    src ← get_source_code(r.id)
    if matches(src.type_signature, proof_step):
        return (r.name, match_type)
```

--------------------------------

### Lean File Headers

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Blueprinter/docs/exec-phases/draft/TASK.md

The initial lines of the Lean blueprint file, including necessary imports and compiler options.

```lean
import Mathlib
import Architect

set_option linter.all false
set_option maxHeartbeats 500000
```

--------------------------------

### Using Local Instances within Sections

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Refiner/docs/contracts/blueprint-format.md

Demonstrates how to define local instances within a 'section' to prevent them from leaking to importers. This is useful for typeclass instances that are specific to a certain context.

```lean
section

  @[blueprint "def:foo-inhab"
    (statement := /-- ... -/)
    (title := /-- ... -/)
    (latexEnv := "definition")]
  local instance foo_inhab : Inhabited Foo := ⟨0⟩

end
```

--------------------------------

### Verifying Extraction with LSP

Source: https://github.com/yuanhez/leanmarathon/blob/main/agents/Worker/docs/references/proof-refactoring.md

After extracting a helper lemma, use LSP tools to verify the refactoring. Check for diagnostic messages and confirm that the goals at the original and new locations match expectations.

```python
lean_diagnostic_messages(file)  # Check for errors
lean_goal(file, line)           # Confirm goals match
```

```python
# Original line number where `have h1 : ...` was
lean_goal(file, line=old_h1_line)
# → Should match helper1's conclusion

# New line number after extraction
lean_goal(file, line=new_h1_line)
# → Should show `h1 : IntermediateGoal1` available
```
Tokens:
Raw