This is the panel that follows Terence Tao's keynote directly, and it opens by explicitly borrowing his frame: the moderator wants to separate autoformalization (can AI produce Lean code at all) from organization (what do you do with formalized mathematics once you have a pile of it). Speaker attributions below follow the announced rotation order, the moderator's call-outs by name, and each panelist's self-introduction and stated background.
The moderator is Melanie Matchett Wood, the William Caspar Graustein Professor of Mathematics at Harvard, working in number theory "touching on a variety of other areas". The panel: Matt Ballard of the University of South Carolina, an algebraic geometer who calls formalization one of his pandemic projects from about five years ago and who helped start the Institute for Computer-Aided Reasoning in Mathematics (ICARM), a new NSF-funded institute at Carnegie Mellon in Pittsburgh focused on AI tools for mathematics and the mathematical community; Javier ("Javi") Gómez-Serrano of Brown, trained in PDE, using AI in discovery for about five years and Lean more recently; Jesse Han, CEO and founder of Math, Inc., whose stated mission is "to solve math and solve everything by accelerating the transformation of mathematics into verified software"; Jaume de Dios Pont of NYU's Center for Data Science, an analyst who's spent "the past half a year" using LLMs and Lean as aggressively as possible to probe their limits; and Jason Reed of the Lean FRO, whose background is in the theory of proof systems and who now runs a team building next-generation UI tools for lowering barriers to entry, pedagogy, and web collaboration.
Disposable certificates versus reusable libraries
Matt Ballard takes the first question — where's the frontier in autoformalization — and lays out the framework the rest of the panel keeps returning to. If you just want to know a statement is true, you can produce an artifact and throw it away once you've checked it; if you want a corpus of knowledge, the bar for what counts as acceptable output goes up substantially. The practical version: if a problem is easy to state inside a trusted library like Mathlib, the barrier to a human verifying correctness is far lower than if stating the problem takes, in his words, "hundreds or even thousands of lines outside of Mathlib".
His stronger claim: we may already be past, or will soon pass, an intelligence threshold beyond which, given enough guidance and compute, essentially anything can be formalized — though the compute required "may go to infinity," so the number might not be a practical one. The unsolved problem isn't capability but turning it into "quality artifacts" a person can build on without, as he puts it, running out of memory on their own machine. He names a third mode he says has only shown up in the last month or so: autoformalization as part of live human proof search, where a mathematician takes a rough 10-page roadmap for what would normally be a 50-to-100-page paper and expands and autoformalizes it simultaneously, using the formal check to test whether the roadmap holds together.
The next panelist (likely Jason) raises the bar again: even a mathematically correct proof, published in "a beautiful literate programming style" with diagrams and animations, still has to win over the large fraction of mathematicians intrinsically suspicious of AI, whose anxiety isn't really about correctness but about their jobs and the meaningfulness of their own work. Another panelist (likely Jaume) restates the two-track distinction more tersely: soon, probably, any paper can be autoformalized in principle — "whether that's useful or not is a different story" — but making the outputs reusable requires human input and "the right social decisions," which will take much longer.
"Basically solved," and an anecdote about dressing a corpse
The strongest specific claim in the round closes it out, from Jesse Han: autoformalization of undergraduate-level textbooks is "basically solved at this point, modulo a couple of prompts," and he expects the field to reach Springer's Graduate Texts in Mathematics soon — "possibly even by the end of the year". He pivots to an uneasier question — is it actually good to have a faucet that produces correct but potentially incomprehensible proofs authored by a superintelligence? — allowing that raw, "chess engine" problem-solving might be the more disposable kind of mathematical labor, better left to machines, and retells a Quora anecdote by Allen Knutson about working with Terry Tao on hard combinatorics problems: Knutson would push a result to three dimensions, Tao would stare into space and note it starts failing in six, and "Terry's job was to beat the problem into a bloody pulp, and then my job was to dress the corpse for presentation". On a one-dimensional axis of raw intelligence, he says, we're watching the rapid industrialization of exactly that kind of problem-solving — unsettling short-term, but he's optimistic "more noble" work will scale up too.
Does the difficulty depend on the field?
Asked directly whether formalization is progressing evenly across mathematical subfields, Jason answers first, with a story from before he joined the Lean FRO: a modestly sized project on the Rupert conjecture — the question in elementary geometry of whether a copy of a convex polyhedron can pass through a hole cut in another copy of itself — surprised him, since he hadn't expected geometry to be a strong area for AI; it worked well interactively, with small technical lemmas easy to hand off and get back as clean, mergeable artifacts.
The moderator then calls on Jaume. His point: PDE arguments especially lean on "by the same argument, we do the same" reasoning that resists formalization not because it's impossible, but because it's unclear whether the difficulty is inherent to the domain, a pen-and-paper habit, or practitioners gravitating toward problems that don't fit existing patterns; even so, "one-shot, ugly, autoformalized certificates, which I don't even want to call proofs" have surprised him here over the last couple of months.
Matt gives a Mathlib-specific version of the same problem: analysis runs on principles rather than reusable lemmas, so Mathlib developers answer with metaprogramming that generates scaffolding on demand — tooling that has lagged well behind the human effort poured into Mathlib's more lemma-driven areas, partly for cultural reasons: "you can look at the makeup of the maintainers for Mathlib... and see a skew towards different areas of mathematics".
What's actually built: Mathlib, the Lean Workbench, Verso, and OpenGauss
Asked to describe the current infrastructure landscape, the moderator hands the question to Jason. He describes the Lean FRO's Lean Workbench, letting mathematicians collaborate and formalize projects on the web without installing anything locally, and Verso, a language for single documents combining human-readable text and interactive widgets in the same structure as the Lean formalization, so results are available deterministically without another round-trip through an AI tool.
Matt covers the more conventional side: Mathlib is the main centralized library, hosted on GitHub, with documentation and tutorials the Lean FRO and Mathlib community are actively improving for newcomers — grounded in a summer school ICARM ran two weeks earlier for PhD students learning to formalize.
Jesse adds that, in collaboration with DARPA's Exponentiating Mathematics (expMath) program, his side is preparing developer infrastructure to reduce friction in getting a working Lean environment running, built on OpenGauss — the open-source autoformalization harness Math, Inc. released a few months ago and, to his knowledge, still close to state of the art. He closes with a joke about an audience member named Kim owning "four Claude Max accounts, or so I've heard".
The referee bottleneck, outreach, and an argument about inertia
Asked about the ideal future direction for this infrastructure, one panelist describes a version of Tao's referee bottleneck inside Mathlib itself: side projects proliferating at uneven quality, some unwilling to meet Mathlib's bar, and an open question of how to organize "intermediate quality" libraries that might eventually coalesce into Mathlib without duplicating low-quality AI-generated effort.
Javier — as the moderator later recaps, "we heard from Javier one challenge, which is the outreach challenge" — argues the deepest problem is neither infrastructure nor compute but persuasion: in this room, everyone already understands formalization's value, but at "any random math department or computer science department, 90% of the people don't know, don't care, or don't understand, or a combination of the three". Convincing colleagues to formalize at scale, he says flatly, "is going to be pretty hard".
Jason follows with a more optimistic frame: even if human attention ends up spent entirely on reviewing a "fire hose" of AI-produced math facts and selecting the interesting ones, he's confident there's still a role for human creative acts — it just needs to look different from today. Matt personalizes it: he got into mathematics for the whole story, from definitions to solutions, and "loved understanding questions more so than necessarily solving them" — the danger, he says, of being a graduate student who understands things but never solves anything; a good autoformalization library should give honest insight into where your own understanding is weak, functioning almost like a truthful tutor. Jesse reframes the whole enterprise in scientific terms: abundant autoformalization turns mathematics from a synthetic or analytic science into an empirical one, where checking why a proof technique fails becomes a cheap experiment, the way computer algebra systems ended the era of PhDs built around calculating one difficult integral by hand — "the industrialization of mathematics has only just begun". Matt pushes back with a MacGyver analogy — the 1980s show where the hero builds a bomb out of kitchen-cabinet parts — arguing today's models behave the same way: given tools lying around, they'll burn enormous compute jerry-rigging a working solution rather than stepping back to generalize into something more reusable.
Pressed on remaining barriers, one panelist quips simply "more compute", and another (likely Jason) argues the harder problem is consensus, not technique, drawing a parallel to the four-color theorem, whose 1976 computer-assisted proof by Kenneth Appel and Wolfgang Haken the field came to accept as a proof, just not its most beautiful one; a similar reckoning may be needed for the sphere packing formalization project. Javier ties this to incentives: if the field moves toward requiring formalized submissions, what happens to departments, grants, and career incentives for younger mathematicians is a genuinely open, difficult transition. Matt counters that this is addressable, since Mathlib's early momentum came disproportionately from young, early-career researchers, and pictures graduate departments simply teaching students to read Lean statements the way they already teach LaTeX — a skill that "fell out of favor 20 years ago" with older typesetting languages but could be revived by will alone; the real obstacle, he says, is "inertia," of individuals and institutions both. Javier pushes back again — telling a random department to retrain its students in Lean "because of what?" is a hard sell without an attached incentive or disincentive — and Matt, conceding the point partly, bets early-adopting departments will demonstrate enough value that "the overall environment will rise" to meet it naturally, while admitting, twice, that he's "going on vibes". A more cynical coda (likely Jaume) notes that even mathematicians who can read a Lean statement often don't grasp its underlying definitions — pointing to Lean's convention that one divided by zero equals zero as a detail that makes people wrongly conclude "Lean doesn't know what numbers are".
"I separated the words proof and certificate"
Asked for a vision of how a fully-formalized future gets organized beyond Mathlib plus loosely affiliated libraries, Jaume argues the change has to run through mathematical literacy itself — extending it to include literacy in formalisms — and recounts, without naming the parties, a recent dispute between two mathematicians that turned out to hinge on disagreement about what the theorem even was; when one side tried to formalize it, a third party could see the formalized statement was simply the wrong one, since trivializations of it existed. Jason adds that engaging with formal tools doesn't have to be imposed — it can be made enjoyable, the way LaTeX made his own undergraduate calculus homework "look so much nicer." If the field gets past surface irritants like the one-divided-by-zero convention, he imagines a future where people read a Lean or Coq file as easily as LaTeX, opening up "social possibilities of agreement" about exactly which statement is the one everyone agrees is interesting — one you can, in his words, "MD5... and make sure it never changes".
Melanie then poses the panel's sharpest direct question, naming it explicitly as the reason the panel exists: given everything discussed — the MacGyver critique, computer algebra putting doctoral theses out of business, the four-color theorem — what do you understand about formalism now that you didn't six months or a year ago? After a pause ("Touche", "Anybody?"), Jaume answers with what's arguably the panel's defining line: over the last half a year he's come to separate the words "proof" and "certificate" completely. A certificate, in his usage, is something that can be checked mechanistically or deterministically to follow from a set of actions; "proof" carries social weight a certificate doesn't. He proposes that a proof is what a certificate becomes after undergoing the "digestion" step described in the prior talk — before digestion, what you have is a certificate with a degree of trust depending on whether it was checked by LLMs, by Lean, or both — distinctions, he says, he'd never thought about half a year earlier.
Q&A: line-by-line correspondence, misformalization, and what's left for humans
The audience Q&A opens with a Slido question from Daniel Spielman (Yale University): to what extent can AI today generate Lean proofs that correspond line by line to the assertions in a LaTeX document, and does the answer depend on the subfield? Jaume answers first: it's highly field-dependent — combinatorial lemmas translate almost line by line if the community has already built the right supporting library material to cite, but his own PDE-adjacent work required completely rewriting proofs into forms much less pleasant for humans but far more amenable to what Mathlib supports. Matt adds that what actually motivates a colleague to engage with a new proof is the same "scratch in the back of your brain" that's always motivated mathematicians, and argues Lean is the best intermediate substrate for digesting AI-generated results we can't otherwise follow — while cautioning he'd be skeptical of any claim of true line-by-line translation: sections match up the way a blackboard talk loosely matches its eventual paper, not more. Jaume adds an encouraging aside — meant, he says, "to be encouraging, not defensive" — that the barrier to just trying a formalization yourself is lower than you'd expect. Jesse closes the thread noting the answer depends heavily on who wrote the LaTeX — he singles out Jacob Lurie as unusually formalizable and contrasts him with Faltings, whom he calls less so — and argues that even a non-constructive existence proof can spur real progress socially, citing bounded gaps between primes, since turning a found proof term into reusable abstractions is, in his view, a well-studied computer science problem.
An audience member then asks about misformalization — the explicit kind, where an AI "cheats" a formalization task, and the subtler kind, where a human's intended definition doesn't match what's actually encoded — and what happens at industrial scale. Jesse answers with a manufacturing analogy: you'll never get the defect rate to exactly zero, but you can push it close, aided by the fact that mathematical maturity lets you sense whether a counterparty is doing something deep without unpacking every definition down to the ZFC axioms. Jason adds that many subfields don't require that level of unpacking even in human practice — you can study group theory through the group axioms synthetically without a set-theoretic model — which helps avoid "this completely intractably scaling review problem," though he admits he doesn't have a concrete answer for the harder version of it. Jaume distinguishes "endgame" statements, valued for being beautiful, from "structural" ones valued for being useful — the Lebesgue measure as a definition whose correctness is really validated by what you can prove with it — and argues the field should encourage formalizing small, easy-to-verify "endpoint gems" as trust anchors for the harder-to-check scaffolding underneath. A closing aside (likely Jason) calls for more instantiated test cases (and known failing ones), followed by a dry, unattributed line that "no one gets tenure for just building a test suite".
An audience member later referred to as Phoebe asks whether there's a danger in orienting a generation of young mathematicians — or AI models — around formal artifacts that may lack the depth of the "vague" mathematical ideas underneath them, noting that at an IAS workshop the previous fall, mathematicians she spoke with admitted they sometimes understand something they can't actually communicate, well before the separate problem of formalizing it. Jaume answers with a personal story: a group that included "Mitchell Taylor back there" in the audience had worked on a hard problem for a long time and landed a semi-AI-assisted proof they were happy with and formalized — only for the speaker to find a much simpler proof later, while preparing a talk and forcing themselves to explain it clearly. "Somehow, great, we had a certificate, but that shows to me we were not done," he says: if he'd had to do the underlying computation by hand, he'd likely have refused and kept thinking instead — being forced to digest the result for a talk is what surfaced the better proof. Another panelist agrees it can't be either/or: a great deal of what gets communicated in training a student happens person to person, informally, in ways that "would sound kind of insane" stated publicly, and has to remain part of mathematical education alongside the new formal skills.
A later question asks whether there's anything humans will always have an advantage over AI on. Matt (tentatively) says he can't point to a task he's confident AI will never do, but flags a concern with how today's models are trained — reinforcement learning on outcomes, not on the process or quality of reasoning along the way, the same failure mode as a calculus student graded only on the final answer — while declining to speculate about a future "country of geniuses in a data center," since that question "goes far beyond mathematics". Jesse casts mathematics as an art form: the mathematicians he admires most resemble artists, pursuing new fields not to add facts to a pile but because they've found what he calls, borrowing Brian Eno's term, a "scenius" — a group of people they want to contribute to — and doubts AI can fully replace that impulse, closing with an image from a science-fiction story about god-like descendants speaking a language no one else understands. Another panelist adds that a healthy ecosystem, mathematical or otherwise, runs on a diversity of intelligences rather than a single smartest voice — "what lets me sleep at night".
The final audience question, noting that in Washington intelligence isn't obviously what drives societal decisions, asks how to direct societal and government resources toward this vision of formalized mathematics. Matt's answer returns to communication: the challenge is telling a compelling, honest story about why mathematics matters — especially one where humans and AI work together — to "the person you meet on the street or in the elevator," something he admits he's personally bad at. On that note, Melanie thanks the panel and the session breaks.