Repo cleanup: dead code out, test isolation fix, real README

- Remove src/lmm_client.py and src/proof_agent.py — MVP-era relics with
zero production importers since the provider routing moved into
rag_chain. Their tests go with them (including the proof_agent
default-model regression test, obsolete with the module deleted).

- Fix sys.modules pollution in test_manual_bug_fixes.py: it installed
MagicMocks at lean_verifier/retriever/rag_chain at import time and
never restored them, poisoning every test module imported later
during discovery (alphabetical order put 6 files after it). Mocks are
now installed only around the langgraph_agent import and restored in
a finally block; the mock-built langgraph_agent is evicted too.

- Replace the 344-line MVP design doc README (Ollama-era, described the
since-removed reranker) with an accurate project README: architecture
diagram, RAG details with real numbers, model matrix, local-run
quickstart, honest small-sample benchmark table, project layout, CI
notes. HF Spaces frontmatter unchanged.

- Track scripts/setup_lean.py — the one-time Lean+Mathlib warmup
utility referenced by the README quickstart.

- UI: rebalance the controls bar (optional Claude key field no longer
gets equal width with the model picker; clearer label).

103 tests pass, ruff clean.

README.md

@@ -8,337 +8,98 @@ app_file: app.py
 pinned: false
 ---
 
-## Brief Non-Technical MVP: AI Lean 4 Proof Assistant
+# Lean 4 Proof Assistant
 
-### Project goal
+An AI agent that completes formal mathematical proofs in **Lean 4**. Paste a theorem containing `sorry`, and the agent retrieves relevant Mathlib lemmas, drafts a proof with an LLM, and verifies it with the Lean compiler — retrying with error feedback until the proof checks or retries run out.
 
-Build an AI assistant that helps users write correct **Lean 4 mathematical proofs**.
+The core guarantee: **only Lean decides correctness.** Every accepted proof is formally verified by the Lean 4 REPL, so the system structurally cannot return a hallucinated proof.
 
