diff --git a/prompts/docs/prompts/blueprint_agent.md b/prompts/docs/prompts/blueprint_agent.md
index b37711f..085ca63 100644
--- a/prompts/docs/prompts/blueprint_agent.md
+++ b/prompts/docs/prompts/blueprint_agent.md
@@ -87,6 +87,17 @@ Final: Combining steps 1-N completes the proof.
 - If proof is >20 lines informal → SPLIT
 - Otherwise → Just update informal proof, don't split
 
+**File Splitting Decision:**
+When splitting into sub-lemmas, also decide whether they should go in a **separate helper file**:
+- If the sub-lemmas are **mathematically independent** (only need Mathlib, not definitions from the main file) → put them in `<main_file>_helpers.lean`
+- If the sub-lemmas depend on definitions in the main file → keep them in the same file
+- Helper files must only `import Mathlib` — no cross-imports between helper files
+
+When placing sub-lemmas in a helper file, update the `file` field in the blueprint accordingly. The proof agent will need to:
+1. Write and check the helper file with `python skills/cli/lean_check.py`
+2. Run `lake build <Project>.<HelperModule>` to produce `.olean`
+3. Import the helper file from the main file
+
 ### Step 4: Update Blueprint
 
 #### Case A: No Splitting Needed
diff --git a/prompts/docs/prompts/common.md b/prompts/docs/prompts/common.md
index 3af7bd1..cfe6320 100644
--- a/prompts/docs/prompts/common.md
+++ b/prompts/docs/prompts/common.md
@@ -90,7 +90,7 @@ lemma name : statement := by
 State: 🔄 partial
 Priority: 1
 Attempts: 12 / 20
-tmp file: PutnamLean/tmp_base_case.lean
+tmp file: tmp/tmp_base_case.lean
 -/
 lemma base_case (n : ℕ) : f 0 = 1 := by
   have h : 0! = 1 := Nat.factorial_zero
@@ -106,13 +106,13 @@ lemma base_case (n : ℕ) : f 0 = 1 := by
 ### Protocol
 1. **Note tmp file** in original file's status comment
    ```lean
-   tmp file: tmp_<lemma_name>.lean
+   tmp file: tmp/tmp_<lemma_name>.lean
    ```
 
-2. **Create tmp file** in same directory as original
+2. **Create tmp file** in a `tmp/` subfolder alongside the original file
    ```bash
-   # If original is PutnamLean/Example.lean
-   # Create PutnamLean/tmp_base_case.lean
+   # If original is Experiment/main_theorem.lean
+   # Create Experiment/tmp/tmp_base_case.lean
    ```
 
 3. **Work in tmp file**
@@ -131,8 +131,8 @@ lemma base_case (n : ℕ) : f 0 = 1 := by
 
 ### Example Tmp File
 ```lean
--- File: PutnamLean/tmp_base_case.lean
-import PutnamLean.Example
+-- File: Experiment/tmp/tmp_base_case.lean
+import Experiment.MainTheorem
 
 lemma base_case (n : ℕ) : f 0 = 1 := by
   -- Working proof here
diff --git a/prompts/docs/prompts/coordinator.md b/prompts/docs/prompts/coordinator.md
index a170368..faa6cde 100644
--- a/prompts/docs/prompts/coordinator.md
+++ b/prompts/docs/prompts/coordinator.md
@@ -166,7 +166,7 @@ Current status: ❌ todo / 🔄 partial (X/Y attempts)
 Budget: Y attempts
 
 Follow the proof agent protocol:
-1. Work in tmp file
+1. Work in tmp file (create in tmp/ subfolder alongside original)
 2. Try hint/grind first
 3. Search with leandex (`python skills/cli/leandex.py`) before proving
 4. Try all 5 categories
diff --git a/prompts/docs/prompts/proof_agent.md b/prompts/docs/prompts/proof_agent.md
index c4a1fc4..495c8bf 100644
--- a/prompts/docs/prompts/proof_agent.md
+++ b/prompts/docs/prompts/proof_agent.md
@@ -25,7 +25,7 @@ This file adds proof-agent-specific rules on top of those common foundations.
 **Your code MUST compile without errors when you exit.**
 
 ### Rules
-1. **All code must compile**: **axle-check** (`python skills/cli/axle.py check`) returns no severity-1 errors
+1. **All code must compile**: **lean-check** (`python skills/cli/lean_check.py FILE`) returns no errors (severity "error")
 2. **NEVER use `axiom`**: Using `axiom` is FORBIDDEN. Use `sorry` instead.
 3. **If cannot complete a proof**:
    - Identify the **smallest** stuck part
@@ -58,8 +58,8 @@ lemma foo : P := by
 ```
 
 ### Before Exiting
-1. Run **axle-check** on file (`python skills/cli/axle.py check FILE --environment lean-4.28.0`)
-2. If ANY error (severity 1): fix it or sorry the minimal stuck part
+1. Run **lean-check** on file (`python skills/cli/lean_check.py FILE`)
+2. If ANY error (severity "error"): fix it or sorry the minimal stuck part
 3. Verify file compiles cleanly
 
 ---
@@ -348,11 +348,15 @@ Starting Attempt: [N] (resume if > 0, else start at 1)
 │  PRIMARY WORKFLOW: WORK IN TMP FILES                            │
 │                                                                 │
 │  1. Note tmp file in original                                   │
-│  2. Create tmp_<lemma_name>.lean in same directory              │
+│  2. Create tmp/<lemma_name>.lean in a tmp/ subfolder            │
+│     alongside the original file                                 │
 │  3. Work in tmp file (all attempts)                             │
 │  4. Copy back when proven                                       │
 │  5. Delete tmp file                                             │
 │                                                                 │
+│  IMPORTANT: NEVER write tmp files to /tmp or the system temp    │
+│  directory. Always use a tmp/ subfolder next to the original.   │
+│                                                                 │
 │  WHY: Keeps iteration context separate, avoids cluttering       │
 │       original code with failed attempts                        │
 └─────────────────────────────────────────────────────────────────┘
@@ -369,7 +373,7 @@ Starting Attempt: [N] (resume if > 0, else start at 1)
 │  ORDER MATTERS:                                                  │
 │                                                                 │
 │  1. FIRST: Edit original file to add tmp file path in comment   │
-│  2. THEN:  Create the tmp file                                  │
+│  2. THEN:  Create the tmp file in tmp/ subfolder                │
 │                                                                 │
 │  WHY: If you create tmp file first and forget to update the     │
 │       original, other agents won't know work is in progress.    │
@@ -382,20 +386,21 @@ Update the status comment in the **original file**:
 State: ❌ todo
 Priority: 1
 Attempts: 0 / 20
-tmp file: PutnamLean/tmp_base_case.lean  ← ADD THIS FIRST!
+tmp file: Experiment/tmp/tmp_base_case.lean  ← ADD THIS FIRST!
 -/
 lemma base_case (n : ℕ) : f 0 = 1 := sorry
 ```
 
-**Verify**: Run **axle-check** on the original file to ensure it still compiles.
+**Verify**: Run **lean-check** on the original file to ensure it still compiles.
 
 #### Step 2: Create Tmp File (AFTER updating original)
 
 **Only create the tmp file AFTER Step 1 is complete.**
+Create a `tmp/` subfolder alongside the original file if it doesn't exist.
 
 ```lean
