About Isabelle MCP
Isabelle MCP is an MCP server published by xqyww123 in the Other category.
The repository has 4 stars and 2 forks, with the last commit a month ago. Recent commit activity is the strongest signal that reported issues will get attention.
Install
git clone https://github.com/xqyww123/Isabelle-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 (13)
isabelle_cancel_evaluationCancel a running evaluation
Parameters not published.
isabelle_command_outputProver output messages
Parameters not published.
isabelle_command_statusWhat state the command(s) covering each of several lines are in
Parameters not published.
isabelle_definitionJump to symbol definition
Parameters not published.
isabelle_evaluate_toEvaluate the theory up to a line; returns a per-file snapshot of errors / sorry / running command lines
Parameters not published.
isabelle_evaluation_statusPoll progress of a running evaluation (same snapshot)
Parameters not published.
isabelle_find_theoremsSearch the theorem database in the context at a position (Isabelle's `find_theorems`): by name, pattern, intro/elim/dest, solves, simp
Parameters not published.
isabelle_goal**Proof goals** — omit after_text for before/after diff
Parameters not published.
isabelle_hoverType info and documentation at position
Parameters not published.
isabelle_launchStart (or restart) the prover with the session/logic that fits the work (bare `Main` is only a minimal fallback); **call this first**
Parameters not published.
Show all 13 tools
isabelle_local_occurrencesIn-file occurrences (definition + uses) of a local entity
Parameters not published.
isabelle_session_infoCurrent session info
Parameters not published.
isabelle_terminateTerminate the running prover (the MCP server stays up; you can relaunch)
Parameters not published.
Ask AI
Ask AI about Isabelle MCP
Powered by Claude · Grounded in docs
Security checks
6 checks have not been run yet.