substitute axle check to diagnostic with server

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

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

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

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 |
 

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,18 +173,18 @@ 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)
 
 ### 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)
 

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
 

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

prompts/docs/technique/WORKFLOW_DIAGRAM.md

@@ -143,15 +143,15 @@ 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!       │   │
 │  │  -/                                                        │   │
 │  └──────────────────────────────────────────────────────────┘   │
 │                            │                                     │
 │                            ▼                                     │
 │  ┌──────────────────────────────────────────────────────────┐   │
 │  │  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                                             │