-The user provides a theorem. The system searches Lean’s Mathlib library, finds useful related theorems, asks an AI model to write a proof, checks the proof using Lean, and automatically retries if the proof fails.
+**[Try it on Hugging Face Spaces →](https://huggingface.co/spaces/Ray5th/lean4-helper)**
 
-The key idea is:
+## How it works
 
-```text
-AI suggests the proof.
-Lean verifies the proof.
-Only Lean decides if the answer is correct.
+```mermaid
+flowchart LR
+    UI[Gradio UI] --> V[Verify<br/>Lean 4 REPL]
+    V -->|errors / goals| R[Retrieve<br/>LeanDojo ByT5 + FAISS]
+    R -->|top-5 premises| G[Generate<br/>LLM]
+    G -->|candidate proof| V
+    V -->|no goals left| OK([Verified proof])
 ```
 
----
-
-## MVP flow
-
-```text
-User enters theorem
-        ↓
-Lean tooling reads the theorem and current proof goal
-        ↓
-System retrieves useful Mathlib lemmas
-        ↓
-System reranks the lemmas and keeps the best ones
-        ↓
-LangChain organizes the prompt and retrieval flow
-        ↓
-Local LLM generates a Lean proof
-        ↓
-Lean checks the proof
-        ↓
-If correct → return final proof
-If wrong → send Lean error back to the AI and retry
-```
-
----
-
-## Simple explanation
-
-This project is like an **AI coding assistant for mathematical proofs**.
-
-But unlike a normal chatbot, it does not just guess. It uses Lean itself to check whether the proof is truly valid.
-
-The assistant works in three stages:
-
-```text
-1. Search
-Find useful existing Mathlib theorems.
-
-2. Generate
-Ask the AI model to write a proof using those theorems.
-
-3. Verify
-Run the proof through Lean and retry if Lean finds an error.
-```
-
----
-
-## Main MVP components
-
-### 1. Lean tooling
-
-Use **LeanInteract** to connect Python with Lean 4.
-
-LeanInteract lets Python interact with Lean through the Lean REPL, which means your program can send Lean code, inspect proof goals, and receive Lean feedback programmatically. ([GitHub][1])
-
-In simple terms:
-
-```text
-LeanInteract lets the AI system talk to Lean.
-```
-
-Instead of only seeing an error like:
-
-```text
-type mismatch
-```
-
-the system can see more useful information like:
+A LangGraph state machine drives a `verify → retrieve → generate` loop:
 
-```text
-Current goal:
-n : Nat
-⊢ n = n
-```
+1. **Verify** — the file is checked by the Lean 4 REPL (via [lean-interact](https://github.com/augustepoiroux/LeanInteract)) with Mathlib available. Open goals and errors are extracted.
+2. **Retrieve** — the current proof state (goals only, canonical `h : T ⊢ goal` form) is embedded with **LeanDojo's pretrained ByT5 premise retriever** and searched against a FAISS index of **180,973 Mathlib premises**. The index is IVFPQ-compressed, so 1.06 GB of raw embeddings ship as a 17 MB file via Git LFS.
+3. **Generate** — retrieved premises are passed to the LLM as *optional hints* (RAFT-style distractor-aware framing), and the model must cite which lemmas it actually used (`-- used: Nat.add_comm`). The generated proof goes back to step 1.
 
-That makes the retry much smarter.
+Lean error messages feed the LLM prompt on retry but are kept out of the retrieval query — the encoder was trained on clean proof states, and error text degrades the embedding.
 
----
+## Supported models
 
-### 2. Retrieve Mathlib lemmas
+| Provider | Models | Notes |
+|---|---|---|
+| **Groq** (default) | `openai/gpt-oss-120b`, `openai/gpt-oss-20b`, `qwen/qwen3-32b`, `meta-llama/llama-4-scout-17b-16e-instruct` | Needs `GROQ_API_KEY` (Space secret / env var) |
+| **Anthropic** | Claude Opus 4.7 · Sonnet 4.6 · Haiku 4.5 | Bring-your-own key in the UI; never stored |
+| **Claude CLI** | `claude-cli-opus` etc. | Local `claude -p` subprocess — bills a Claude Pro subscription instead of API credits |
 
-The system searches Mathlib for useful theorems.
+## Running locally
 
-For example, if the theorem is about even numbers, the retriever may find lemmas related to:
-
-```text
-Even
-Odd
-Nat.even_or_odd
-parity
-multiplication
-powers
+```bash
+git clone https://github.com/ray5th/lean4-helper && cd lean4-helper
+pip install -r requirements.txt
+git lfs pull                          # fetch the FAISS index
+python scripts/setup_lean.py          # one-time Lean + Mathlib warmup (slow first run)
+export GROQ_API_KEY=...               # or use a Claude key / CLI in the UI
+python app.py                         # Gradio UI on :7860
 ```
 
-This is the “retrieve” part.
-
-Use:
+CLI instead of UI:
 
-```text
-FAISS for fast semantic search
-BM25 / keyword search for exact Lean names
+```bash
+python scripts/run_agent.py problems/simple_add.lean --model openai/gpt-oss-120b
 ```
 
-FAISS is useful for quickly finding similar text from a large collection of embedded documents, while keyword search helps when exact theorem names matter.
+Benchmark on local problem files or MiniF2F:
 
----
-
-### 3. Rerank retrieved lemmas
-
-Retrieval alone is not enough.
-
-The system may retrieve 50 possible Mathlib lemmas, but many may be weak or irrelevant. So we add a **reranker**.
-
-The improved flow is:
-
-```text
-Retrieve top 50 lemmas
-        ↓
-Rerank them based on the current theorem and proof goal
-        ↓
-Keep the best 8–12 lemmas
-        ↓
-Send only those to the AI model
+```bash
+python scripts/benchmark.py --problems-dir problems --retries 3 --verbose
+python scripts/benchmark.py --subset 20 --model claude-cli-opus   # MiniF2F via HF datasets
 ```
 
-A Cross-Encoder reranker is useful here because it scores each query-document pair more carefully than the first-pass retriever. Sentence Transformers describes this as a common retrieve-and-rerank setup where fast retrieval finds candidates and the Cross-Encoder reranks them for better relevance. ([SentenceTransformers][2])
+## Benchmarks (small-sample, honest numbers)
 
-In simple terms:
+| Set | Result | Notes |
+|---|---|---|
+| 16 intro lecture problems (calc / linarith / ring) | 16/16 | 15 solved on first generation |
+| 6 harder problems (named-lemma, induction, divisibility) | 6/6 | retrieved-lemma citations fired on 4/6 |
+| MiniF2F sample (5 AMC/AIME problems) | 3/5 | competition-grade; n far too small to quote as a pass rate |
 
-```text
-Retrieve finds possible useful lemmas.
-Rerank chooses the best ones.
-```
+## Project structure
 
-This improves the quality of the context given to the AI.
-
----
-
-### 4. LangChain role
-
-Use **LangChain** for orchestration, not for proof correctness.
-
-LangChain can help organize:
-
-```text
-retrieval
-reranking
-prompt templates
-document formatting
-LLM calls
-retry history
 ```
-
-LangChain has retrieval utilities such as contextual compression, where retrieved documents can be filtered or shortened before sending them to the model. ([LangChain][3])
-
-But LangChain does **not** make Lean proofs correct by itself.
-
-The correctness still comes from:
-
-```text
-Lean compiler
-Lean proof state
-Mathlib retrieval quality
-LLM proof generation
-retry loop
+app.py                       Gradio UI (two-pane editor, model picker, logs)
+src/
+  langgraph_agent.py         verify→retrieve→generate state machine
+  lean_verifier.py           Lean 4 REPL wrapper (lean-interact)
+  retriever.py               FAISS retrieval over Mathlib premises
+  byt5_embedder.py           LeanDojo ByT5 encoder wrapper
+  rag_chain.py               prompts + LLM provider routing (Groq/Anthropic/CLI)
+  mathlib_corpus.py          Mathlib source → premise extraction
+scripts/
+  build_leandojo_index.py    build the IVFPQ FAISS index from LeanDojo embeddings
+  benchmark.py               pass@k benchmark (local files or MiniF2F)
+  run_agent.py               CLI entry point
+  setup_lean.py              one-time Lean + Mathlib warmup
+problems/                    sample .lean problems
+tests/                       ~110 unit/fuzz tests (mocked LLM + Lean)
 ```
 
-So the right positioning is:
-
-```text
-LangChain manages the workflow.
-Lean verifies the truth.
-```
-
----
-
-### 5. Local LLM first
-
-For the MVP, use a local model first.
-
-Example:
-
-```text
-Ollama + Qwen Coder
-```
-
-Why local first?
-
-```text
-No API cost
-Easy to test many times
-Good for debugging the pipeline
-Private and simple for development
-```
-
-Later, once the workflow works, replace the local model with Claude.
-
-The architecture stays the same.
-
----
-
-### 6. Lean verification and retry
-
-After the AI generates a proof, the system sends it to Lean.
-
-If Lean accepts the proof:
-
-```text
-Success → return proof
-```
-
-If Lean rejects the proof:
-
-```text
-Failure → capture Lean error → add error to prompt → retry
-```
-
-Example:
-
-```text
-Attempt 1:
-AI generates proof.
-Lean says: unknown theorem name.
-
-Attempt 2:
-AI sees the error and tries a different lemma.
-Lean says: type mismatch.
-
-Attempt 3:
-AI fixes the proof.
-Lean accepts it.
-```
-
-This is the most important part of the MVP.
-
----
-
-## Final MVP architecture
-
-```text
-User Theorem
-     │
-     ▼
-LeanInteract
-Get theorem goal and Lean feedback
-     │
-     ▼
-Hybrid Retrieval
-FAISS semantic search + keyword search
-     │
-     ▼
-Reranker
-Keep only the most useful Mathlib lemmas
-     │
-     ▼
-LangChain Prompt Flow
-Organize theorem, lemmas, history, and Lean errors
-     │
-     ▼
-Local LLM
-Generate Lean proof
-     │
-     ▼
-Lean Checker
-Verify proof
-     │
-     ├── Success → Return final proof
-     │
-     └── Failure → Retry with Lean error
-```
-
----
-
-## Libraries to use
-
-| Purpose                      | Library                                           |
-| ---------------------------- | ------------------------------------------------- |
-| Interact with Lean           | `LeanInteract`                                    |
-| Semantic retrieval           | `sentence-transformers`                           |
-| Vector search                | `faiss-cpu`                                       |
-| Keyword search               | `rank-bm25`                                       |
-| Reranking                    | `sentence-transformers` CrossEncoder or FlashRank |
-| Workflow orchestration       | `LangChain`                                       |
-| More advanced workflow graph | `LangGraph`                                       |
-| Local model                  | `Ollama`                                          |
-| Future stronger model        | Claude API                                        |
-
-LangGraph is useful later if you want the proof process to behave like a clear state machine: retrieve → generate → verify → retry → success/failure. LangGraph is designed for stateful agent workflows, which fits this kind of multi-step proof loop. ([Emergent Mind][4])
-
----
-
-## Non-technical value proposition
-
-This MVP creates an AI assistant that helps people write mathematically verified Lean proofs.
-
-It does not only generate text. It checks every answer with Lean, learns from errors, and keeps trying until it produces a valid proof.
-
-The project demonstrates:
-
-```text
-AI-assisted formal reasoning
-verified code generation
-search over mathematical knowledge
-automatic error correction
-LLM + compiler feedback loops
-```
-
----
-
-## One-line MVP summary
+## Testing & CI
 
-```text
-An AI-powered Lean 4 proof assistant that searches Mathlib, reranks useful lemmas, generates a proof with a local LLM, checks it using Lean tooling, and automatically retries using Lean errors until the proof is verified.
+```bash
+python -m unittest discover -s tests   # full suite, no API keys or Lean needed
+ruff check .
 ```
 
-[1]: https://github.com/augustepoiroux/LeanInteract?utm_source=chatgpt.com "LeanInteract: A Python Interface for Lean 4"
-[2]: https://sbert.net/examples/sentence_transformer/applications/retrieve_rerank/README.html?utm_source=chatgpt.com "Retrieve & Re-Rank Pipeline"
-[3]: https://www.langchain.com/blog/improving-document-retrieval-with-contextual-compression?utm_source=chatgpt.com "Improving Document Retrieval with Contextual Compression"
-[4]: https://www.emergentmind.com/topics/langgraph?utm_source=chatgpt.com "LangGraph: Modular LLM Agent Orchestration"
+GitHub Actions runs lint + tests on every push and auto-deploys to the Space on merge to `main` (when `HF_TOKEN` is configured).

app.py

@@ -621,10 +621,10 @@ with gr.Blocks(
             label="Max retries", scale=1,
         )
         anthropic_key_input = gr.Textbox(
-            label="Anthropic API key (Claude models only)",
-            placeholder="sk-ant-…",
+            label="Claude API key (optional)",
+            placeholder="sk-ant-… — only for Claude models",
             type="password",
-            scale=2,
+            scale=1,
         )
 
     # ─── Two editor panes ───────────────────────────────────────────

scripts/setup_lean.py

@@ -0,0 +1,35 @@
+#!/usr/bin/env python3
+import os
+import sys
+
+# Add src to Python path
+sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
+
+from lean_verifier import LeanEnvironment
+
+
+def main():
+    print("Setting up Lean Environment and pre-caching Mathlib...")
+    print("This might take a while if Mathlib has not been built yet.")
+
+    # Initialize the Lean environment with Mathlib
+    lean_env = LeanEnvironment(use_mathlib=True)
+
+    print("\nEnvironment initialized successfully!")
+
+    # Run a simple test
+    print("\nRunning a quick verification test...")
+    test_code = """
+import Mathlib
+
+example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 :=
+  sorry
+"""
+    result = lean_env.verify_proof(test_code)
+    print(f"Test Result: {result['status']}")
+    if result['status'] != 'success':
+        print(f"Errors: {result['errors']}")
+        print(f"Goals: {result['goals']}")
+
+if __name__ == "__main__":
+    main()

src/lmm_client.py

@@ -1,56 +0,0 @@
-from typing import List, Optional
-
-from groq import Groq
-
-
-class LMMClient:
-    """
-    Client for interacting with LLMs via Groq API.
-    """
-
-    def __init__(self, model_name: str = "llama-3.3-70b-versatile"):
-        self.model_name = model_name
-        self._client = Groq()
-
-    def chat(self, prompt: str, system_prompt: Optional[str] = None) -> str:
-        messages = []
-        if system_prompt:
-            messages.append({"role": "system", "content": system_prompt})
-        messages.append({"role": "user", "content": prompt})
-
-        response = self._client.chat.completions.create(
-            model=self.model_name,
-            messages=messages,
-            max_tokens=1024,
-        )
-        # Defensive: Groq can return empty `choices` on content filter / quota
-        # issues — accessing [0] would IndexError and kill the agent.
-        choices = getattr(response, "choices", None) or []
-        if not choices:
-            return ""
-        message = getattr(choices[0], "message", None)
-        content = getattr(message, "content", None) if message else None
-        return content or ""
-
-    def generate_proof_steps(self, lean_code: str, goals: List[str], errors: List[str]) -> str:
-        system_prompt = (
-            "You are an expert Lean 4 proof assistant. "
-            "Your goal is to complete the proof by replacing 'sorry' with valid Lean 4 code. "
-            "Use Mathlib theorems where appropriate. "
-            "Respond ONLY with the corrected Lean code block."
-        )
-        prompt = f"""
-Current Lean Code:
-```lean
-{lean_code}
-```
-
-Current Proof Goals:
-{chr(10).join(goals)}
-
-Lean Errors:
-{chr(10).join(errors)}
-
-Please provide the corrected Lean code. Focus on solving the current goals and fixing the errors.
-"""
-        return self.chat(prompt, system_prompt)

src/proof_agent.py

@@ -1,11 +0,0 @@
-from langgraph_agent import LangGraphAgent
-
-
-class ProofAgent:
-    """Thin compatibility wrapper around LangGraphAgent."""
-
-    def __init__(self, model_name: str = "llama-3.3-70b-versatile", max_retries: int = 5):
-        self._agent = LangGraphAgent(model_name=model_name, max_retries=max_retries)
-
-    def solve_file(self, file_path: str) -> bool:
-        return self._agent.solve_file(file_path)

tests/test_manual_bug_fixes.py

@@ -21,18 +21,30 @@ sys.path.insert(0, "src")
 sys.modules.pop("langgraph_agent", None)
 
 # `langgraph_agent` imports lean_verifier + retriever + rag_chain which each
-# pull in heavyweight ML libs. Mock those three modules directly so we can
-# import the helpers without installing langchain-groq / lean-interact.
-for _mod in ("lean_verifier", "retriever", "rag_chain"):
+# pull in heavyweight ML libs. Mock those three modules just long enough to
+# import the pure helpers, then RESTORE sys.modules — leaving MagicMocks
+# behind poisons every test module imported after this one during discovery.
+_DEPS = ("lean_verifier", "retriever", "rag_chain")
+_saved = {m: sys.modules.get(m) for m in _DEPS}
+for _mod in _DEPS:
     sys.modules[_mod] = mock.MagicMock()
-
-import langgraph_agent
-
-importlib.reload(langgraph_agent)  # ensure regex/keyword changes are picked up
-_count_theorem_blocks = langgraph_agent._count_theorem_blocks
-_extract_lean_code = langgraph_agent._extract_lean_code
-_read_file = langgraph_agent._read_file
-_write_file = langgraph_agent._write_file
+try:
+    import langgraph_agent
+
+    importlib.reload(langgraph_agent)  # ensure regex/keyword changes are picked up
+    _count_theorem_blocks = langgraph_agent._count_theorem_blocks
+    _extract_lean_code = langgraph_agent._extract_lean_code
+    _read_file = langgraph_agent._read_file
+    _write_file = langgraph_agent._write_file
+finally:
+    for _mod, _orig in _saved.items():
+        if _orig is not None:
+            sys.modules[_mod] = _orig
+        else:
+            sys.modules.pop(_mod, None)
+    # This langgraph_agent was built against mocks — evict it so later
+    # importers get a real one.
+    sys.modules.pop("langgraph_agent", None)
 
 
 class TestCountTheoremBlocksKeywordFix(unittest.TestCase):
@@ -132,25 +144,8 @@ class TestUtf8FileIO(unittest.TestCase):
             os.unlink(path)
 
 
-class TestProofAgentDefaultModel(unittest.TestCase):
-    """
-    `ProofAgent` used to default to `qwen3-vl:4b` (an Ollama model name) after
-    the Groq migration, which would fail at runtime. Now defaults to a real
-    Groq model.
-    """
-
-    def test_default_model_is_not_a_stale_ollama_name(self):
-        # Inspect the function default directly — avoids needing a working
-        # LangGraphAgent mock chain.
-        import inspect
-
-        import proof_agent
-
-        sig = inspect.signature(proof_agent.ProofAgent.__init__)
-        default = sig.parameters["model_name"].default
-        self.assertNotIn("qwen", default.lower())
-        self.assertNotIn(":", default,
-                         "Default looks like an Ollama 'name:tag' format")
+# (A TestProofAgentDefaultModel regression test lived here until the unused
+# `proof_agent` wrapper module it covered was deleted.)
 
 
 if __name__ == "__main__":

tests/test_proof_agent.py

@@ -1,147 +0,0 @@
-import os
-import sys
-import unittest
-from unittest.mock import MagicMock, patch
-
-# Add src to Python path
-sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), '..', 'src')))
-
-# Mock langgraph_agent.LangGraphAgent before importing proof_agent (so its
-# top-level `from langgraph_agent import LangGraphAgent` doesn't pull in the
-# heavy real module). Restore sys.modules afterward so this file doesn't
-# poison the langgraph_agent import for other test files in the same run.
-_orig_langgraph_agent = sys.modules.get('langgraph_agent')
-sys.modules['langgraph_agent'] = MagicMock()
-
-from proof_agent import ProofAgent
-
-if _orig_langgraph_agent is not None:
-    sys.modules['langgraph_agent'] = _orig_langgraph_agent
-else:
-    del sys.modules['langgraph_agent']
-
-
-class TestProofAgentConstructor(unittest.TestCase):
-    def test_default_args_constructs_langgraph_agent_with_defaults(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            ProofAgent()
-            MockLangGraphAgent.assert_called_once_with(
-                model_name="llama-3.3-70b-versatile",
-                max_retries=5,
-            )
-
-    def test_custom_model_name_forwarded(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            ProofAgent(model_name="custom-model:7b")
-            MockLangGraphAgent.assert_called_once_with(
-                model_name="custom-model:7b",
-                max_retries=5,
-            )
-
-    def test_custom_max_retries_forwarded(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            ProofAgent(max_retries=10)
-            MockLangGraphAgent.assert_called_once_with(
-                model_name="llama-3.3-70b-versatile",
-                max_retries=10,
-            )
-
-    def test_all_custom_args_forwarded(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            ProofAgent(model_name="other-model:13b", max_retries=3)
-            MockLangGraphAgent.assert_called_once_with(
-                model_name="other-model:13b",
-                max_retries=3,
-            )
-
-    def test_underlying_agent_stored_on_instance(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            MockLangGraphAgent.return_value = mock_instance
-            agent = ProofAgent()
-            self.assertIs(agent._agent, mock_instance)
-
-
-class TestProofAgentSolveFile(unittest.TestCase):
-    def test_solve_file_delegates_returning_true(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            mock_instance.solve_file.return_value = True
-            MockLangGraphAgent.return_value = mock_instance
-
-            agent = ProofAgent()
-            result = agent.solve_file("path/to/file.lean")
-
-            self.assertTrue(result)
-            mock_instance.solve_file.assert_called_once_with("path/to/file.lean")
-
-    def test_solve_file_delegates_returning_false(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            mock_instance.solve_file.return_value = False
-            MockLangGraphAgent.return_value = mock_instance
-
-            agent = ProofAgent()
-            result = agent.solve_file("path/to/file.lean")
-
-            self.assertFalse(result)
-            mock_instance.solve_file.assert_called_once_with("path/to/file.lean")
-
-    def test_solve_file_path_is_forwarded_exactly(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            mock_instance.solve_file.return_value = True
-            MockLangGraphAgent.return_value = mock_instance
-
-            agent = ProofAgent()
-            agent.solve_file("/absolute/path/proof.lean")
-            mock_instance.solve_file.assert_called_once_with("/absolute/path/proof.lean")
-
-    def test_solve_file_propagates_exception(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            mock_instance.solve_file.side_effect = RuntimeError("boom")
-            MockLangGraphAgent.return_value = mock_instance
-
-            agent = ProofAgent()
-            with self.assertRaises(RuntimeError):
-                agent.solve_file("foo.lean")
-
-
-class TestProofAgentNoExtraState(unittest.TestCase):
-    def test_no_unexpected_public_methods(self):
-        with patch('proof_agent.LangGraphAgent'):
-            agent = ProofAgent()
-            public_attrs = {a for a in dir(agent) if not a.startswith('_')}
-            # The wrapper should only expose solve_file
-            self.assertEqual(public_attrs, {"solve_file"})
-
-    def test_solve_file_does_not_mutate_wrapper_state(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            mock_instance.solve_file.return_value = True
-            MockLangGraphAgent.return_value = mock_instance
-
-            agent = ProofAgent()
-            before = set(vars(agent).keys())
-            agent.solve_file("a.lean")
-            after = set(vars(agent).keys())
-            self.assertEqual(before, after)
-
-    def test_multiple_calls_use_same_underlying_agent(self):
-        with patch('proof_agent.LangGraphAgent') as MockLangGraphAgent:
-            mock_instance = MagicMock()
-            mock_instance.solve_file.return_value = True
-            MockLangGraphAgent.return_value = mock_instance
-
-            agent = ProofAgent()
-            agent.solve_file("a.lean")
-            agent.solve_file("b.lean")
-
-            # Only one underlying agent constructed
-            self.assertEqual(MockLangGraphAgent.call_count, 1)
-            self.assertEqual(mock_instance.solve_file.call_count, 2)
-
-
-if __name__ == '__main__':
-    unittest.main()