Email Gateway (Jun 10 2026 at 13:47): Email Gateway (Jun 10 2026 at 13:47):From: "\"Becker, Hanno\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi everyone,
Another report on an AI-related experiment.
I used Claude Opus + AutoCorrode's I/Q & I/R to auto-formalize an old paper of mine, and check + type-set everything using Isabelle's document preparation system. The result is here: https://eprint.iacr.org/2026/1223.pdf
Takeaways:
Unsurprisingly, by now: Claude has no difficulties formalizing the material from the original PDF.
Somewhat surprisingly: Claude wasn't great (in my subjective view) at documenting the material in a way that would make for a pleasant read. I basically shaped the entire narrative.
Claude + I/R were effective at working out proofs in the background (sometimes multiple at once) while I did 'shallow' editorial / narrative work in the same Isabelle/jEdit session. Irrespective of I/R's ad-hoc implementation that needs revisiting, it reinforced the usefulness of a collaborative Human<->AI interaction model to me.
I had not used Isabelle's document preparation system in earnest before, and came away very pleased. With a bit of template customization and selective hiding of material, the formal sources turn into a paper-shaped document that — hopefully! — someone might enjoy. I wish I'd discovered this earlier; the defaults hadn't grabbed me, and I suspect a slightly more inviting out-of-the-box look would help others appreciate the maturity and power of the approach sooner.
The full sources are available here: https://github.com/pq-code-package/mldsa-native/tree/main/proofs/isabelle/neon_ntt (hosted on the mldsa-native implementation of ML-DSA, which uses the modular arithmetic kernels developed in the paper).
All the best,
Hanno
Last updated: Jun 12 2026 at 04:13 UTC