David Wang (Jul 24 2026 at 13:43): David Wang (Jul 24 2026 at 13:43):Does someone know whether most Isabelle users use LLMs to write Isabelle theories and if yes, how?
Notification Bot (Jul 24 2026 at 13:44):A message was moved here from #New Members & Projects > PIDE MCP by Kevin Kappelmann.
Kevin Kappelmann (Jul 24 2026 at 14:30):You can connect agents to Isabelle via MCP. Here are 2 options:
David Wang (Jul 24 2026 at 14:37):Kevin Kappelmann said:
You can connect agents to Isabelle via MCP. Here are 2 options:
Thanks. I have been using I/Q for the past months and am really happy with how well Claude Opus 4.8 and Fable 5 with reasoning set to high or more handle and refactor projects (8k to 35k LOC + AFP imports).
Making them delegate harder proofs to other Opus/Fable agents keeps them somewhat on track in longer sessions. System prompts and skills make them interact smoothly with I/Q and isabelle through the terminal.
I wonder how others use LLMs and which ones and what their impression is.
Kevin Kappelmann (Jul 24 2026 at 15:34):maybe some talks from the isabelle workshop are of interest to you. it is running right now and streamed online:
https://sketis.net/isabelle/isabelle-workshop-2026
András Salamon (Jul 24 2026 at 17:42):I have used LLMs to build proofs of classical results in low-level computational complexity, currently around 65Kloc. This is using the isabelle-query syntax-aware approximate theory search tool, isabelle build with timeouts, a lot of design documents, and human steering.
At the Isabelle workshop Josef Urban earlier today reported on two completed formalisations of entire mathematics textbooks with LLMs, essentially autonomously; with a large prompt, low timeouts, and sledgehammer.
Yong Kiam (Jul 24 2026 at 21:05):with the caveat that I haven't fully inspected the formalization, I tried this past week to use the PIDE MCP mentioned earlier to formalize a certain messy result in theoretical cryptography (22k LoC with wc -l). It worked pretty nicely out of the box with a mix of Fable + subagents (except the interface sometimes hangs...)
Jonathan Julian Huerta y Munive (Jul 30 2026 at 14:17):You might want to try the cli tools that were used in Josef's autoformalisation experiment above and have matured since then. The only caveat is that you have to suggest the agent to do the sorry approach mentioned in the paper because otherwise the agents try to fill-out the tactics themselves and that costs.
Last updated: Aug 05 2026 at 21:11 UTC