--- File: PutnamLean/tmp_base_case.lean
-import PutnamLean.Example  -- Import original file
+-- File: Experiment/tmp/tmp_base_case.lean
+import Experiment.MainTheorem  -- Import original file
 
 lemma base_case (n : ℕ) : f 0 = 1 := by
   sorry
@@ -419,6 +424,30 @@ Clean up after success!
 
 ---
 
+## Splitting Helper Lemmas into Separate Files
+
+When you create helper lemmas that are **mathematically independent** from the main theorem (i.e., they only depend on Mathlib, not on other definitions in the main file), consider placing them in a separate helper file.
+
+### When to Split
+- Helper lemmas are self-contained (only need `import Mathlib`)
+- The main file is getting long and hard to manage
+- The blueprint agent has identified sub-lemmas as independent modules
+
+### How to Split
+1. Create a helper file alongside the main file (e.g., `Experiment/main_theorem_helpers.lean`)
+2. The helper file should only `import Mathlib` (no cross-imports between helper files)
+3. Run `python skills/cli/lean_check.py main_theorem_helpers.lean` to verify it compiles
+4. Run `lake build <Project>.<ModuleName>` (e.g., `lake build Experiment.MainTheoremHelpers`) to produce `.olean` — **this is required before the main file can import it**
+5. Add `import Experiment.MainTheoremHelpers` to the main file
+6. Run `python skills/cli/lean_check.py main_theorem.lean` to verify the import works
+
+### Rules
+- **Helper files must only import Mathlib**, not each other — keeps the build dependency simple
+- **Always `lake build` the helper file** before importing it from the main file — `lean_check.py` alone does NOT produce `.olean` files
+- **Verify both files compile** after splitting — check the helper first, build it, then check the main file
+
+---
+
 ## Attempt Budget System (CRITICAL)
 
 **Hard rules** (cannot be bypassed):
@@ -490,7 +519,7 @@ Please provide:
 [paste lemma statement]
 
 Current proof state:
-[paste from axle-check lean_messages]
+[paste from lean-check lean_messages]
 
 I've tried 2 approaches so far:
 1. [approach 1]: [result/error]
@@ -654,7 +683,7 @@ Can you suggest a simpler or more direct way to structure this proof?"
 - `simp_rw [lemmas]` - rewrite then simplify
 - `norm_cast` - normalize casts between types
 
-**Try 3-5 tactic variations** by editing the file and running **axle-check** after each:
+**Try 3-5 tactic variations** by editing the file and running **lean-check** after each:
 ```lean
 -- Try each of these in turn:
 hint / grind / omega / simp; omega / norm_cast; ring
@@ -730,9 +759,9 @@ lemma parent_lemma_helper (args) : goal := sorry
 
 When a proof is broken or too complex and you want to isolate the failing part automatically:
 1. Replace the failing tactic with `sorry`
-2. Run **axle-check** to confirm the file compiles (warnings OK, zero errors)
+2. Run **lean-check** to confirm the file compiles (warnings OK, zero errors)
 3. Run `python skills/cli/axle.py sorry2lemma FILE --environment lean-4.28.0 --names THEOREM --reconstruct-callsite`
-4. Run **axle-check** to verify the extracted lemma + reconstructed call site compiles
+4. Run **lean-check** to verify the extracted lemma + reconstructed call site compiles
 
 This automatically captures local context variables, generates a standalone lemma above the theorem, and replaces the sorry with a call to the new lemma. See `skills/sorrifier/SKILL.md` for the full protocol.
 
@@ -767,17 +796,17 @@ Is N == 0, 2, 4, 8, 16, or 32?
 ### Step 4: Implement Approach (in tmp file!)
 
 **Before coding**:
-- Run **axle-check** to see current proof state and errors
+- Run **lean-check** to see current proof state and errors
 - If goal looks classic → search with leandex
 - Always try hint/grind first
 
 **During coding**:
 - Work in tmp file
-- Try tactic variations and run **axle-check** after each
+- Try tactic variations and run **lean-check** after each
 - Pick what makes most progress
 
 **After coding**:
-- Run **axle-check** to verify
+- Run **lean-check** to verify
 - If error, analyze carefully
 - If success, prepare to copy back!
 
@@ -833,7 +862,7 @@ After attempts 10, 20, 30, 40:
 
 1. **Copy proof from tmp file to original**
 2. **Delete tmp file**
-3. **Verify with axle-check**
+3. **Verify with lean-check** (`python skills/cli/lean_check.py FILE`)
 4. **Update BLUEPRINT**
 5. **Complete agent log**
 6. **Report to Coordinator**
@@ -872,7 +901,7 @@ All tools are CLI scripts in `skills/cli/`. For full parameters, read `skills/<c
 
 | Tool | CLI | When to use |
 |------|-----|-------------|
-| **axle-check** | `python skills/cli/axle.py check FILE --environment lean-4.28.0` | After every code change |
+| **lean-check** | `python skills/cli/lean_check.py FILE` | After every code change |
 | **axle-verify-proof** | `python skills/cli/axle.py verify-proof STMT PROOF --environment lean-4.28.0` | To verify proof matches statement |
 | **axle-repair** | `python skills/cli/axle.py repair-proofs FILE --environment lean-4.28.0` | When close but small errors remain |
 
diff --git a/prompts/docs/prompts/session_start.md b/prompts/docs/prompts/session_start.md
index 57e77ff..f26552d 100644
--- a/prompts/docs/prompts/session_start.md
+++ b/prompts/docs/prompts/session_start.md
@@ -36,8 +36,8 @@ BLUEPRINT is the single source of truth. If it's out of sync, the next session w
 
 ## ⚠️ CRITICAL: Verification Protocol
 
-**Proof agents must use axle-check for compilation checks.**
-- ✅ USE: `python skills/cli/axle.py check FILE --environment lean-4.28.0`
+**Proof agents must use lean-check for compilation checks.**
+- ✅ USE: `python skills/cli/lean_check.py FILE`
 - ❌ AVOID: lake build (slow, unnecessary for single file)
 
 ## Workflow
@@ -82,10 +82,10 @@ BLUEPRINT is the single source of truth. If it's out of sync, the next session w
             Common rules: /mnt/nvme1/jacky/workspace/claude_base/putnam/docs/prompts/common.md
 
             Rules:
-            1. Work in tmp file (create tmp_<lemma_name>.lean in same directory)
+            1. Work in tmp file (create tmp/tmp_<lemma_name>.lean in a tmp/ subfolder alongside the original)
             2. Try hint → grind FIRST before any manual tactics
             3. Search leandex (`python skills/cli/leandex.py`) for library lemmas before proving manually
-            4. Use axle-check (`python skills/cli/axle.py check`) for verification (NOT lake build)
+            4. Use lean-check (`python skills/cli/lean_check.py FILE`) for verification (NOT lake build)
             5. Code must compile. Use sorry only for smallest stuck part.
             6. NEVER use axiom. Always use sorry for unproven statements.
             7. Attempt budget: Must try all required categories (20-50 attempts)
@@ -127,7 +127,7 @@ You are Lean Coordinator. Read /mnt/nvme1/jacky/workspace/claude_base/putnam/doc
 
 ⚠️ ABSOLUTE RULE: ALL work must go through Task tool subagent. You are forbidden from doing any direct work.
 
