Organizing Mathematical Knowledge in the Age of AI
A National Academies meeting on how AI-assisted mathematics and formalization are changing how mathematical knowledge is created, organized, and validated — both days, eleven talks and panels, recapped and slide-checked.
Day 1 · July 20, 2026
7 postsTraffic Jams on 19th-Century Streets: Terence Tao Opens the NAS Meeting on Mathematical Knowledge
Terence Tao · UCLA
Traffic jams on 19th-century streets: why proof abundance, not proof scarcity, is the era's real problem.
Read the postCertificates, Not Proofs: A Panel on Where Formalization Actually Stands
Panel discussion · Moderated by Melanie Matchett Wood (Harvard); with Matt Ballard (U South Carolina), Javier Gómez-Serrano (Brown), Jesse Han (Math, Inc.), Jaume de Dios Pont (NYU), Jason Reed (Lean FRO)
Disposable certificates versus reusable libraries: where formalization actually stands today.
Read the postExtraordinary Librarians: Ken Ono on Formally Verified Knowledge as Infrastructure
Ken Ono · University of Virginia & Axiom Math
Extraordinary librarians: from a perfect Putnam to eighteen new papers, and what a formally verified proof is actually for.
Read the postWhat Lean Actually Looks Like: Alex Kontorovich Proves the Handshake Lemma, Live
Alex Kontorovich · Rutgers University
Building a handshake-parity proof live in Lean, with an LLM as the deterministic pair's stochastic partner.
Read the postA Library Launches Mid-Panel: Tau Ceti and the Question of What Comes After Mathlib
Panel discussion · Moderated by Lauren Williams (Harvard); with Andrea Ferrari (Cambridge), Benjy Firester (MIT), Xinze Li (Toronto), Kim Morrison (Lean FRO)
A library launches mid-panel: the question of what comes after Mathlib, live cross-examination included.
Read the postShow Me the Money: A Panel on the Formalization Resources Landscape
Panel discussion · Moderated by Brendan Hassett (Brown); with Ralph Abboud (Renaissance Philanthropy), Carina Hong (Axiom Math), David Spergel (Simons Foundation), Shida Wang (XTX Markets)
Show me the money: funders, tool-builders, and the question of whether there's still a future in proving theorems.
Read the postThe Protein Data Bank Problem: Formalizing Knowledge Beyond Mathematics
Panel discussion · Moderated by Simone Severini (Google); with Scott Duke Kominers (Harvard Business School), Sabrina Pasterski (Perimeter Institute), Natarajan Shankar (SRI International), Joseph Tooby-Smith (U Bath)
Beyond mathematics: formalized knowledge as infrastructure for science, engineering, and academic credit itself.
Read the postDay 2 · July 21, 2026
4 postsTrust, Interpretability, and Worms: Andrew Blumberg's Science Fiction for Formalization
Andrew Blumberg · Columbia University
Trust, interpretability, and worms: a working scientist's science fiction for what formalization does to science itself.
Read the postMathlib, Moats, and Many Names for the Same Object: A Panel on Infrastructure for Mathematical Knowledge
Panel discussion · Moderated by Ravi Vakil (Stanford / AMS); with Stella Biderman (EleutherAI), Alexander Hicks (Ethereum Foundation), Jared Duker Lichtman (Stanford), Bernie Wang (NTT Data AIVista)
Mathlib, moats, and many names for the same object: what infrastructure for mathematical knowledge should actually be built.
Read the postIsolated Networks, Fruit-Fly Years, and the Outfield: A Federal Panel on Formalizing Mathematics
Panel discussion · Moderated by Pat Shafto (DARPA); with Stacey Levine (NSF), Mike O'Hara (NSA), George Stantchev (Naval Research Laboratory)
Isolated networks, fruit-fly years, and the outfield: how three federal agencies see formalizing mathematics.
Read the postFour Roadmaps and a Fight Over Credit: The Closing Town Hall
Report-out & town hall · Facilitated by Pat Shafto (DARPA); four working-group report-outs and closing discussion
Four roadmaps and a fight over credit: the breakout report-outs and the closing town hall that ended the meeting.
Read the post