Email Gateway (May 12 2026 at 16:50): Email Gateway (May 12 2026 at 16:50):From: "\"Lammich, Peter (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
I'm curious what AI tools you are using. I've heard a few names now like assistant, codex, IQ, but would be curious about your experience. Including: is it publicly available? How to use it ( with which editor, easy to set up?). How much does it cost (like compute costs etc), is there a free test version (like GitHub Copilot that you can use for free until you hit some token limits)?
Happy to hear about your experiences.
(In particular experience on cost are important to know b/c of funding applications, which generally require you to estimate such costs upfront)
--
Peter Lammich
Email Gateway (May 12 2026 at 18:40):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
Two rather different setups are described here:
Opencode + I/Q + Isabelle/jEdit: https://arxiv.org/pdf/2604.15713
Claude Code + isabelle build + process_theories: https://arxiv.org/pdf/2604.07455
Opencode makes it quite easy to switch between different models, also free/local ones. But to be honest free/local models are too dumb/slow to do meaningful work in Isabelle. I use GitHub Copilot Pro switching betwee Claude Sonnet 4.6 and GPT 5.4, which both have been successful in proving some non-trivial things. GitHub Copilot Pro has been free for academics, but I believe they have stopped that for new sign-ups. Also some other people could not use it with state-of-the-art models (the one I mentioned work for me, but Claude Opus isn’t there anymore for example). In addition, I have a 20$ upper limit set beyond what the GitHub Copilot Pro subscription offers (but usually stay below that).
We have also experimented with different isolation setups to avoid agents destroying our computers; my favorite is based on Docker. I am happy to share scripts (privately for now, but we also have submitted something on this topic to the Isabelle workshop), but they are “use at your own risk”. :)
Best wishes,
Dmitriy
On 12 May 2026, at 18.50, Lammich, Peter (UT-EEMCS) <cl-isabelle-users@lists.cam.ac.uk> wrote:
Dear list,
I'm curious what AI tools you are using. I've heard a few names now like assistant, codex, IQ, but would be curious about your experience. Including: is it publicly available? How to use it ( with which editor, easy to set up?). How much does it cost (like compute costs etc), is there a free test version (like GitHub Copilot that you can use for free until you hit some token limits)?
Happy to hear about your experiences.
(In particular experience on cost are important to know b/c of funding applications, which generally require you to estimate such costs upfront)
--
Peter Lammich
Email Gateway (May 13 2026 at 15:49):From: Lawrence Paulson <lp15@cam.ac.uk>
An easy option is Isabelle Assistant:
https://github.com/awslabs/AutoCorrode/blob/main/isabelle-assistant/README.md
Once it is set up, you have a chat window through which you can converse with your favourite LLM (e.g. Claude). It can see your theory file, edit it and check the response. I'm impressed at how it can write (somewhat) natural-looking proofs. It can also comment with seeming intelligence when something might be false as stated and requires additional assumptions. These are capabilities that I have dreamed of for years.
Larry
On 12 May 2026, at 17:50, Lammich, Peter (UT-EEMCS) <cl-isabelle-users@lists.cam.ac.uk> wrote:
I'm curious what AI tools you are using. I've heard a few names now like assistant, codex, IQ, but would be curious about your experience. Including: is it publicly available? How to use it ( with which editor, easy to set up?). How much does it cost (like compute costs etc), is there a free test version (like GitHub Copilot that you can use for free until you hit some token limits)?
Last updated: May 23 2026 at 03:31 UTC