diff --git a/.worktreeinclude b/.worktreeinclude
index 1290842..8b791ee 100644
--- a/.worktreeinclude
+++ b/.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
diff --git a/crates/openproof-cli/src/autonomous_headless.rs b/crates/openproof-cli/src/autonomous_headless.rs
index beb9e4c..4cdbf78 100644
--- a/crates/openproof-cli/src/autonomous_headless.rs
+++ b/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
diff --git a/crates/openproof-cli/src/system_prompt.rs b/crates/openproof-cli/src/system_prompt.rs
index 45985aa..9999d45 100644
--- a/crates/openproof-cli/src/system_prompt.rs
+++ b/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",
diff --git a/crates/openproof-cli/src/turn_handling.rs b/crates/openproof-cli/src/turn_handling.rs
index 7b010b1..265764c 100644
--- a/crates/openproof-cli/src/turn_handling.rs
+++ b/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
diff --git a/crates/openproof-core/src/apply_content.rs b/crates/openproof-core/src/apply_content.rs
index 67f004b..a127e1a 100644
--- a/crates/openproof-core/src/apply_content.rs
+++ b/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(),
diff --git a/crates/openproof-lean/src/lib.rs b/crates/openproof-lean/src/lib.rs
index 60a5193..69bd99f 100644
--- a/crates/openproof-lean/src/lib.rs
+++ b/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,
 };
