Great event organized by National Academy of Sciences and Defense Advanced Research Projects Agency (DARPA), regarding…

M / 000

Great event organized by National Academy of Sciences and Defense Advanced Research Projects Agency (DARPA), regarding AI and the (auto)formalization of mathematics. AI in mathematics is moving forward at an incredibly high speed. Mathematics really is the proving ground for AI, where rigorous and disciplined reasoning matters as much as in life-or-death decisions.

In the last couple of days I got myself convinced that AI can help with (auto)formalizing mathematics and even mathematical discovery. To prevent non-sense, the generative AI needs to be coupled with a very strict gating function: a theorem prover. With the help of Claude, I generated the completeness proof of separation logic in Lean. This was done in only a couple of days, while that same proof effort took me many years during the PhD. It even showed me a direct proof of a novel and really elegant Lindenbaum construction involving the general @-connective, going beyond what I was able to find myself, and I got an incredibly deep insight in the nature of pointer structures. Heck, it even discovered a new axiomatization for arithmetic itself, that uses separation logic and only the binary successor and less-than relations! (Blog post will come out soon.)

Thanks to Patrick Shafto, Terence Tao, Axiom Math, and many others for this event. https://www.nationalacademies.org/units/DEPS-BMSA-22-P-451/event/46979?status=attended&session=4253994&eventID=364145&ID=71240453

nationalacademies.org Organizing Mathematical Knowledge in the Age of AI and Formalization Recent advances in AI-assisted mathematics and formalization are rapidly changing how mathematical knowledge is created, organized, and validated. As these capabilities mature, they raise broader questions about the future of mathematical knowledge as a form of shared infrastructure—not only for mathematics itself, but also for science, engineering, and other high-assurance domains that depend on reliable reasoning. This meeting will bring together experts from the mathematics, formalization, and AI communities as well as leaders in industry, government, philanthropy, and more. Discussions will focus on questions of infrastructure, incentives, and coordination, as well as the role that different sectors can play in shaping the future of the field.

First published on LinkedIn. The event is Organizing Mathematical Knowledge in the Age of AI and Formalization, held 20–21 July 2026; the day this was posted is not recorded, so the date above is the day the event opened.