ツール

MCP server for the Lean 4 theorem prover: lets agents read proof goals, diagnostics and definitions and search theorems via LeanSearch and Loogle, helping mathematicians and students with formal proofs. Needs uv and the Lean toolchain; run it from the Lean project root.

Lean 4 theorem-proving plugin with workflows to draft, formalize, prove, disprove, review and golf proofs, plus mathlib search, axiom checks and safety guardrails, helping mathematicians and teachers produce machine-checked proofs. Needs Lean 4 and mathlib; pairs well with lean-lsp-mcp.