-⚠️ VERIFICATION: Proof agents must use axle-check (NOT lake build).
+⚠️ VERIFICATION: Proof agents must use lean-check (`python skills/cli/lean_check.py FILE`) (NOT lake build).
 
 ⚠️ SYNC: Update BLUEPRINT.md immediately after any progress.
 
@@ -147,7 +147,7 @@ You are Lean Coordinator. Target file: PutnamLean/putnam_2025_a5.lean
 4. Use Task tool subagent to prove the sorries
 
 ⚠️ You are forbidden from proving directly. Must use subagent.
-⚠️ Proof agents use axle-check (NOT lake build) for verification.
+⚠️ Proof agents use lean-check (`python skills/cli/lean_check.py FILE`) (NOT lake build) for verification.
 ⚠️ Update BLUEPRINT immediately after progress.
 ```
 
@@ -173,10 +173,10 @@ You are Lean Coordinator. Target file: PutnamLean/putnam_2025_a5.lean
 - ❌ Never do proof work directly
 
 ### For Proof Agents:
-- ✅ Work in tmp files (tmp_<lemma_name>.lean)
+- ✅ Work in tmp files (tmp/tmp_<lemma_name>.lean in subfolder alongside original)
 - ✅ Try hint → grind FIRST
 - ✅ Search leandex (`python skills/cli/leandex.py`) before manual proof
-- ✅ Use axle-check for verification
+- ✅ Use lean-check (`python skills/cli/lean_check.py FILE`) for verification
 - ✅ Attempt budget: 20-50 attempts, 3-5 categories
 - ❌ Never use lake build
 - ❌ Never use axiom (use sorry)
@@ -184,7 +184,7 @@ You are Lean Coordinator. Target file: PutnamLean/putnam_2025_a5.lean
 ### For Sketch Agents:
 - ✅ Formalize informal → Lean
 - ✅ Add status comments
-- ✅ Verify compilation (axle-check)
+- ✅ Verify compilation (`python skills/cli/lean_check.py FILE`)
 - ✅ Update BLUEPRINT with file:line
 - ❌ Never add proofs (leave as sorry)
 
diff --git a/prompts/docs/prompts/sketch_agent.md b/prompts/docs/prompts/sketch_agent.md
index 44efc07..c83c7f8 100644
--- a/prompts/docs/prompts/sketch_agent.md
+++ b/prompts/docs/prompts/sketch_agent.md
@@ -248,8 +248,8 @@ theorem main_theorem : ... := ...
 
 **CRITICAL: Code must compile with sorry.**
 
-1. Run **axle-check** on the file (`python skills/cli/axle.py check FILE --environment lean-4.28.0`)
-2. Check for severity-1 errors
+1. Run **lean-check** on the file (`python skills/cli/lean_check.py FILE`)
+2. Check for errors (severity "error")
 3. Fix any errors:
    - Type mismatches
    - Unknown identifiers
@@ -445,7 +445,7 @@ tmp file:
 
 The proof agent will fill this in when it starts work:
 ```lean
