feat(lean): optimize all Lean tools via Pantograph and LSP incremental elaboration

.worktreeinclude

@@ -1,5 +1,9 @@
-# Files to copy into git worktrees (gitignored files that sessions need)
+# Files to copy/link into git worktrees (gitignored files that sessions need)
 .env
 .env.local
 .openproof/
 CLAUDE.md
+
+# Lean build artifacts (symlink manually if not auto-linked: too large to copy)
+lean/.lake
+vendor

crates/openproof-cli/src/autonomous_headless.rs

@@ -451,6 +451,7 @@ pub async fn run_autonomous(
                         &verify_session,
                         verify_session.proof.nodes.first().unwrap(),
                         persistent_path.as_deref(),
+                        None,
                     )
                 })
                 .await

crates/openproof-cli/src/system_prompt.rs

@@ -82,7 +82,7 @@ fn tools_and_workflow_section() -> &'static str {
         "`file_patch(path, patch)` (primary edit tool), `workspace_ls()`\n",
         "**Lean:** `lean_verify(file)`, `lean_goals(file)`, ",
         "`lean_screen_tactics(file, line, tactics)` (batch-test tactics without modifying file), ",
-        "`lean_check(expr)`, `lean_search_tactic(tactic, file, line)`\n",
+        "`lean_check(exprs)` (batch type lookup -- pass all names in one call), `lean_search_tactic(tactic, file, line)`\n",
         "**Research:** `corpus_search(query)` (190K+ Mathlib declarations), ",
         "`shell_run(command)` (sage, python3), web search\n\n",
 
@@ -97,6 +97,7 @@ fn tools_and_workflow_section() -> &'static str {
 
         "## Avoid\n",
         "- Repeated corpus_search without writing code\n",
+        "- Multiple separate lean_check calls (batch into one call with `exprs` array)\n",
         "- lean_check guessing random names (use exact?/apply? instead)\n",
         "- Explaining plans instead of executing them\n",
         "- shell_run for filesystem exploration (use workspace_ls)\n",

crates/openproof-cli/src/turn_handling.rs

@@ -710,6 +710,7 @@ pub fn start_branch_verification(
                     })
                     .unwrap_or(&verification_clone.proof.nodes[0]),
                 scratch.as_deref(),
+                None,
             )
         })
         .await

crates/openproof-core/src/apply_content.rs

