About Lean Aristotle MCP
Lean Aristotle MCP is an MCP server in the Other category.
Install
git clone https://github.com/septract/lean-aristotle-mcpThis server has no ConduID identity, so agent calls to it are not receipted. Pin the version you install and review the source before granting it credentials.
Tools (6)
check_formalizePoll async formalization jobs for completion
Parameters not published.
check_proofPoll async proof jobs for completion
Parameters not published.
check_prove_filePoll async file proof jobs for completion
Parameters not published.
formalizeConvert natural language math to Lean 4 code
Parameters not published.
proveFill in `sorry` statements in Lean code snippets
Parameters not published.
prove_fileProve all sorries in a Lean file with automatic import resolution
Parameters not published.
Ask AI
Ask AI about Lean Aristotle MCP
Powered by Claude · Grounded in docs
Security checks
6 checks have not been run yet.