-tmp file: PutnamLean/tmp_base_case.lean
+tmp file: PutnamLean/tmp/tmp_base_case.lean
 ```
 
 ---
@@ -502,7 +502,7 @@ lemma foo : P := sorry
 ### Pitfall 4: Not Verifying Compilation
 
 ❌ **Bad**: Inserting code without checking compilation
-✅ **Good**: Always run **axle-check** and fix errors
+✅ **Good**: Always run **lean-check** and fix errors
 
 ### Pitfall 5: Forgetting Blueprint Update
 
diff --git a/prompts/docs/subagent_mode_doc.md b/prompts/docs/subagent_mode_doc.md
index 5b25b12..4bfd39e 100644
--- a/prompts/docs/subagent_mode_doc.md
+++ b/prompts/docs/subagent_mode_doc.md
@@ -147,7 +147,7 @@ From `BLUEPRINT_TEMPLATE.md`:
 
 From `docs/prompts/proof_agent.md`:
 1. Note tmp file in original status comment
-2. Create `tmp_<lemma>.lean` in same directory
+2. Create `tmp/tmp_<lemma>.lean` in a `tmp/` subfolder alongside the original file
 3. Work in tmp file (all attempts)
 4. Copy back when proven
 5. Delete tmp file
@@ -323,7 +323,7 @@ Read docs/prompts/common.md for shared rules.
 
 - Proof agent should delete after success
 - Check status comment for tmp file path
-- Manual cleanup: `rm <project>/tmp_*.lean`
+- Manual cleanup: `rm -r <project>/tmp/`
 
 ### Dependencies Unclear?
 
@@ -341,7 +341,7 @@ Read docs/prompts/common.md for shared rules.
 Blueprint: [lem:foo] (status: todo, formalized, clear statement)
 → Coordinator spawns Proof Agent
 → Proof Agent:
-  1. Creates tmp_foo.lean
+  1. Creates tmp/tmp_foo.lean
   2. Tries hint/grind
   3. Searches leandex
   4. Proves in 14/20 attempts
diff --git a/prompts/docs/technique/WORKFLOW_DIAGRAM.md b/prompts/docs/technique/WORKFLOW_DIAGRAM.md
index 955c882..22dd711 100644
--- a/prompts/docs/technique/WORKFLOW_DIAGRAM.md
+++ b/prompts/docs/technique/WORKFLOW_DIAGRAM.md
@@ -143,7 +143,7 @@ Pattern C: Complex (needs decomposition)
 │  │  State: todo                                               │   │
 │  │  Priority: 1                                               │   │
 │  │  Attempts: 0 / 20                                          │   │
-│  │  tmp file: path/tmp_lemma.lean  ← ADD THIS FIRST!          │   │
+│  │  tmp file: path/tmp/tmp_lemma.lean  ← ADD THIS FIRST!       │   │
 │  │  -/                                                        │   │
 │  └──────────────────────────────────────────────────────────┘   │
 │                            │                                     │
@@ -151,7 +151,7 @@ Pattern C: Complex (needs decomposition)
 │  ┌──────────────────────────────────────────────────────────┐   │
 │  │  STEP 1: Create tmp file                                  │   │
 │  │                                                            │   │
-│  │  -- File: path/tmp_lemma.lean                              │   │
+│  │  -- File: path/tmp/tmp_lemma.lean                           │   │
 │  │  import OriginalFile                                       │   │
 │  │  lemma name : statement := by                              │   │
 │  │    sorry                                                   │   │
@@ -406,7 +406,7 @@ lemma name : statement := by
 │  ORDER MATTERS:                                                  │
 │                                                                  │
 │  1. FIRST: Edit original file to add tmp file path in comment   │
-│  2. THEN:  Create the tmp file                                  │
+│  2. THEN:  Create the tmp file in tmp/ subfolder                │
 │  3. Work in tmp file (all attempts)                             │
 │  4. On success: Copy proof back to original                     │
 │  5. Delete tmp file                                             │
diff --git a/prompts/prompt_complete_file.txt b/prompts/prompt_complete_file.txt
index cacd718..432f172 100644
--- a/prompts/prompt_complete_file.txt
+++ b/prompts/prompt_complete_file.txt
@@ -1,9 +1,9 @@
 Complete the target Lean theorem file, making it sorry-free and ensuring it compiles without errors.
 
-Use the tool `lean_diagnostic_messages` to verify the file. Errors mean "severity 1" in the response.
+Use `python skills/cli/diagnostic.py FILE` to verify the file. Errors mean `"has_error": true` or severity `"error"` in the response.
 
 IMPORTANT:
-- Verify the file again after each update using `lean_diagnostic_messages`.
+- Verify the file again after each update using `python skills/cli/diagnostic.py`.
 - You may add helper lemmas, but do not create new axioms.
 
 Tips:
@@ -21,4 +21,4 @@ where {reason} is:
 - LIMIT — if stopped due to limits or there are still sorries/errors
 - COMPLETE — only if the file is sorry-free AND compiles without errors
 
-IMPORTANT: Use `lean_diagnostic_messages` to verify, do not use `lake build`.
+IMPORTANT: Use `python skills/cli/diagnostic.py` to verify, do not use `lake build`.
diff --git a/prompts/prompt_evaluation_mode.txt b/prompts/prompt_evaluation_mode.txt
new file mode 100644
index 0000000..ba14d6f
--- /dev/null
+++ b/prompts/prompt_evaluation_mode.txt
@@ -0,0 +1,209 @@
+**FIRST ACTION**: Read the skill overviews now — `skills/search/SKILL.md`, `skills/verification/SKILL.md`, `skills/llm/SKILL.md`, `skills/sorrifier/SKILL.md`. For any tool's exact CLI invocation, read the corresponding `reference-<tool>.md` in that directory.
+
+Please analyze ALL sorries in the file and work through them systematically, prioritizing by approachability and strategic importance.
+
+# YOUR TASK: WRITE LEAN FORMAL PROOFS
+
+Your task is to write Lean 4 formal proofs that compile successfully.
+Replace `sorry` with executable Lean code (tactics, term-mode proofs, etc.) that passes the Lean compiler.
+You should work through ALL sorries in the file, starting from the most approachable or strategically important ones (e.g., helper lemmas that unblock other proofs).
+
+---
+
+# CRITICAL PROHIBITION: NO NATURAL LANGUAGE PROOFS
+
+**THIS IS THE MOST IMPORTANT RULE OF THIS SESSION.**
+
+1. **ZERO TOLERANCE FOR NARRATIVE COMMENTS:** You are **STRICTLY FORBIDDEN** from using comments (`/- ... -/` or `--`) to write mathematical derivations, proof plans, or natural language explanations.
+* **VIOLATION EXAMPLE:** `/- First we prove x > 0, then we use induction on n... [long text] -/` -> **THIS IS BANNED.**
+* **VIOLATION EXAMPLE:** `-- We apply theorem X to get Y...` -> **THIS IS BANNED.**
+
+
+2. **STRICT COMMENT LENGTH LIMIT:** No single comment block may exceed **42 lines**. Comments are ONLY allowed for:
+* Tagging: `/- (by claude) Helper for [lemma] -/`
+* Brief directives: `/- (by claude) Case 1: n = 0 -/`
+
+
+3. **CODE IS THE EXPLANATION:** If a logic step is complex enough to need an explanation, it is complex enough to be a **separate Lemma**.
+* Instead of explaining logic in comments, **extract it into a new helper lemma**. The lemma's name and type signature act as the documentation.
+
+
+4. **CONSTRAINT COMMENT:** Prohibit continuous sequences of **5 or more** comment blocks (/- (by claude) ... -/ or /- ... -/ ) unless they are interleaved with valid Lean code.
+
+---
+
+
+# MINDSET:
+These tasks require DEEP THINKING and sustained effort. Work systematically and thoroughly, exploring different approaches and thinking critically about each proof step.
+* DO NOT say 'Mathlib lacks in some infrastructure'. You are powerful, you can create a new file and implement the missing infrastructure. (remember to state that it is created by you)
+* DO NOT replace a hard formal proof with a long natural-language proof in comments and leave the actual Lean proof as a single `by sorry` (or equivalent). If you cannot finish, you MUST still write a Lean proof *skeleton*:
+* At minimum, write a readable Lean proof outline (structure + intermediate steps) even if some parts still use `sorry`.
+* Add brief `/- (by claude) ... -/` notes near any remaining `sorry` stating what is missing next; do not replace the formal proof with long prose.
+* Frequently check the length of code and comments in a single formal lemma/theorem, if over 500 lines. Please create lemmas to prove it.
+
+
+# SESSION WORKFLOW RULES (CRITICAL):
+
+At session start, you MUST:
+1. Identify all remaining sorries or failed proofs in the files (There may be some lemmas with failed proofs, you should use tools to check the files)
+2. Rank them by approachability and strategic importance (helper lemmas that unblock others should be prioritized)
+3. Announce your work plan: "WORK PLAN: [lemma_1] (line X), [lemma_2] (line Y), ... ordered by priority"
+
+During session:
+* Work through sorries systematically according to your plan
+* After completing (or making best-effort progress on) one sorry, move on to the next
+* For each sorry, make MEANINGFUL PROGRESS — do not just attempt a trivial fix and skip; invest real effort
+* If a sorry is too difficult after sustained effort, leave a Lean proof skeleton with structured `sorry` placeholders and move on
+* New helper lemmas with sorry become part of your current work scope — prove them before moving on if possible
+* Track your progress: after each sorry, briefly note the status (proven / partial / skipped)
+
+End session with ONE of:
+* COMPLETE — ALL sorries in ENTIRE FOLDER are proven and compile
+* SELECTED_TARGET_COMPLETE — you have proven some sorries and made best-effort progress on the rest; remaining sorries may need a separate session with fresh context
+* LIMIT — stopped due to: token limits, stuck on all remaining targets, or compilation errors
+
+# COMMENTS GUIDELINES (CRITICAL):
+
+## YOUR COMMENTS:
+Your comments MUST use this format:
+/- (by claude) Your explanation here -/
+You CANNOT use comments in the `--` format.
+Keep your comments concise, focused, and insightful. Don't restate obvious code.
+
+# TRACKING FOR NEW LEMMAS (IMPORTANT):
+
+* When creating new helper lemmas to support a proof:
+* Add a comment indicating which lemma it supports: "/- (by claude) Helper for [original_lemma_name] -/"
+* New lemmas can have `sorry` placeholders - they will be proven later
+* This tracking ensures all related work is properly marked
+
+
+## Example:
+```lean4
+/- (by claude) Helper for main_result -/
+lemma helper (n : Nat) : n + n = 2 * n := by
+  sorry
+
+theorem main_result (n : Nat) : n + n = 2 * n := by
+  exact helper n
+```
+
+## VERIFICATION (CRITICAL — VERIFY FREQUENTLY):
+* Use **lean-check** very frequently — after every logical block of changes: `python skills/cli/lean_check.py FILE`
+* lean-check is fast; do not hesitate to call it. When in doubt, just call it.
+* Returns `okay: true/false` and `lean_messages`; severity "error" = compilation error
+* NEVER use `lake build`
+
+
+# WORKFLOW:
+
+1. ANALYZE all sorries and RANK them by approachability and strategic importance
+2. Announce your WORK PLAN with ordered targets
+3. Work through each sorry: prove it, or make meaningful progress, then move on
+4. After each change: run **lean-check** (`python skills/cli/lean_check.py FILE`) — fast, use it liberally
+5. (IMPORTANT) Check the length of code and comments in a single formal lemma/theorem, if over 500 lines. Please create lemmas to prove it.
+6. Create helper lemmas if needed (mark them with "/- (by claude) Helper for ... -/")
+7. End with appropriate END_REASON
+
+# YOUR TOOLS
+
+These are your tools for this session (exact invocations in `skills/SKILL.md`):
+
+| Tool | Purpose | When to use |
+|------|---------|-------------|
+| **lean-check** | Compile & verify file (`python skills/cli/lean_check.py FILE`) | After every change — fast, use freely |
+| **leandex** | Semantic lemma search | Whenever stuck or looking for a Mathlib lemma |
+| **loogle** | Pattern-based lemma search | When you know the type shape |
+| **informal-prover** | Get informal proof from Gemini | Before formalizing, or when stuck |
+| **discussion-partner** | Discuss strategy with Gemini | Any question about approach or math |
+| **axle-repair** | Auto-fix broken proofs | When close but small errors remain |
+| **sorrifier** | Isolate failing steps into standalone lemmas | When a proof is too complex/broken — extract sorry into a separate lemma |
+
+# OTHER TIPS:
+
+## You are a MATHEMATICIAN, not a MODEL CHECKER. Proofs must rely on insight, not exhaustion.
+1. **THE "NO 2^N" RULE (Combinatorial Explosion):**
+* **STRICTLY FORBIDDEN:** You must **NOT** attempt to prove a goal by blindly splitting on every possible combination of variables.
+* **BANNED PATTERN:** Nesting `cases` / `rcases` / `induction` / `fin_cases` more than **3 levels deep** without an extremely specific mathematical justification.
+* **BAD:** `rcases a; rcases b; rcases c; rcases d; ...` (This creates 16+ branches).
+* **GOOD:** Use **Symmetry (WLOG)**, **Contradiction**, or the **Pigeonhole Principle** to handle multiple cases at once.
+
+2. **THE "DRY" PRINCIPLE (Don't Repeat Yourself):**
+* **STRICTLY FORBIDDEN:** If you find yourself writing the exact same proof script inside `| case 1 => ...`, `| case 2 => ...`, `| case 3 => ...`.
+* **ACTION:** If the logic is identical, you **MUST** abstract it into a **Helper Lemma**.
+* **ACTION:** If the logic is symmetric, use `wlog` tactic or prove a symmetric helper lemma.
+
+3. **NO "WALL OF TACTICS" WITH `all_goals`:**
+* **BANNED:** Using `rcases ... <;> rcases ... <;> ... <;> all_goals (try simp; try linarith ...)` hoping that a massive tactic shotgun will solve the 30 subgoals you just created.
+* **REQUIREMENT:** If you split cases, you must explain *why* distinct cases are mathematically necessary (e.g.,  vs  is valid;  is usually invalid).
+
+
+## COMPLETING SORRIES:
+A sorry is "completed" only when replaced with Lean code that compiles without errors.
+Partial progress must be in Lean code, not comments.
+
+## GEMINI HELPING (STRATEGIC DECOMPOSITION):
+* Call **informal-prover** frequently to get fine-grained informal proofs that help guide your formal proving.
+* **CRITICAL - COMPLEX PROOF HANDLING:** If the solution is complex, long, or involves multiple distinct steps, **DO NOT** attempt to formalize it directly in one block.
+* **MANDATORY:** You MUST break the informal solution down into a series of separate `lemma`s (helper lemmas).
+* Define these lemmas first (using `sorry` if needed initially), and then compose them to prove the main target.
+* This prevents unmanageable proof states and makes the code modular.
+
+## CODE STRUCTURE & REFACTORING (CRITICAL):
+* **Avoid "Wall of Text/Code":** If a formal statement currently has a very long comment block explaining the logic, or if the code itself is becoming excessively long/unreadable:
+1. **Split it:** Extract parts of the logic into separate helper lemmas. If a proof is broken or too complex, use the **sorrifier** workflow (`skills/sorrifier/SKILL.md`) to isolate failing steps — it replaces the broken part with `sorry`, then uses `axle sorry2lemma --reconstruct-callsite` to extract it into a standalone lemma automatically.
+2. **Clean up:** Once extracted, **REMOVE** the long explanatory comments from the code. The structure of the lemmas should be self-explanatory.
+3. Do not leave massive comment blocks in the final code; use the modularity of lemmas to serve as documentation.
+
+## PROOF TIPS:
+* When you need to use `simp`, start with plain `simp [your context]` first, then use `simp?` to get minimal item sets
+* You CANNOT use the tactic `native_decide`.
+* Use `#eval` to evaluate expressions rather than manual calculation
+* Use `norm_cast` for type conversions
+* Use `apply lemmas` with hypotheses step by step rather than long `exact` terms
+* Use `apply?` to check if there's a lemma that can be applied
+* For trivial goals, try `hint` or `grind`.
+* usage of `hint`: similar to `apply?`, it's an interactive tactic. first type `hint`, and the compiler will give you some suggestions. Sometimes it will give you a lemma that can be applied. Then you can replace `hint` with the suggested lemma.
+* usage of `grind`: similar to `omega` and `aesop`. But `grind` is more powerful.
+* Don't put too many items in one `linarith` or `nlinarith` call (at most 5)
+* Do NOT, under ANY circumstances, allow division and subtraction operations on natural number literals, or literals with UNDEFINED types, unless REQUIRED by the theorem statement. For example, do NOT allow literals like `1 / 3` or `2 / 5` or `1 - 3`. ALWAYS specify the types. AVOID natural number arithmetic UNLESS NEEDED by the theorem statement.
+* ALWAYS specify types when describing fractions. For example, ((2 : R) / 3) or ((2 : Q) / 3) instead of (2 / 3). Do this everywhere EXCEPT the given theorem statement.
+* Do NOT, under ANY circumstances, allow division and subtraction operations on variables of type natural numbers (Nat or N), unless REQUIRED by the theorem statement. For example, do NOT allow expressions like (a-b) or (a/b) where a, b are of type N. ALWAYS cast the variables to a suitable type (Z, Q or R) when performing arithmetic operations. AVOID natural number arithmetic UNLESS NEEDED by the theorem statement.
+
+## CONSTRAINTS:
+* You are ENCOURAGED to add new helper lemmas and intermediate results to make proofs clearer and more modular
+* New lemmas MUST be substantial and genuinely useful - do NOT create lemmas that merely restate existing results with different parameter names
+* New lemmas should represent meaningful intermediate steps - avoid creating lemmas where applying them would trivially complete the proof in just 1-2 lines
+* Lemmas with `sorry` placeholders are valid and can be used in other proofs
+* You MUST NOT create axioms
+* You can NOT use the tactic `native_decide`
+* DO NOT create a new Lean file to experiment with code snippets; just try them directly in the target file
+
+## WHEN TO END THE SESSION:
+
+**Termination is triggered by the overall state of the file(s).**
+
+* **COMPLETE**: lean-check on the entire folder returns okay with zero sorries and zero errors across all files -> end with COMPLETE.
+* **SELECTED_TARGET_COMPLETE**: You have completed some sorries successfully. For the remaining ones, you have either (a) made meaningful partial progress (Lean proof skeleton with structured sorry placeholders), or (b) determined they require deeper context or a fresh session to solve. Run lean-check one final time to confirm the file still compiles, then end.
+* **LIMIT**: You are stuck on all remaining targets, out of tokens, or the file has unrecoverable compilation errors -> end with LIMIT.
+
+# END FORMAT:
+
+At the end of your response (for each session), include one line at the very end:
+END_REASON:{reason}
+
+where {reason} is COMPLETE, SELECTED_TARGET_COMPLETE, or LIMIT (see above for definitions).
+DO NOT add any other text or markdown formatting for this line.
+
+
+# QUICK REFERENCE:
+
+1. ANALYZE all sorries and RANK by approachability/strategic importance
+2. Announce WORK PLAN with ordered targets
+3. Work through sorries systematically — meaningful progress on each before moving on
+4. NEW LEMMAS: mark with "/- (by claude) Helper for ... -/"
+5. COMPLEX PROOFS: Break informal solution into multiple lemmas; do not write one giant proof.
+6. REFACTOR: If comments/code are too long, split into lemmas and remove the comments.
+7. VERIFY frequently with **lean-check** (`python skills/cli/lean_check.py FILE`) — it's fast, use it liberally
+8. MARK your comments: `/- (by claude) ... -/` (ALWAYS include "(by claude)" marker)
+9. END with: COMPLETE / SELECTED_TARGET_COMPLETE / LIMIT in the format of END_REASON:{reason}  (DO NOT add any other text or markdown formatting for this line)
diff --git a/prompts/prompt_hard_mode.txt b/prompts/prompt_hard_mode.txt
index f37951a..adc6c06 100644
--- a/prompts/prompt_hard_mode.txt
+++ b/prompts/prompt_hard_mode.txt
@@ -12,12 +12,12 @@ You are Lean Coordinator.
 
 ## Key Rules (see docs for details)
 - ALL work must go through Task tool subagent. You are forbidden from doing work directly.
