Qiyuan Xu (Jul 27 2026 at 15:24): Qiyuan Xu (Jul 27 2026 at 15:24):Following the AoA proof agent, I'd also like to announce Isabelle-MCP, which I built a couple of months ago as a development tool for AoA (and which, as a result, has been more or less battle-tested for a while now). It was developed in parallel with Kevin's. (Apologies — I wasn't aware Kevin was working on his at the time; had I known, I probably wouldn't have duplicated the effort)
Functionally, the two MCPs overlap to a large extent. The most significant difference, I think, is the editing model: PIDE MCP ships its own edit tools. Isabelle-MCP deliberately provides none — the agent edits files with whatever tools it already has, including plain bash commands like sed. A file-system watcher monitors the relevant files and automatically syncs any modification into Isabelle.
(My picture of PIDE MCP comes from a fairly shallow investigation and may well contain errors — corrections welcome.)
conda create -n isabelle -c https://conda.qiyuan.me -c conda-forge isabelle-ai # Same installation as AoA — if you've already installed AoA, skip this step.
conda activate isabelle
isabelle-mcp install
conda activate isabelle
claude # OR codex
source code: https://github.com/xqyww123/Isabelle-MCP
Kevin Kappelmann (Jul 27 2026 at 15:41):Hi Qiyuan, I would argue the most significant difference is architectural: your MCP uses LSP while PIDE MCP directly manages a PIDE session. I wrote a preprint including a paragraph that compares these approaches: https://zenodo.org/records/21519365
Qiyuan Xu (Jul 27 2026 at 15:51):Thanks for the addition :+1: :+1: :+1:
Last updated: Aug 05 2026 at 21:11 UTC