The day's last session opens with introductions that matter more than usual, since each panelist's backstory becomes the lens they answer everything else through. Simone Severini, from the office of the CTO at Google, moderates: Scott Duke Kominers from Harvard Business School (virtual), Natarajan Shankar from SRI International (also virtual), and in the room, Sabrina Pasterski from the Perimeter Institute and Joseph Tooby-Smith from the University of Bath.
Four routes into formalization
Shankar goes first. He's been at SRI's computer science laboratory for something like 37 years, in formal methods generally for about 45. In the early 1980s the state of the art was proving individual theorems — arguments spanning a paragraph or so — and he instead formalized proofs spanning a textbook, including the first incompleteness theorem and the Church-Rosser theorem, using an early Boyer-Moore theorem prover, Thm, developed in the same SRI lab. That led his thesis advisor, Robert Boyer, to state "Boyer's theorem": formalization of mathematics is entirely feasible. Since then he's built the PVS proof assistant, the Yices family of SMT solvers, and the SAL model-checking tools.
Scott Kominers is a market designer and economic theorist at Harvard Business School and the Harvard Department of Economics, also a research partner at a16z crypto, with a background as a number theorist. Newer to formalization than the rest of the panel, he sees parallels between an organized math corpus and how economic theory gets used in the world, and has recently been working with Ken Ono and Carina Hong and others at Axiom Math, aiming to build "an economics analog of Mathlib".
Sabrina Gonzalez Pasterski is faculty at the Perimeter Institute for Theoretical Physics. A year ago, she says, she'd have been watching these NAS AI-for-Math meetings just to make a list of people to bother; now she's in the room asking, in her words, "the dumb questions" — does it have to be academia versus industry, and can researchers build equity in the infrastructure rather than just watch the value flow into companies?
Joseph Tooby-Smith is introduced; the moderator slips and addresses him once as "Joel" a few lines later.
A high-energy physicist by training, he turned to Lean three years ago, before the current AI wave. His library went through two name changes — HepLean, then PhysLean — before settling on PhysLib, after merging with a quantum information library. He's now a lecturer in computer science at Bath; the goal of PhysLib is to be "something like Mathlib, but for physics", carrying the physics context around a result, not just its mathematical content.
The Protein Data Bank problem
Severini's first question goes to Tooby-Smith: through his work leading the charge to formalize physics in Lean, he's argued for transitioning away from static papers toward a single community-driven corpus, and often draws a parallel to the Protein Data Bank. His answer is the clearest through-line of the whole panel. He walks through a short history of "wow" moments in AI — Go beating a human, more recently the Erdős problems and the unit distance conjecture — but argues AlphaFold sits above all of them, made possible by the Protein Data Bank, a structured database of protein results. Where are the equivalent wow moments in physics or chemistry, he asks, and isn't the answer simply that "we haven't organized the knowledge that we have in the correct way"?
He frames the moment as a tug-of-war between a pull toward something more structured — what Mathlib and autoformalization have already demonstrated works — and a push away from papers, since trust in them is dropping as AI makes it easier to write, review, and read them. Those forces aren't currently pointed the same direction: "That's why right now I'm saying we need to move towards something that is better, and now's the time to do that".
Asked how such a project avoids becoming, in Severini's phrasing, a "specialized academic sandbox", Tooby-Smith splits the answer in two. Short-term, he borrows a line attributed to the Apache Software Foundation, "Community before code" — build the community first and good code follows; writing the code itself, he adds, is "kind of the easy part... AI can do that". Long-term, the harder problem is trust: mathematicians and physicists skeptical of AI-produced work need to feel proud to contribute, and proud of what's in the corpus.
A CERN model for physics
Severini turns next to Pasterski, of the Perimeter Institute, asking about the business case for what she calls a scientific knowledge layer.
Her CERN analogy is candid about the funding problem underneath it all. The historical pitch for theoretical physics — "look back at GR and its impact on GPS, or quantum mechanics and its impact on the transistor" — "used to drive me up a wall," she says, because it puts the whole value proposition on faith. CERN's parallel is that a collider or detector generates transferable technology value alongside the physics; can theoretical physics, via a formalized knowledge corpus, do the same?
She then turns the question on the room. Academic employment is comparatively cheap, she argues — a "cheap labor" pool whose whole passion is a given subfield, custodians of a knowledge canon. Does it have to be zero-sum between faculty lines and tooling investment? Her "dream scenario" involves a committed pool of investment money, open communication between researchers instead of "friends of friends" lab access, and funding structures — "even like a Genesis project or whatnot" — plus "nice ground rules for public-private partnerships" so the value created funds the researchers themselves.
Kominers offers a working analog: venture funds in blockchain have run "miniature versions" of this for years, since almost every blockchain business rests on a cryptography or incentive-design question, letting an investor benefit from field-wide advances rather than just company-specific ones. He can explain Lean to "a randomly selected MBA student" and have them immediately grasp its relevance to their company, unusual for formal logic infrastructure, and hopes formalization's use cases will be "very near term".
What to build first, and who coordinates it
Asked what to build first, Pasterski describes the near-term goal as getting industry people (who know the market case) and research people (who know which questions are tractable) in a room often enough to find achievable goals. Physics, unlike mathematics, lacks a deep bench of long-standing, well-posed open problems, so part of the work is inventing "challenge questions". She raises XPRIZE as precedent — a deadline, a prize pool, target questions, a scoring model that refunds toward further research if the deadline is missed — and credits coding tools, "you can really code stuff now with these Claude or Codex or whatnot", with democratizing what used to require hiring a dedicated coder. She wants a body like NAS to play coordinator, saying plainly this isn't going to be profitable to companies for the next year, so academic groups aren't racing a well-resourced lab behind closed doors — comparing the risk to a "Bell Labs closed door".
Trust, papers, and getting non-mathematicians in
A batch of Slido questions follows. George Carlin argues the real problem with papers is that nobody vets them for truthful research, and asks whether AI can do that vetting. Tooby-Smith sidesteps the trust question: a corpus gives you benefits papers structurally can't, regardless — interdependencies between results, the way Mathlib links proofs together, more you can "just do" with structured data than prose. "We've been using papers since the printing press", he says, and in 100 years "it's very unlikely... that we're still going to be writing papers" — a shift that needs to start now.
Tyler Josephson asks how non-mathematicians get brought into formal mathematics given how easy code generation has made things. Shankar's answer is the most quotable line of the panel: getting mathematicians to use formal tools has always been hard, and the value proposition is hard to appreciate until you practice it — at which point "it's actually like having the paper talk back at you and give you... embarrassing feedback on your mistakes," or, in his phrase, "you get to debug your neurons". Something has genuinely changed lately: the "connectedness" formal methods used to lack is now closing, as AI flattens the learning curve.
Abstraction engineering, and truth as a tower of approximations
Severini relays a sharper question from Nicolas Rouquette, framed almost as a thesis: in mathematics, truth is built on absolute foundations; in science and engineering, truth is a tower of carefully chosen approximations — does Shankar agree? He describes his own profession as "abstraction engineering": building towers of abstraction from models, theories, grammars, and programs, sometimes shaping the model to reality and sometimes bending reality toward the model. Successes he lists: Carolyn Talcott modeling biological pathways with logic-based tools; John Rushby formalizing pilots' mental models of automation to catch "automation surprises" before they happen; the company Imandra modeling stock exchanges and financial regulations; NASA formalizing air traffic control safety margins into an extensive PVS library, NASALib — noting that formal models let you quantify the modeling error itself, bridging to simulation and uncertainty quantification. Pressed on why formalization "becomes much more complicated in engineering", he credits generative AI's latent space with being unusually well-organized for bridging informal and formal representations, catching modeling errors early enough to save trouble in hardware-in-the-loop testing.
Severini then reads back a line from the meeting's prep notes, attributed to Dana Scott: "Formalization is an experimental science".
Severini reading the Dana Scott line from the meeting's prep notes. Shankar's gloss: most people think formalization validates results — tells you something is right or wrong — but "that is not the experience of those who actually work with formalization". What you actually get is fast, cheap feedback that lets you refactor and try different formalizations of the same concept, which is why he worries about "casting things in stone" in libraries. "The spirit of formalization is that it's not rigor mortis, it's actually liberating".
Citations as composability, and who gets academic credit for curation
The next stretch belongs to Kominers, asked directly about redesigning the academic reward system as a market designer. Institutions "move slowly... in part by design", but he argues the building block of "a contribution to knowledge" has already changed multiple times in recent memory, most obviously once knowledge became networked and global on the internet. His central claim: citations were always a rough proxy for composability — how many ideas feed into yours, how far yours moves things forward — and formalization lets you draw that dependency graph exactly, including, for economics, "assumption accounting": knowing precisely what assumptions a model made so you can reason about how much it taught you about physical or economic reality.
But new contribution types — curation, synthesis, translation into practice — lack a robust analog in existing academic credit systems, even as material volume explodes. Conference submission counts have gone, in his words, "from 1,000 submissions to 10,000 submissions to 70,000 submissions", part of a broader "10 to 40x increase in submissions" the journal system isn't built to absorb. His conclusion: there needs to be "a very powerful and important and distinguished role for the curators," one academia hasn't figured out how to reward yet.
Blockchains as prior art, and the compute bottleneck
Asked to connect this to blockchain and crypto infrastructure, Kominers defines a blockchain plainly as "a type of database with a specific set of guarantees" — open, decentralized, capable of immutable commitments to stay open, unlike a web platform that opens an API and closes it once network effects kick in — and also a ledger recording the hierarchy and composability of software. Blockchain communities, he argues, have already worked through questions this panel keeps circling: rewarding open-source participation through token and fee-sharing schemes, and how the network effect shifts from the platform to the underlying protocol in these "protocolized economies". He's candid about limits too — protocols have succeeded in some ways and struggled in others, since you can observe how many pieces of software embed a component but "can't actually observe how much value is being created" further up the chain.
An audience question relayed live, from someone identifying with the Ethereum Foundation, pushes on scale: how big does this have to be before it's worth convincing Ethereum or elsewhere in crypto to run it as a real experiment? Kominers' answer is mostly "we should talk offline", though he names examples: a research corpus on long COVID, a math project attempting blockchain-based systemization of automated mathematics, and blockchain registries for biobanks and tissue samples. At all-of-science scale, the real bottleneck is compute — blockchains aren't yet ready as computation layers, and storage is at a premium since it depends on incentivizing decentralized storage. His pattern: keep data infrastructure off-chain, enshrine only open access on-chain. "And then you just try to find someone to give the compute, like Google. No" — a jab at Severini's employer.
Paywalls, creative discovery, and open models
Three more Slido questions round out the session. Catherine Russo asks whether formalization-based tools will fragment, with some locked behind paywalls. Tooby-Smith: "I hope not" — he argues for what's best for humanity over any one company, disagrees "completely" with companies keeping libraries closed, and calls for "the right equilibrium".
Mandana Reisie asks how future AI can support creative scientific discovery and rigorous formal verification without sacrificing either. Shankar's answer is the panel's most cautionary moment: there's real synergy between exploration, rigor, and AI, but delegate proof construction wholesale to generative AI and we "descale" ourselves into human reviewers of AI content, accelerate inequality since whoever controls the resources controls the means of production, and build a mountain of technical debt as AI masks deficiencies. His prescription: operationalize something like the Leiden Declaration into an action plan so the technology amplifies human capability instead.
Will Zen asks whether panelists should push for funding open reasoning models alongside open infrastructure, to avoid dependence on proprietary tools. Pasterski is less confrontational toward industry than the question invites: she likes that there's now transferable value in this space, wants researchers to learn from industry as much as industry uses their labor cheaply, and notes agentic coding tools make researchers less "victims of circumstance" — but the immediate ask is subsidized access to existing models, so the field isn't split by "this inequity between the tools that they have access to".
The room's last question: models, reality, and metaphysics
With a few minutes left, an audience member identifying as working at the Ethereum Foundation asks the final substantive question. His first contact with formal mathematics, he says, was trying to formalize Noether's theorem in Isabelle back in 2015.
Doing physics, biology, or engineering means caring about more than mathematical correctness, since you're working with a model that has to be validated against reality. An aside — "I guess Kim has fixed this issue for us" — refers to something not clear from context.
His question to Tooby-Smith: how do you justify the resources a foundational library like PhysLib takes, while also bridging to real physics, biology, and engineering?
Tooby-Smith stays close to home: PhysLib's job is to encode physics reasoning that Mathlib doesn't carry, sitting downstream of it, so a physicist's starting assumptions can go straight into the project. He notes a real limit: the project favors computability where possible, but "this is not always possible in Lean" — Feynman diagrams, he says, "you can't really just do... in a computable way".
Pasterski's answer turns philosophical. Her own subfield — high-energy theoretical physics — takes a reductionist approach: given what's known about the universe's physical content, you use mathematical consistency to bootstrap toward a fundamental theory, framed as building a knowledge graph where dualities show up as redundancies within it, something she's happy to scope narrowly "for the business case of my own little subfield".
She distinguishes that from a hypothetical where "GPT-8's going to solve theoretical physics" as an oracle for individual problems — physics isn't about having an oracle, she says, it's about the space of possible axiomatizations and whether a fundamental theory can even be distinguished from its alternatives, questions she calls genuinely metaphysical. She closes on an unguarded note: "We're at the time now where we can do this. Isn't that really f*g cool?"
The session's last exchange circles back to Shankar's "abstraction engineer" framing — model-checking technology, built for hardware verification, turning out useful in biology — and closes with Kominers noting that economics faces the same problem: narrowing a proliferation of separate economic ideas into one grand unified model.
End of Day 1
The moderator calls for a final question and gets none. Severini thanks the panelists, the room, and everyone online, closing on a two-line summary: real challenges, but real opportunities, and a room full of people ready to think differently about resources. Day 2 starts at 9:00 a.m., pointed at the future of mathematics — a story for the next post in this series.