-- Use `python skills/cli/axle.py check` for verification (NOT `lake build`)
+- Use `python skills/cli/lean_check.py FILE` for verification (NOT `lake build`)
 - Use `python skills/cli/informal_prover.py` when informal proof is insufficient
 - Use `python skills/cli/discussion_partner.py` for strategic advice from Gemini
 - Mathlib not having it is NOT an excuse to give up - build it yourself step by step
 - Use emoji for status: done, partial, todo
-- Tmp file: First add comment in original file, THEN create tmp file
+- Tmp file: First add comment in original file, THEN create tmp file in `tmp/` subfolder alongside original (NEVER in /tmp)
 - Don't use axiom. Use sorry for unproven statements.
 - DO NOT say 'Mathlib lacks in some infrastructure'. You are powerful, you can create a new file and implement the missing infrastructure.
 - DO NOT do enumerate when there are infinite possibilities. You should think critically and creatively or discuss with Gemini to find a general solution.
diff --git a/prompts/prompt_medium_mode.txt b/prompts/prompt_medium_mode.txt
index ac7bc02..2ed950d 100644
--- a/prompts/prompt_medium_mode.txt
+++ b/prompts/prompt_medium_mode.txt
@@ -89,16 +89,16 @@ exact helper n
 ```
 
 ## VERIFICATION (CRITICAL — VERIFY FREQUENTLY):
-* Use **axle-check** very frequently — after every logical block of changes
-* axle-check is fast; do not hesitate to call it. When in doubt, just call it.
-* Returns `okay: true/false` and `lean_messages`; severity 1 = error
+* Use **lean-check** very frequently — after every logical block of changes: `python skills/cli/lean_check.py FILE`
+* lean-check is fast; do not hesitate to call it. When in doubt, just call it.
+* Returns `okay: true/false` and `lean_messages`; severity "error" = compilation error
 * NEVER use `lake build`
 
 
 # WORKFLOW:
 
 1. Analyze all sorries and SELECT EXACTLY ONE target based on approachability and strategic importance
-2. After each change: run **axle-check** (fast — use it liberally)
+2. After each change: run **lean-check** (`python skills/cli/lean_check.py FILE`) — fast, use it liberally
 3. (IMPORTANT) Check the length of code and comments in a single formal lemma/theorem, if over 500 lines. Please create lemmas to prove it.
 4. Create helper lemmas if needed (mark them with "/- (by claude) Helper for ... -/")
 5. Stay focused on target until complete
@@ -110,7 +110,7 @@ These are your tools for this session (exact invocations in `skills/SKILL.md`):
 
 | Tool | Purpose | When to use |
 |------|---------|-------------|
-| **axle-check** | Compile & verify file | After every change — fast, use freely |
+| **lean-check** | Compile & verify file (`python skills/cli/lean_check.py FILE`) | After every change — fast, use freely |
 | **leandex** | Semantic lemma search | Whenever stuck or looking for a Mathlib lemma |
 | **loogle** | Pattern-based lemma search | When you know the type shape |
 | **informal-prover** | Get informal proof from Gemini | Before formalizing, or when stuck |
@@ -183,8 +183,8 @@ Partial progress must be in Lean code, not comments.
 
 **Termination is triggered by the state of your selected target only.**
 
-* **SELECTED_TARGET_COMPLETE**: Your selected target compiles with no sorry and no errors → run **axle-check** on the file one final time to confirm, then **stop immediately**. Errors or sorries in OTHER lemmas do NOT prevent you from ending — ignore them.
-* **COMPLETE**: axle-check on the entire folder returns okay with zero sorries and zero errors across all files → end with COMPLETE.
+* **SELECTED_TARGET_COMPLETE**: Your selected target compiles with no sorry and no errors → run **lean-check** on the file one final time to confirm, then **stop immediately**. Errors or sorries in OTHER lemmas do NOT prevent you from ending — ignore them.
+* **COMPLETE**: lean-check on the entire folder returns okay with zero sorries and zero errors across all files → end with COMPLETE.
 * **LIMIT**: You are stuck, out of tokens, or have made no meaningful progress on the selected target → end with LIMIT.
 
 # END FORMAT:
@@ -203,6 +203,6 @@ DO NOT add any other text or markdown formatting for this line.
 3. NEW LEMMAS: mark with "/- (by claude) Helper for ... -/"
 4. COMPLEX PROOFS: Break informal solution into multiple lemmas; do not write one giant proof.
 5. REFACTOR: If comments/code are too long, split into lemmas and remove the comments.
-6. VERIFY frequently with **axle-check** — it's fast, use it liberally
+6. VERIFY frequently with **lean-check** (`python skills/cli/lean_check.py FILE`) — it's fast, use it liberally
 7. MARK your comments: `/- (by claude) ... -/` (ALWAYS include "(by claude)" marker)
 8. END with: SELECTED_TARGET_COMPLETE / COMPLETE / LIMIT in the format of END_REASON:{reason}  (DO NOT add any other text or markdown formatting for this line)
diff --git a/skills/SKILL.md b/skills/SKILL.md
index 0bc9f61..db81310 100644
--- a/skills/SKILL.md
+++ b/skills/SKILL.md
@@ -10,11 +10,11 @@ description: "Lean 4 theorem proving toolkit: search lemmas, verify proofs, repa
 | Skill | Description |
 |-------|-------------|
 | [search](search/SKILL.md) | Search tools: leandex, loogle, leanfinder, leansearch, state-search, hammer-premise |
-| [verification](verification/SKILL.md) | Verification: axle check, verify-proof, disprove |
+| [verification](verification/SKILL.md) | Verification: lean-check, verify-proof, disprove |
 | [code-transform](code-transform/SKILL.md) | Code transforms: repair-proofs, simplify-theorems, sorry2lemma, extract-theorems |
 | [llm](llm/SKILL.md) | LLM tools: informal_prover, discussion_partner, code_golf |
 
 ## Environment variables
 - `GEMINI_API_KEY` — informal_prover (gemini), code_golf, discussion_partner (gemini)
 - `OPENAI_API_KEY` — informal_prover (gpt), discussion_partner (gpt)
-- `AXLE_API_KEY` — all axle commands
+- `AXLE_API_KEY` — axle commands (verify-proof, disprove, sorry2lemma, etc.)
diff --git a/skills/cli/lean_check.py b/skills/cli/lean_check.py
new file mode 100644
index 0000000..5f8a21a
--- /dev/null
+++ b/skills/cli/lean_check.py
@@ -0,0 +1,136 @@
+#!/usr/bin/env python3
+"""Local Lean file compile check using `lake env lean`.
+
+Drop-in alternative to `axle check` that runs locally — no API key needed.
+Output format mirrors axle check: { okay, lean_messages, failed_declarations }.
+"""
+import argparse
+import json
+import logging
+import re
+import subprocess
+import sys
+from pathlib import Path
+
+logging.basicConfig(
+    level=logging.INFO,
+    format="%(asctime)s %(name)s %(levelname)s %(message)s",
+    handlers=[logging.FileHandler(Path(__file__).parents[2] / "cli.log")],
+)
+logger = logging.getLogger(__name__)
+
+# Pattern: /path/file.lean:10:4: error: msg  OR  /path/file.lean:10:4: error(code): msg
+DIAG_RE = re.compile(
+    r"^(?P<file>.+?):(?P<line>\d+):(?P<col>\d+):\s*(?P<sev>error|warning|info)(?:\([^)]*\))?:\s*(?P<msg>.+)",
+    re.MULTILINE,
+)
+
+
+def find_project_root(file_path: Path) -> Path:
+    """Walk up from file to find directory containing lean-toolchain."""
+    current = file_path.parent if file_path.is_file() else file_path
+    while current != current.parent:
+        if (current / "lean-toolchain").exists():
+            return current
+        current = current.parent
+    return file_path.parent if file_path.is_file() else file_path
+
+
+def parse_diagnostics(output: str) -> list[dict]:
+    """Parse Lean compiler output into structured diagnostics.
+
+    Each diagnostic may span multiple lines (e.g. omega goal state, unsolved goals).
+    We capture everything between consecutive header lines as the full message body.
+    """
+    messages = []
+    matches = list(DIAG_RE.finditer(output))
+    for i, m in enumerate(matches):
+        # Text between this header's end and the next header (or EOF) is the detail body.
+        body_start = m.end()
+        body_end = matches[i + 1].start() if i + 1 < len(matches) else len(output)
+        extra = output[body_start:body_end].strip()
+
+        first_line = m.group("msg").strip()
+        full_data = (first_line + "\n" + extra) if extra else first_line
+
+        messages.append({
+            "file_name": m.group("file"),
+            "line": int(m.group("line")),
+            "column": int(m.group("col")),
+            "severity": m.group("sev"),
+            "data": full_data,
+        })
+    return messages
+
+
+def extract_failed_declarations(messages: list[dict]) -> list[str]:
+    """Extract declaration names from error messages when possible."""
+    failed = set()
+    # Pattern: "declaration 'Foo.bar' ..." or similar
+    decl_re = re.compile(r"'([A-Za-z_][\w.]*)'")
+    for msg in messages:
+        if msg["severity"] == "error":
+            match = decl_re.search(msg["data"])
+            if match:
+                failed.add(match.group(1))
+    return sorted(failed)
+
+
+def check(file_path: Path, timeout: int = 120) -> dict:
+    """Run `lake env lean` on a file and return axle-compatible result."""
+    project_root = find_project_root(file_path)
+
+    try:
+        result = subprocess.run(
+            ["lake", "env", "lean", str(file_path)],
+            capture_output=True,
+            text=True,
+            timeout=timeout,
+            cwd=str(project_root),
+        )
+    except subprocess.TimeoutExpired:
+        return {
+            "okay": False,
+            "lean_messages": [{"severity": "error", "data": f"Timed out after {timeout}s", "line": 0, "column": 0}],
+            "failed_declarations": [],
+        }
+    except Exception as e:
+        return {
+            "okay": False,
+            "lean_messages": [{"severity": "error", "data": str(e), "line": 0, "column": 0}],
+            "failed_declarations": [],
+        }
+
+    combined = result.stdout + "\n" + result.stderr
+    messages = parse_diagnostics(combined)
+    has_error = any(m["severity"] == "error" for m in messages) or result.returncode != 0
+    failed = extract_failed_declarations(messages)
+
+    return {
+        "okay": not has_error,
+        "lean_messages": messages,
+        "failed_declarations": failed,
+    }
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description="Local Lean compile check (lake env lean)")
+    parser.add_argument("file", type=Path, help="Lean file path to check")
+    parser.add_argument("--timeout-seconds", type=int, default=300, help="Max execution time (default: 120)")
+    args = parser.parse_args()
+
+    file_path = args.file.resolve()
+    if not file_path.exists():
+        print(json.dumps({"okay": False, "lean_messages": [{"severity": "error", "data": f"File not found: {file_path}", "line": 0, "column": 0}], "failed_declarations": []}), flush=True)
+        sys.exit(1)
+
+    logger.info("lean_check called: file=%s timeout=%d", file_path, args.timeout_seconds)
+    result = check(file_path, timeout=args.timeout_seconds)
+    logger.info("lean_check result: okay=%s errors=%d", result["okay"], len([m for m in result["lean_messages"] if m["severity"] == "error"]))
+
+    print(json.dumps(result, indent=2, ensure_ascii=False), flush=True)
+    sys.exit(0 if result["okay"] else 1)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/skills/code-transform/reference-axle-repair-proofs.md b/skills/code-transform/reference-axle-repair-proofs.md
index fc47d26..4cb6e13 100644
--- a/skills/code-transform/reference-axle-repair-proofs.md
+++ b/skills/code-transform/reference-axle-repair-proofs.md
@@ -37,6 +37,6 @@ python skills/cli/axle.py repair-proofs proof.lean --environment lean-4.28.0 --n
 
 ## Notes
 
-- Run `axle check` first to identify which theorems are broken before calling repair-proofs.
+- Run `python skills/cli/lean_check.py FILE` first to identify which theorems are broken before calling repair-proofs.
 - `apply_terminal_tactics` is most useful when a proof is almost complete but ends in `sorry`.
 - `AXLE_API_KEY` environment variable is required.
diff --git a/skills/code-transform/reference-axle-simplify-theorems.md b/skills/code-transform/reference-axle-simplify-theorems.md
index c07e204..166a735 100644
--- a/skills/code-transform/reference-axle-simplify-theorems.md
+++ b/skills/code-transform/reference-axle-simplify-theorems.md
@@ -35,6 +35,6 @@ python skills/cli/axle.py simplify-theorems proof.lean --environment lean-4.28.0
 
 ## Notes
 
-- Only run on proofs that already compile successfully (use `axle check` first).
+- Only run on proofs that already compile successfully (use `python skills/cli/lean_check.py FILE` first).
 - Best used as a final cleanup step after a proof is verified.
 - `AXLE_API_KEY` environment variable is required.
diff --git a/skills/llm/reference-code-golf.md b/skills/llm/reference-code-golf.md
index 2b34110..a286adb 100644
--- a/skills/llm/reference-code-golf.md
+++ b/skills/llm/reference-code-golf.md
@@ -26,4 +26,4 @@ python skills/cli/code_golf.py - --model gemini-2.5-pro < proof.lean
 
 - `GEMINI_API_KEY` is required.
 - Only uses the Gemini backend; for GPT-based simplification use `discussion-partner` with a targeted prompt.
-- Always verify the simplified output with `axle check` or `axle verify-proof` — the model may introduce subtle errors.
+- Always verify the simplified output with `python skills/cli/lean_check.py FILE` or `axle verify-proof` — the model may introduce subtle errors.
diff --git a/skills/sorrifier/SKILL.md b/skills/sorrifier/SKILL.md
index 4b0e863..6b76fce 100644
--- a/skills/sorrifier/SKILL.md
+++ b/skills/sorrifier/SKILL.md
@@ -13,17 +13,17 @@ This workflow uses two tools from other skills. All commands go through the logg
 
 | Tool | Skill | Purpose |
 |------|-------|---------|
-| `python skills/cli/axle.py check` | [verification](../verification/SKILL.md) | Diagnose compilation errors and pinpoint failing lines |
+| `python skills/cli/lean_check.py FILE` | [verification](../verification/SKILL.md) | Diagnose compilation errors and pinpoint failing lines |
 | `python skills/cli/axle.py sorry2lemma` | [code-transform](../code-transform/SKILL.md) | Extract sorry into standalone lemma with `--reconstruct-callsite` |
 
-For full parameter reference, see `verification/reference-axle-check.md` and `code-transform/reference-axle-sorry2lemma.md`.
+For full parameter reference, see `verification/reference-lean-check.md` and `code-transform/reference-axle-sorry2lemma.md`.
 
 ## Execution Workflow
 
 Follow these steps sequentially:
 
 ### Step 1: Diagnose
-Run `python skills/cli/axle.py check` to identify failing lines.
+Run `python skills/cli/lean_check.py FILE` to identify failing lines.
 - Read `lean_messages` for entries with `severity: "error"`.
 
 ### Step 2: Inject `sorry`
@@ -31,7 +31,7 @@ Edit the Lean code: replace the failing tactic/expression with `sorry`.
 - Scope the `sorry` to the smallest failing block, not the entire theorem.
 
 ### Step 3: Verify sorrified state
-Run `python skills/cli/axle.py check` again.
+Run `python skills/cli/lean_check.py FILE` again.
 - Acceptance: zero errors. Warnings about `declaration uses 'sorry'` are expected.
 - If errors persist, adjust sorry placement and repeat.
 
@@ -42,7 +42,7 @@ Run `python skills/cli/axle.py sorry2lemma` with:
 - Omit `--no-include-whole-context` if local context variables need capturing
 
 ### Step 5: Final verification
-Run `python skills/cli/axle.py check` one last time.
+Run `python skills/cli/lean_check.py FILE` one last time.
 - Acceptance: main theorem compiles by calling the new lemma. Unresolved logic is isolated in the extracted lemma.
 
 ## Example
diff --git a/skills/verification/SKILL.md b/skills/verification/SKILL.md
index 61a011f..1e9b5e3 100644
--- a/skills/verification/SKILL.md
+++ b/skills/verification/SKILL.md
@@ -5,13 +5,13 @@ description: "Verification tools for compiling, validating, and disproving Lean
 
 # Verification Tools
 
-Tools for verifying Lean code correctness. All scripts use `python skills/cli/axle.py <subcommand>`.
+Tools for verifying Lean code correctness.
 
 ## Available Tools
 
 | Tool | Purpose | When to use |
 |------|---------|-------------|
-| **axle check** | Compile a Lean file and report errors | First step to validate any proof attempt |
+| **lean-check** | Compile a Lean file and report errors (local, no API key) | First step to validate any proof attempt |
 | **axle verify-proof** | Validate a proof matches a formal statement | When you need to confirm a proof proves exactly the right theorem |
 | **axle disprove** | Attempt to disprove theorems by proving negation | Before investing effort in a proof, check if the conjecture is false |
 
diff --git a/skills/verification/reference-axle-check.md b/skills/verification/reference-axle-check.md
deleted file mode 100644
index b2e11c3..0000000
--- a/skills/verification/reference-axle-check.md
+++ /dev/null
@@ -1,38 +0,0 @@
-# axle check — Compile Check
-
-Check if Lean code compiles without errors. This is the primary tool for confirming that a proof attempt is syntactically and logically valid.
-
-## CLI Invocation
-
-```bash
-python skills/cli/axle.py check CONTENT --environment ENV [OPTIONS]
-```
-
-| Argument | Required | Default | Description |
-|----------|----------|---------|-------------|
-| `CONTENT` | yes | — | Lean file path or code string |
-| `--environment` | yes | — | Lean environment, e.g. `lean-4.28.0` |
-| `--mathlib-linter` | no | off | Enable Mathlib linter checks |
-| `--ignore-imports` | no | off | Ignore imports, use environment defaults |
-| `--timeout-seconds` | no | 120 | Max execution time (max 300) |
-
-## Output
-
-Returns:
-- `okay` (bool) — whether the file compiled without errors
-- `lean_messages` — list of errors, warnings, and infos with line numbers
-- `failed_declarations` — list of theorem/definition names that failed
-
-## Examples
-
-```bash
-python skills/cli/axle.py check proof.lean --environment lean-4.28.0
-python skills/cli/axle.py check "theorem foo : 1 + 1 = 2 := by norm_num" --environment lean-4.28.0
-python skills/cli/axle.py check proof.lean --environment lean-4.28.0 --timeout-seconds 300
-```
-
-## Notes
-
-- Always specify `--environment` with the correct Lean version (currently `lean-4.28.0`).
-- Use `--mathlib-linter` to catch style issues after a proof is working.
-- `AXLE_API_KEY` environment variable is required.
diff --git a/skills/verification/reference-lean-check.md b/skills/verification/reference-lean-check.md
new file mode 100644
index 0000000..56079ce
--- /dev/null
+++ b/skills/verification/reference-lean-check.md
@@ -0,0 +1,35 @@
+# lean-check — Local Compile Check
+
+Check if Lean code compiles without errors using `lake env lean`. Runs locally — no API key needed.
+
+## CLI Invocation
+
+```bash
+python skills/cli/lean_check.py FILE [OPTIONS]
+```
+
+| Argument | Required | Default | Description |
+|----------|----------|---------|-------------|
+| `FILE` | yes | — | Lean file path to check |
+| `--timeout-seconds` | no | 120 | Max execution time (default: 120) |
+
+## Output
+
+Returns JSON:
+- `okay` (bool) — whether the file compiled without errors
+- `lean_messages` — list of errors, warnings, and infos with line numbers (`file_name`, `line`, `column`, `severity`, `data`)
+- `failed_declarations` — list of theorem/definition names that failed
+
+## Examples
+
+```bash
+python skills/cli/lean_check.py proof.lean
+python skills/cli/lean_check.py proof.lean --timeout-seconds 300
+```
+
+## Notes
+
+- No `--environment` flag needed — automatically detects the Lean project root by finding `lean-toolchain`.
+- Runs `lake env lean` locally, so the project must have been built at least once (`lake build` or `lake exe cache get`).
+- No API key required.
+- Multiple checks can run in parallel (each is an independent process).