Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] PIDE MCP: Connecting AI Agents to Isabelle

view this post on Zulip Email Gateway (Jun 30 2026 at 07:19):

From: Kevin Kappelmann <cl-isabelle-users@lists.cam.ac.uk>

Dear list,

We have built a Model Context Protocol (MCP) server that lets AI agents
interactively write, edit, and explore Isabelle theories and ML files. [1]

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 [2] 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.

Best wishes,

Kevin

[1] https://github.com/kappelmann/isabelle-pide-mcp
[2] https://github.com/awslabs/AutoCorrode/tree/main/iq

view this post on Zulip Email Gateway (Jul 01 2026 at 14:39):

From: Tobias Nipkow <nipkow@in.tum.de>

A short user report:
I have used this Isabelle-Claude Opus connection and was very pleased with it.
It worked very well for a few formal language autoformalizations.

Tobias

On 30/06/2026 09:19, Kevin Kappelmann (via cl-isabelle-users Mailing List) wrote:

Dear list,

We have built a Model Context Protocol (MCP) server that lets AI agents
interactively write, edit, and explore Isabelle theories and ML files. [1]

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 [2] 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.

Best wishes,

Kevin

[1] https://github.com/kappelmann/isabelle-pide-mcp
[2] https://github.com/awslabs/AutoCorrode/tree/main/iq

smime.p7s

Last updated: Jul 02 2026 at 07:34 UTC