Kevin Kappelmann (Jun 30 2026 at 07:07): Kevin Kappelmann (Jun 30 2026 at 07:07):We have built a Model Context Protocol (MCP) server that lets AI agents interactively write, edit, and explore Isabelle theories and ML files.
The MCP is headless and editor-agnostic. You can let the agent work on its own or run it alongside Isabelle/jEdit or Isabelle/VSCode.
It currently requires a development version of Isabelle (we tested it with Isabelle/c13a4bd3c018). A stable release aligned with Isabelle2026 is planned.
The README covers installation and usage notes: https://github.com/kappelmann/isabelle-pide-mcp
Note that I/Q is an alternative Isabelle MCP which provides an Isabelle/jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the strengths of both MCPs can be combined in the future.
For feedback, questions, discussions, please use this Zulip stream.
Yutaka Nagashima (Jun 30 2026 at 13:55):@Kevin Kappelmann
Note that I/Q is an alternative Isabelle MCP which provides an Isabelle/jEdit-centred workflow.
Experience reports using both systems are very welcome: we hope that the strengths of both MCPs can be combined in the future.
I’d be interested in incorporating this into AbductionProver.
From your perspective, are there already any philosophical or design differences between your Isabelle MCP and I/Q?
I'm curious whether the two systems have different long-term goals.
Notification Bot (Jun 30 2026 at 14:25):A message was moved from this topic to #New Members & Projects > PIDE MCP by Kevin Kappelmann.
Kevin Kappelmann (Jul 13 2026 at 07:58):We released a version compatible with Isabelle2025-2 in branch 2025-2 of the repository:
https://github.com/kappelmann/isabelle-pide-mcp/tree/2025-2
We also improved the MCP's edit tool and added a plugin system such that users can freely add and remove tools on their own. Enjoy!
Last updated: Jul 18 2026 at 02:40 UTC