Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] I/Q plugin for AI <-> Isabelle/jEdit interaction

view this post on Zulip Email Gateway (Aug 22 2025 at 12:44):

From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi,

We just pushed "I/Q", an experimental mechanism for AI agents to interface with live Isabelle/jEdit sessions for autonomous/collaborative interactive theorem proving.

I/Q is an Isabelle/jEdit plugin exposing proof editing/exploration capabilities as an MCP server:

  1. Reading and writing theory files through jEdit
  2. Querying open documents and document stats (warnings, errors, timing information)
  3. Querying command states (e.g. intermediate proof states)
  4. Proof search and exploration via sledgehammer, find_theorems, and an overlay-based mechanism for try-running Isar proof steps/scripts without interfering with the user.

See the README for details. Once setup, you start your favorite MCP-capable chatbot (e.g. Amazon Q: https://aws.amazon.com/q/) and interface with an open Isabelle/jEdit IDE through natural language.

Please note:
I/Q is still a very early prototype. We expect that its mechanisms will need tweaking/expanding. I/Q is mechanism only: It needs to be complemented with behavioral guidance and/or additional knowledge to become an effective proof engineer. We share I/Q with the community at this early stage because we see experimentation as the primary path to identify those improvements. If you are curious, please try I/Q and let us know about your use cases and ideas for improvement!

I/Q is part of AutoCorrode and can be found here: https://github.com/awslabs/AutoCorrode

Best,
Hanno

Last updated: Sep 13 2025 at 04:22 UTC