Craig Alan Feinstein (May 25 2025 at 18:52): Craig Alan Feinstein (May 25 2025 at 18:52):Has anyone tried using artificial intelligence like chatgpt to save time writing proofs in Isabelle. I have tried it with ChatGpt and Claude where you pay $20 a month. Has anyone tried any other AI tools?
Craig Alan Feinstein (May 25 2025 at 19:34):I just found this article saying Baldur works well with Isabelle. https://spectrum.ieee.org/amp/ai-debug-software-2667018624
Mathias Fleury (May 25 2025 at 19:43):I have never seen a demo of the system showing that it is working for the end-user
Craig Alan Feinstein (May 25 2025 at 23:23):I didn’t see it either.
Yutaka Nagashima (May 26 2025 at 17:09):The AbductionProver for Isabelle is currently more of a search-based approach, but I still call it an AI prover.
(Also, it runs on a laptop without requiring expensive graphics cards.)
Craig Alan Feinstein (May 26 2025 at 20:37):Thank you Yutaka I will check that out. I was about to give up on Claude yesterday after having discovered that if you stay on the same conversation for a long enough time, it appears to run out of intelligent things to say with respect to your code. However, I discovered that if you transfer to another conversation, it will come up with more intelligent comments about the code.
Yutaka Nagashima (May 26 2025 at 21:39):I haven't tried Claude 4 yet.
However, I discovered that if you transfer to another conversation, it will come up with more intelligent comments about the code.
Overall, this seems like an issue someone else will automatically solve after n months or weeks—if they haven't already. We just need to wait while focusing on something else—unless you're really keen to tackle it yourself. :stuck_out_tongue_wink:
Craig Alan Feinstein (May 26 2025 at 23:33):Yutaka I’m in a spot where I would like to finish doing my proofs I’ve been working on for a long time. At this point if I can do this using ai I’ll use it.
Craig Alan Feinstein (May 28 2025 at 13:57):I figure ai is in many ways like a human. If you talk to much to it, it gets tired and eventually it gets so exhausted that it forgets a lot of what has been said and starts saying stupid stuff
Last updated: Jun 29 2025 at 20:22 UTC