LeanProbe

Fast Lean 4 proof verification for coding agents via the LeanProbe MCP server's warm REPL. Use when you need to know whether Lean 4 code compiles (no errors, no `sorry`), iterate on a declaration inside a Lake/Mathlib project, test a replacement proof candidate, or explore a goal tactic by tactic — far faster than `lake build`. Covers the lean_check / lean_check_target / lean_status / lean_proof_state / lean_tactic / lean_close_proof tools, reading `success` vs `ok`, the error codes, and how `cwd` is resolved. Requires the `lean-probe` MCP server to be connected.