diff --git a/crates/openproof-lean/src/tools.rs b/crates/openproof-lean/src/tools.rs
index d3ed129..9f815f9 100644
--- a/crates/openproof-lean/src/tools.rs
+++ b/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> {
diff --git a/crates/openproof-lean/src/verify.rs b/crates/openproof-lean/src/verify.rs
index 3301c69..2f44347 100644
--- a/crates/openproof-lean/src/verify.rs
+++ b/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,
diff --git a/crates/openproof-lean/tests/lean_check_test.rs b/crates/openproof-lean/tests/lean_check_test.rs
new file mode 100644
index 0000000..3567374
--- /dev/null
+++ b/crates/openproof-lean/tests/lean_check_test.rs
@@ -0,0 +1,359 @@
+//! Integration tests for Pantograph fast paths and LSP verification.
+//!
+//! Requires Pantograph/lean-lsp-mcp and Lean with Mathlib.
+//! Tests marked #[ignore] need external tooling.
+
+use openproof_lean::lsp_mcp::LeanLspMcp;
+use openproof_lean::proof_tree::SessionProver;
+use openproof_lean::tools::{execute_tool, ToolContext};
+use openproof_lean::verify_scratch_via_lsp;
+use std::path::Path;
+use std::sync::{Arc, Mutex};
+use std::time::Instant;
+
+fn lean_project_dir() -> &'static Path {
+    // cargo test runs from the package root (crates/openproof-lean/),
+    // but the lean project is at the workspace root's lean/ directory.
+    Path::new("../../lean")
+}
+
+fn spawn_prover() -> Option<Arc<Mutex<SessionProver>>> {
+    match SessionProver::spawn(lean_project_dir()) {
+        Ok(p) => Some(Arc::new(Mutex::new(p))),
+        Err(e) => {
+            eprintln!("SessionProver::spawn failed: {e:#}");
+            None
+        }
+    }
+}
+
+#[test]
+#[ignore] // Requires Pantograph + Mathlib (~18s startup)
+fn pantograph_single_expr() {
+    let prover = spawn_prover().expect("Pantograph not available");
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: Path::new("/tmp"),
+        imports: &[],
+        lsp_mcp: None,
+        prover: Some(prover),
+    };
+
+    let start = Instant::now();
+    let result = execute_tool("lean_check", r#"{"expr": "deriv_add"}"#, &ctx);
+    let elapsed = start.elapsed();
+
+    assert!(result.success, "lean_check failed: {}", result.content);
+    assert!(
+        result.content.contains("deriv_add"),
+        "output should contain expression name: {}",
+        result.content
+    );
+    assert!(
+        result.content.contains("deriv"),
+        "output should contain type info: {}",
+        result.content
+    );
+    // Pantograph path should be fast (< 2s, typically <100ms)
+    assert!(
+        elapsed.as_secs() < 2,
+        "Pantograph inspect took too long: {elapsed:?}"
+    );
+}
+
+#[test]
+#[ignore] // Requires Pantograph + Mathlib (~18s startup)
+fn pantograph_batch_exprs() {
+    let prover = spawn_prover().expect("Pantograph not available");
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: Path::new("/tmp"),
+        imports: &[],
+        lsp_mcp: None,
+        prover: Some(prover),
+    };
+
+    let start = Instant::now();
+    let result = execute_tool(
+        "lean_check",
+        r#"{"exprs": ["deriv_add", "Nat.Prime.dvd_mul", "List.map"]}"#,
+        &ctx,
+    );
+    let elapsed = start.elapsed();
+
+    assert!(
+        result.success,
+        "batch lean_check failed: {}",
+        result.content
+    );
+    assert!(
+        result.content.contains("deriv_add"),
+        "should contain deriv_add"
+    );
+    assert!(
+        result.content.contains("Nat.Prime.dvd_mul"),
+        "should contain Nat.Prime.dvd_mul"
+    );
+    assert!(
+        result.content.contains("List.map"),
+        "should contain List.map"
+    );
+    // 3 expressions via Pantograph should still be fast
+    assert!(
+        elapsed.as_secs() < 3,
+        "Batch Pantograph inspect took too long: {elapsed:?}"
+    );
+}
+
+#[test]
+#[ignore] // Requires Pantograph + Mathlib (~18s startup)
+fn pantograph_unknown_expr() {
+    let prover = spawn_prover().expect("Pantograph not available");
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: Path::new("/tmp"),
+        imports: &[],
+        lsp_mcp: None,
+        prover: Some(prover),
+    };
+
+    let result = execute_tool(
+        "lean_check",
+        r#"{"expr": "totally_fake_lemma_xyz_12345"}"#,
+        &ctx,
+    );
+    // Should not crash; returns success=false with descriptive message
+    assert!(!result.success);
+    assert!(
+        result.content.contains("not found") || result.content.contains("error"),
+        "should indicate not found: {}",
+        result.content
+    );
+}
+
+// --- LSP verify tests ---
+
+fn spawn_lsp() -> Option<Arc<Mutex<LeanLspMcp>>> {
+    match LeanLspMcp::spawn(lean_project_dir()) {
+        Ok(client) => Some(Arc::new(Mutex::new(client))),
+        Err(e) => {
+            eprintln!("LeanLspMcp::spawn failed: {e:#}");
+            None
+        }
+    }
+}
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_verify_valid_proof() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+
+    let content = "import Mathlib\n\ntheorem foo : 1 + 1 = 2 := by norm_num\n".to_string();
+
+    let start = Instant::now();
+    let result = verify_scratch_via_lsp(&lsp, lean_project_dir(), content).unwrap();
+    let elapsed = start.elapsed();
+
+    eprintln!(
+        "lsp_verify_valid_proof: ok={}, elapsed={elapsed:?}, stderr={}",
+        result.ok, result.stderr
+    );
+    assert!(result.ok, "valid proof should verify: {}", result.stderr);
+}
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_verify_sorry_detected() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+
+    let content = "import Mathlib\n\ntheorem bar : 1 + 1 = 2 := by sorry\n".to_string();
+
+    let result = verify_scratch_via_lsp(&lsp, lean_project_dir(), content).unwrap();
+
+    eprintln!(
+        "lsp_verify_sorry: ok={}, error={:?}, stderr={}",
+        result.ok, result.error, result.stderr
+    );
+    assert!(!result.ok, "sorry proof should fail: {}", result.stderr);
+    assert_eq!(
+        result.error.as_deref(),
+        Some("sorry-placeholder"),
+        "should detect sorry"
+    );
+}
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_verify_type_error() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+
+    let content = "import Mathlib\n\ntheorem baz : 1 + 1 = 3 := by norm_num\n".to_string();
+
+    let result = verify_scratch_via_lsp(&lsp, lean_project_dir(), content).unwrap();
+
+    eprintln!(
+        "lsp_verify_type_error: ok={}, stderr={}",
+        result.ok, result.stderr
+    );
+    assert!(!result.ok, "wrong proof should fail: {}", result.stderr);
+}
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_verify_incremental_is_fast() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+
+    // First call: cold start (may be slow)
+    let content1 = "import Mathlib\n\ntheorem warmup : 1 = 1 := rfl\n".to_string();
+    let _ = verify_scratch_via_lsp(&lsp, lean_project_dir(), content1);
+
+    // Second call: should be incremental (fast)
+    let content2 = "import Mathlib\n\ntheorem fast_check : 2 + 2 = 4 := by norm_num\n".to_string();
+    let start = Instant::now();
+    let result = verify_scratch_via_lsp(&lsp, lean_project_dir(), content2).unwrap();
+    let elapsed = start.elapsed();
+
+    eprintln!(
+        "lsp_verify_incremental: ok={}, elapsed={elapsed:?}",
+        result.ok
+    );
+    assert!(result.ok, "incremental verify failed: {}", result.stderr);
+    // Incremental should be much faster than cold (~2s vs ~18s)
+    assert!(
+        elapsed.as_secs() < 30,
+        "incremental verify too slow: {elapsed:?} (expected <30s)"
+    );
+}
+
+// --- lean_eval LSP tests ---
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_eval_computation() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+    let workspace = std::env::temp_dir().join("openproof-test-eval");
+    let _ = std::fs::create_dir_all(&workspace);
+
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: &workspace,
+        imports: &[],
+        lsp_mcp: Some(lsp),
+        prover: None,
+    };
+
+    let start = Instant::now();
+    let result = execute_tool("lean_eval", r#"{"expr": "Nat.gcd 12 8"}"#, &ctx);
+    let elapsed = start.elapsed();
+
+    eprintln!(
+        "lsp_eval: success={}, elapsed={elapsed:?}, content={}",
+        result.success, result.content
+    );
+    assert!(result.success, "eval should succeed: {}", result.content);
+    assert!(
+        result.content.contains("4"),
+        "gcd(12,8) should be 4: {}",
+        result.content
+    );
+}
+
+// --- lean_search_tactic LSP tests ---
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_search_tactic_exact() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+    let workspace = std::env::temp_dir().join("openproof-test-search");
+    let _ = std::fs::create_dir_all(&workspace);
+
+    // Write a file with a sorry that exact? can solve
+    let lean_content = "import Mathlib\n\ntheorem trivial_rfl : 1 = 1 := by sorry\n";
+    std::fs::write(workspace.join("Scratch.lean"), lean_content).unwrap();
+
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: &workspace,
+        imports: &[],
+        lsp_mcp: Some(lsp),
+        prover: None,
+    };
+
+    let start = Instant::now();
+    let result = execute_tool(
+        "lean_search_tactic",
+        r#"{"tactic": "exact?", "file": "Scratch.lean", "line": 3}"#,
+        &ctx,
+    );
+    let elapsed = start.elapsed();
+
+    eprintln!(
+        "lsp_search_tactic: success={}, elapsed={elapsed:?}, content={}",
+        result.success, result.content
+    );
+    // exact? should find rfl or similar
+    assert!(
+        result.success,
+        "exact? should find a suggestion: {}",
+        result.content
+    );
+    assert!(
+        result.content.contains("rfl") || result.content.contains("exact"),
+        "should suggest rfl: {}",
+        result.content
+    );
+}
+
+// --- lean_verify via tool dispatch (e2e through execute_tool) ---
+
+#[test]
+#[ignore] // Requires lean-lsp-mcp + Mathlib
+fn lsp_verify_via_execute_tool() {
+    let lsp = spawn_lsp().expect("lean-lsp-mcp not available");
+    let workspace = std::env::temp_dir().join("openproof-test-verify-tool");
+    let _ = std::fs::create_dir_all(&workspace);
+
+    let lean_content = "import Mathlib\n\ntheorem e2e_test : 1 + 1 = 2 := by norm_num\n";
+    std::fs::write(workspace.join("Scratch.lean"), lean_content).unwrap();
+
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: &workspace,
+        imports: &[],
+        lsp_mcp: Some(lsp),
+        prover: None,
+    };
+
+    // Warmup
+    let _ = execute_tool("lean_verify", r#"{"file": "Scratch.lean"}"#, &ctx);
+
+    // Incremental
+    let start = Instant::now();
+    let result = execute_tool("lean_verify", r#"{"file": "Scratch.lean"}"#, &ctx);
+    let elapsed = start.elapsed();
+
+    eprintln!(
+        "lsp_verify_tool_e2e: success={}, elapsed={elapsed:?}, content={}",
+        result.success, result.content
+    );
+    assert!(result.success, "e2e verify should pass: {}", result.content);
+}
+
+#[test]
+fn lean_check_missing_args() {
+    let ctx = ToolContext {
+        project_dir: lean_project_dir(),
+        workspace_dir: Path::new("/tmp"),
+        imports: &[],
+        lsp_mcp: None,
+        prover: None,
+    };
+
+    let result = execute_tool("lean_check", r#"{}"#, &ctx);
+    assert!(!result.success);
+    assert!(
+        result.content.contains("missing"),
+        "should report missing args: {}",
+        result.content
+    );
+}
diff --git a/crates/openproof-model/src/tools.rs b/crates/openproof-model/src/tools.rs
index 2956e7a..ebbe39d 100644
--- a/crates/openproof-model/src/tools.rs
+++ b/crates/openproof-model/src/tools.rs
@@ -97,16 +97,21 @@ fn lean_check_tool() -> Value {
     json!({
         "type": "function",
         "name": "lean_check",
-        "description": "Run `#check <expr>` in Lean 4 to look up the type of an expression or find the exact name of a Mathlib lemma. Returns the type signature.",
+        "description": "Look up the type signature of one or more Lean 4 expressions. Accepts a single `expr` or a batch of `exprs` (preferred when checking multiple names). Batching is much faster than separate calls.",
         "parameters": {
             "type": "object",
             "properties": {
                 "expr": {
                     "type": "string",
-                    "description": "The Lean expression to check, e.g. 'Nat.Prime.dvd_mul' or '@List.map'"
+                    "description": "A single Lean expression to check, e.g. 'Nat.Prime.dvd_mul' or '@List.map'"
+                },
+                "exprs": {
+                    "type": "array",
+                    "items": { "type": "string" },
+                    "description": "Multiple Lean expressions to check in one call, e.g. ['deriv_add', 'deriv_mul', 'deriv_const']. Preferred over repeated single-expr calls."
                 }
             },
-            "required": ["expr"],
+            "required": [],
             "additionalProperties": false
         }
     })