4 ms·
Curious if there is any analysis on how often an LLM can create proofs correctly without special prompting.
by Karrot_Kream 8mo ago
Curious if there is any analysis on how often an LLM can create proofs correctly without special prompting.
- namin 8mo agoSince around Opus 4.5, systems like Claude Code are very good at Dafny proofs. They don’t get everything right in one shot but can iterate with verifier feedback. Some proofs take over 20 minutes to complete. The system knows to put temporary axioms to tackle proofs step by step.
- Karrot_Kream 8mo agoAwesome thanks! Would be nice to have a sort of "worked example" where you take a simple project and derive Typescript and Dafny for it and have the LLM (Claude) generate proofs. Just some feedback to broaden it up to folks not as familiar with Dafny.
- namin 8mo agoThanks, we will provide case studies. Already today, lemmafit doesn't need familiarity with Dafny. It is used under the hood, so you just use Claude Code normally and lemmafit adds the verification harness. You don't need to interact with Dafny or the proofs at all.