@@ -473,7 +473,7 @@ impl AppState {
             "lean_verify" => "verifying proof...".to_string(),
             "lean_goals" => "extracting goals...".to_string(),
             "lean_screen_tactics" => "testing tactics...".to_string(),
-            "lean_check" => "checking type...".to_string(),
+            "lean_check" => "checking types...".to_string(),
             "lean_search_tactic" => "searching for tactic...".to_string(),
             "corpus_search" => "searching corpus...".to_string(),
             "file_write" => "writing file...".to_string(),

crates/openproof-lean/src/lib.rs

@@ -19,4 +19,5 @@ pub use render::render_node_scratch;
 pub use tools::find_sorry_positions;
 pub use verify::{
     detect_lean_health, verify_active_node, verify_node, verify_node_at, verify_scratch_content,
+    verify_scratch_via_lsp,
 };

crates/openproof-lean/src/tools.rs

@@ -76,6 +76,24 @@ fn tool_lean_verify(args: &Value, ctx: &ToolContext) -> Result<ToolOutput> {
 
     let full_content = build_compilation_unit(&content, ctx);
 
+    // Fast path: LSP incremental verification (~200ms-2s vs 5-30s).
+    if let Some(ref lsp) = ctx.lsp_mcp {
+        if let Ok(result) =
+            crate::verify::verify_scratch_via_lsp(lsp, ctx.project_dir, full_content.clone())
+        {
+            let output = if result.ok {
+                result.stdout.clone()
+            } else {
+                result.stderr.clone()
+            };
+            return Ok(ToolOutput {
+                success: result.ok,
+                content: truncate_output(&output),
+            });
+        }
+    }
+
+    // Fallback: full Lean compiler invocation.
     let scratch_path = write_temp_file(&full_content)?;
     let (ok, output) = run_lean_command(ctx.project_dir, &scratch_path)?;
     let has_sorry = output.contains("declaration uses 'sorry'");
@@ -418,12 +436,55 @@ pub fn find_sorry_positions(content: &str) -> Vec<(usize, usize)> {
 }
 
 fn tool_lean_check(args: &Value, ctx: &ToolContext) -> Result<ToolOutput> {
-    let expr = args
-        .get("expr")
-        .and_then(Value::as_str)
-        .context("missing 'expr' argument")?;
+    // Collect expressions from either `expr` (single) or `exprs` (batch).
+    let mut exprs: Vec<String> = Vec::new();
+    if let Some(arr) = args.get("exprs").and_then(Value::as_array) {
+        for v in arr {
+            if let Some(s) = v.as_str() {
+                exprs.push(s.to_string());
+            }
+        }
+    }
+    if let Some(s) = args.get("expr").and_then(Value::as_str) {
+        if !exprs.iter().any(|e| e == s) {
+            exprs.push(s.to_string());
+        }
+    }
+    if exprs.is_empty() {
+        anyhow::bail!("missing 'expr' or 'exprs' argument");
+    }
+
+    // Fast path: Pantograph env.inspect (milliseconds per expression).
+    if let Some(ref prover) = ctx.prover {
+        if let Ok(mut sp) = prover.lock() {
+            if sp.is_alive() {
+                let mut parts = Vec::new();
+                let mut all_ok = true;
+                for expr in &exprs {
+                    match sp.pantograph.inspect(expr) {
+                        Ok(Some(ty)) => parts.push(format!("{expr} : {ty}")),
+                        Ok(None) => {
+                            all_ok = false;
+                            parts.push(format!("{expr} : unknown (not found in environment)"));
+                        }
+                        Err(_) => {
+                            all_ok = false;
+                            parts.push(format!("{expr} : error (Pantograph inspect failed)"));
+                        }
+                    }
+                }
+                return Ok(ToolOutput {
+                    success: all_ok,
+                    content: truncate_output(&parts.join("\n")),
+                });
+            }
+        }
+    }
+
+    // Fallback: batch all expressions into a single Lean invocation.
     let imports = build_import_block(ctx.imports);
-    let content = format!("{imports}\n#check {expr}\n");
+    let checks: String = exprs.iter().map(|e| format!("#check {e}\n")).collect();
+    let content = format!("{imports}\n{checks}");
     let scratch_path = write_temp_file(&content)?;
     let (ok, output) = run_lean_command(ctx.project_dir, &scratch_path)?;
     Ok(ToolOutput {
@@ -437,9 +498,29 @@ fn tool_lean_eval_fn(args: &Value, ctx: &ToolContext) -> Result<ToolOutput> {
         .get("expr")
         .and_then(Value::as_str)
         .context("missing 'expr' argument")?;
+
     let imports = build_import_block(ctx.imports);
-    // #eval runs a Lean expression and prints the result
     let content = format!("{imports}\n#eval ({expr})\n");
+
+    // Fast path: LSP incremental verification.
+    if let Some(ref lsp) = ctx.lsp_mcp {
+        if let Ok(result) =
+            crate::verify::verify_scratch_via_lsp(lsp, ctx.project_dir, content.clone())
+        {
+            // #eval output appears as info-level diagnostics.
+            let output = if !result.stdout.is_empty() {
+                result.stdout
+            } else {
+                result.stderr
+            };
+            return Ok(ToolOutput {
+                success: !output.is_empty(),
+                content: truncate_output(&output),
+            });
+        }
+    }
+
+    // Fallback: full Lean compiler invocation.
     let scratch_path = write_temp_file(&content)?;
     let (ok, output) = run_lean_command(ctx.project_dir, &scratch_path)?;
     Ok(ToolOutput {
@@ -477,10 +558,49 @@ fn tool_lean_search_tactic(args: &Value, ctx: &ToolContext) -> Result<ToolOutput
         format!("{imports}\n{modified}")
     };
 
+    // Fast path: LSP incremental verification. "Try this:" appears in diagnostics.
+    if let Some(ref lsp) = ctx.lsp_mcp {
+        if let Ok(result) =
+            crate::verify::verify_scratch_via_lsp(lsp, ctx.project_dir, full_content.clone())
+        {
+            let output = format!("{}\n{}", result.stdout, result.stderr);
+            let suggestions = extract_search_suggestions(&output);
+            return if suggestions.is_empty() {
+                Ok(ToolOutput {
+                    success: false,
+                    content: truncate_output(&format!(
+                        "No suggestions found.\n\nFull output:\n{output}"
+                    )),
+                })
+            } else {
+                Ok(ToolOutput {
+                    success: true,
+                    content: truncate_output(&suggestions.join("\n")),
+                })
+            };
+        }
+    }
+
+    // Fallback: full Lean compiler invocation.
     let scratch_path = write_temp_file(&full_content)?;
     let (_ok, output) = run_lean_command(ctx.project_dir, &scratch_path)?;
 
-    // Extract just the suggestions from the output.
+    let suggestions = extract_search_suggestions(&output);
+    if suggestions.is_empty() {
+        Ok(ToolOutput {
+            success: false,
+            content: truncate_output(&format!("No suggestions found.\n\nFull output:\n{output}")),
+        })
+    } else {
+        Ok(ToolOutput {
+            success: true,
+            content: truncate_output(&suggestions.join("\n")),
+        })
+    }
+}
+
+/// Extract "Try this:" suggestions from Lean compiler or LSP diagnostic output.
+fn extract_search_suggestions(output: &str) -> Vec<String> {
     let mut suggestions = Vec::new();
     for line in output.lines() {
         let trimmed = line.trim();
@@ -494,19 +614,15 @@ fn tool_lean_search_tactic(args: &Value, ctx: &ToolContext) -> Result<ToolOutput
                 suggestions.push(trimmed[pos + 1..].trim().to_string());
             }
         }
+        // LSP diagnostics may include "Try this:" inside the message field
+        if let Some(idx) = trimmed.find("Try this:") {
+            let rest = trimmed[idx + 9..].trim();
+            if !rest.is_empty() && !suggestions.iter().any(|s| s == rest) {
+                suggestions.push(rest.to_string());
+            }
+        }
     }
-
-    if suggestions.is_empty() {
-        Ok(ToolOutput {
-            success: false,
-            content: truncate_output(&format!("No suggestions found.\n\nFull output:\n{output}")),
-        })
-    } else {
-        Ok(ToolOutput {
-            success: true,
-            content: truncate_output(&suggestions.join("\n")),
-        })
-    }
+    suggestions
 }
 
 fn tool_file_read(args: &Value, ctx: &ToolContext) -> Result<ToolOutput> {

crates/openproof-lean/src/verify.rs

@@ -6,7 +6,9 @@ use openproof_protocol::{LeanHealth, LeanVerificationSummary, ProofNode, Session
 use std::fs;
 use std::path::{Path, PathBuf};
 use std::process::Command;
+use std::sync::Mutex;
 
+use crate::lsp_mcp::LeanLspMcp;
 use crate::render::render_node_scratch;
 
 pub fn detect_lean_health(project_dir: &Path) -> Result<LeanHealth> {
@@ -70,16 +72,18 @@ pub fn verify_node(
     session: &SessionSnapshot,
     node: &ProofNode,
 ) -> Result<LeanVerificationSummary> {
-    verify_node_at(project_dir, session, node, None)
+    verify_node_at(project_dir, session, node, None, None)
 }
 
 /// Verify a node, optionally writing to a persistent scratch path.
 /// If `persistent_path` is Some, writes to that path instead of a temp file.
+/// If `lsp` is Some, tries the fast LSP path first.
 pub fn verify_node_at(
     project_dir: &Path,
     session: &SessionSnapshot,
     node: &ProofNode,
     persistent_path: Option<&Path>,
+    lsp: Option<&Mutex<LeanLspMcp>>,
 ) -> Result<LeanVerificationSummary> {
     if node.content.trim().is_empty() {
         return Ok(failed_result(
@@ -95,6 +99,15 @@ pub fn verify_node_at(
     }
 
     let rendered_scratch = render_node_scratch(session, node);
+
+    // Fast path: LSP incremental verification.
+    if let Some(lsp) = lsp {
+        if let Ok(result) = verify_scratch_via_lsp(lsp, project_dir, rendered_scratch.clone()) {
+            return Ok(result);
+        }
+    }
+
+    // Fallback: full Lean compiler invocation.
     let scratch_path = if let Some(path) = persistent_path {
         if let Some(parent) = path.parent() {
             fs::create_dir_all(parent)?;
@@ -143,6 +156,78 @@ pub fn verify_scratch_content(
     verify_scratch(project_dir, rendered, scratch_path)
 }
 
+/// Verify via the LSP server (incremental elaboration, much faster after first call).
+///
+/// Writes `rendered_scratch` to `project_dir/Scratch.lean` and calls
+/// `LeanLspMcp.get_diagnostics()`. The LSP server keeps Mathlib loaded,
+/// so subsequent calls only re-elaborate the changed portions.
+pub fn verify_scratch_via_lsp(
+    lsp: &Mutex<LeanLspMcp>,
+    project_dir: &Path,
+    rendered_scratch: String,
+) -> Result<LeanVerificationSummary> {
+    let project_dir = project_dir
+        .canonicalize()
+        .unwrap_or_else(|_| project_dir.to_path_buf());
+    let scratch_path = project_dir.join("Scratch.lean");
+    fs::write(&scratch_path, &rendered_scratch)
+        .with_context(|| format!("writing {}", scratch_path.display()))?;
+
+    let diagnostics = {
+        let mut client = lsp.lock().map_err(|e| anyhow::anyhow!("LSP lock: {e}"))?;
+        if !client.is_alive() {
+            anyhow::bail!("LSP server is not alive");
+        }
+        client.get_diagnostics(&scratch_path)?
+    };
+
+    let mut errors = Vec::new();
+    let mut warnings = Vec::new();
+    let mut infos = Vec::new();
+    for item in &diagnostics.items {
+        let line = format!("{}:{}: {}", item.line, item.column, item.message);
+        match item.severity.as_str() {
+            "error" => errors.push(line),
+            "warning" => warnings.push(line),
+            _ => infos.push(line),
+        }
+    }
+
+    let has_sorry = diagnostics.items.iter().any(|d| {
+        let msg = d.message.to_ascii_lowercase();
+        msg.contains("uses 'sorry'")
+            || msg.contains("uses `sorry`")
+            || msg.contains("uses sorry")
+            || msg.contains("has sorry")
+    });
+
+    let stderr = if !errors.is_empty() || !warnings.is_empty() {
+        [errors, warnings].concat().join("\n")
+    } else {
+        String::new()
+    };
+
+    Ok(LeanVerificationSummary {
+        ok: diagnostics.success && !has_sorry,
+        code: Some(if diagnostics.success && !has_sorry {
+            0
+        } else {
+            1
+        }),
+        stdout: infos.join("\n"),
+        stderr,
+        error: if has_sorry {
+            Some("sorry-placeholder".to_string())
+        } else {
+            None
+        },
+        checked_at: Utc::now().to_rfc3339(),
+        project_dir: project_dir.display().to_string(),
+        scratch_path: scratch_path.display().to_string(),
+        rendered_scratch,
+    })
+}
+
 pub(crate) fn verify_scratch(
     project_dir: &Path,
     rendered_scratch: String,