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

Merged

markm39 merged 6 commits into

worktree-refactor+lean-check-optimization

Mar 28, 2026

Commits on Mar 28, 2026

feat(lean): use Pantograph for lean_check, add batch support
markm39
committed
fix(lean): remove failed lean_verify/lean_eval Pantograph attempts
markm39
committed
feat(lean): route lean_verify through LSP for incremental elaboration
markm39
committed
test(lean): add LSP verify tests, fix sorry detection for backtick quotes
markm39
committed
feat(lean): add LSP fast path for lean_eval and lean_search_tactic
markm39
committed
Merge remote-tracking branch 'origin/master' into worktree-refactor+lean-check-optimization
markm39
committed