András Salamon (May 22 2026 at 01:24): András Salamon (May 22 2026 at 01:24):I've been working with Claude Code using isabelle build as the source of ground truth, editing theories on disk and avoiding the IDE. For my project this has worked well and I now have a proof of the first main result. This takes about 30s to build. However, the cache system doesn't behave like I expected (each theory is rebuilt within a session) and the only approach that I have found to work as the project grows is to split into multiple sessions.
Is splitting into many sessions the right workflow, or is there a better approach that people tend to use?
Most of the time is spent waiting for isabelle build to generate an error or to time out, and this time increases as the theories grow even if most of the theories in a session don't change. I would appreciate pointers to more efficient workflows or ways people think about structuring projects. AFP entries tend to be single sessions (only 19 right now have two or more, 2% of the entries), with ODE on 7 as an outlier. Maybe I am using incorrect session/theory granularity?
Mathias Fleury (May 22 2026 at 04:38):Have you looked at the IDE integrations discussed on the mailing list?
Mathias Fleury (May 22 2026 at 04:40):But, at that point, you should ask claude to write a wrapper around isabelle server.
Mathias Fleury (May 22 2026 at 04:40):You are not using like anyone else is. So it is not surprising that the tooling is not great
Mathias Fleury (May 22 2026 at 05:08):*using Isabelle like anyone else is
Maximilian Schäffeler (May 22 2026 at 09:06):This paper describes an autoformalization workflow based on isabelle build: https://arxiv.org/pdf/2604.07455. In my experience, Claude is quite good at interacting with Isabelle/Q. This MCP-based approach also avoids isabelle build.
András Salamon (May 22 2026 at 11:00):Maximilian Schäffeler said:
This paper describes an autoformalization workflow based on
isabelle build: https://arxiv.org/pdf/2604.07455. ... This MCP-based approach also avoidsisabelle build.
Thanks for the pointers! I'm using custom tooling extensively but haven't looked at wrapping it in MCP or using Isabelle/Q.
The proofs are easy but bulky, with large objects being reasoned about for many steps. The challenge here seems to be balancing the writing out of proof steps in excruciating detail versus the effort put into finding a proof method that works quickly with the chosen abstractions. Carefully crafting Isar in an IDE seems appropriate for results that need more difficult reasoning but seems hard to justify here.
András Salamon (May 22 2026 at 11:03):Mathias Fleury said:
But, at that point, you should ask claude to write a wrapper around
isabelle server.
Sounds like an excellent idea, thanks!
Last updated: Jun 06 2026 at 17:17 UTC