The meeting opens the way these things always do: Sam Koretsky from the National Academies runs through the Slido logistics, and Pat Shafto — who's convening this on behalf of the Board on Mathematical Sciences and Analytics — frames the actual question the next two days are supposed to answer. Mathematical knowledge used to live in journals, textbooks, and human heads. Formalization is now making its dependency structure explicit — not just within math, but for every field downstream of it that needs reliable reasoning. So: if formalized math is going to be infrastructure for science and technology, what should we be doing right now to make that actually work?
Then Terence Tao takes the podium, and the talk that follows is a version of one he gave at Stanford in May, updated because — his words — it was already out of date. That alone tells you something about the pace we're operating at.
The old bundle is cracking
Tao's frame for "how math has always worked" is worth stating plainly because the rest of the talk is about what breaks when you remove pieces of it. Small groups of PhD-trained specialists, working with a high baseline of mutual trust — you don't want to review garbage, so you trust your collaborators to have already checked their own work.
The part I hadn't thought about before is his distinction between explicit and implicit goals. The explicit goal of a research project is the thing you write on the grant application: solve this conjecture, find a new proof of that theorem. But every project also carries a bundle of implicit goals nobody writes down — connect the result to prior literature, develop techniques reusable elsewhere, map out which adjacent questions are natural and which aren't, build a narrative around isolated results, and, not incidentally, train the humans doing the work to become better mathematicians.
The danger, as Tao lays it out, is that we've suddenly gotten very good at the explicit goals and not the implicit ones. Modern AI can generate a correct proof of something, and you can even push it through a formalizer so you know it's correct — but it won't cite its influences, it presents the routine parts of an argument with the same weight as the hard parts (often more), it doesn't suggest future directions the way a human who struggled with the same problem would, and the person who typed the prompt doesn't necessarily get any better at math from having done so.
Proof abundance, and the "traffic jam" analogy
Journals are already reporting a flood of AI-generated submissions. Tao says it plainly: he gets an unmanageable volume of math documents by email now, and the frustrating part isn't that the proofs are wrong — many are technically correct and technically novel. They just aren't digested.
Formal verification helps with triage — you can at least filter by "has this been machine-checked" — but correctness was never the only thing a referee does. A referee also validates how a result connects to the literature, whether it's interesting, whether it's well-organized. Handing that whole job to an AI referee is risky in an obvious way: the instant you make "passing the AI referee" a hard gate, people start prompt-injecting white text into PDFs to game it.
His analogy for the moment: our math infrastructure is a 19th-century street grid, built for pedestrians and horses, and cars just got invented. The cars are getting bigger and more powerful, but dropping them onto the same streets just produces worse traffic jams. The fix isn't fewer cars — it's designing new lanes, junctions, and rules that let slow deliberative human mathematics and fast machine-assisted mathematics coexist without each blocking the other.
Polymath as a proof of concept — and why it stalled
To ground this in something concrete, Tao walks through the Polymath Projects Tim Gowers started roughly 10–15 years ago — crowdsourced attempts to solve hard problems by farming them out to dozens or hundreds of volunteers rather than one or two experts.
The part I found genuinely useful: Polymath worked when a problem had a specific shape. A single legible metric to drive down (a number, not an abstract "is this true"), modular decomposability (you can specialize on one piece and feed results back), tolerance for partial progress rather than binary success/fail, and enough diversity of possible approaches that no one person could hold all the relevant tricks.
The canonical example is the bounded-gaps-between-primes project after Yitang Zhang's breakthrough: his original bound was 70 million, and Polymath drove it down to 246 over about six months of distributed, incremental improvement.
Polymath also had a side effect nobody optimized for: it made the process of mathematics visible — the dead ends, the false starts, all the stuff a published paper conceals. Grad students in particular valued being able to see that failure is universal, not just their own.
But the workflow didn't scale, and Tao is direct about why: it required one human moderator tracking dozens of comments a day, summarizing state by hand, with nothing like GitHub or Lean to do it for you. That's basically why you don't see many active Polymath projects today — modern formalization projects inherited the crowdsourced spirit (blueprints that decompose a big proof into little claimable pieces, with a graphic of colored bubbles turning green as each piece lands) but run on GitHub and Zulip instead of blogs and wikis.
Autoformalization reproduces the same traffic jam, one level up
Here's the turn in the talk that I think is the real thesis: pointing a large AI agent at one of these modular formalization projects doesn't solve the scaling problem — it reproduces it in a new form. An agent will hand you a 10,000-line Lean proof of theorem one, and a separate 10,000-line proof of theorem two, with none of the shared-lemma structure a human would naturally factor out, because factoring costs the human effort they're incentivized to avoid, and the AI has no such incentive. If the AI gets stuck, it doesn't post to Zulip asking for help — it just keeps looping. The collaborative tooling that made modern formalization projects work was built for humans, not for AI agents, and that mismatch is now the bottleneck.
Tao's tentative resolution is to split into two tracks. One track where formalization is the entire goal — you don't care if the proof is 100,000 unmaintainable lines, you just want the check-mark. And a second track where you actually want elegant, integrated, reusable proofs, community expertise, and maintainable structure — and that track, he thinks, still has to run on the older (his word: "2023-era") crowdsourced model, with AI doing narrow, well-scoped tasks like proving routine lemmas.
But splitting the tracks creates a new problem: an incentive gap. Volunteer formalization projects have always run partly on the cachet of being first to formalize something. If an AI tool can spit out a low-quality version of the same theorem instantly, the "first" prize is gone, and the incentive to do the careful, maintainable version goes with it. Tao says this is already happening in projects he runs personally — he's had to start writing detailed style guides and submission rules for pull requests, something he never needed before.
Erdős problems: proof indigestion, in numbers
The clearest illustration in the talk is the Erdős problems. Tao's slide gives the count: 1,217 problems in the database, of which 529 (43%) have been solved.
Tao shows a graph tracking solved-problem counts: back in September, roughly 350 problems solved; now around 550. A second line tracks how many of those solutions have been formalized in Lean — with autoformalization, that count has jumped from a handful to hundreds.
And yet there's now a backlog: dozens of Erdős problems where someone has posted "I used an AI, got a proof, but I don't understand it — can someone else check?", followed by someone else running it through another AI and formalizing it in Lean, also without understanding it, followed by the proof sitting in limbo until an actual domain expert eventually looks, identifies which techniques are being combined and why, and only then does it get accepted. Tao's working definition of "digested": someone can give a talk about the proof and field follow-up questions about the key idea. That didn't used to need stating explicitly — of course the person who solved a problem could talk about it. Now we can solve problems we can't explain, which he calls a "very weird situation to be in."
He closes this section with a line from Thurston: the goal of mathematics isn't to meet some abstract production quota of theorems, but to help people understand and think more clearly.
A live example: the Inverse Galois Challenge
Tao then walks through a concrete project he's involved in — a joint effort between the SAIR Foundation and the LMFDB (the L-functions and modular forms database) — as an example of a workflow designed to absorb heavy AI use rather than fight it.
Quick refresher: every degree-n polynomial has a Galois group, a transitive permutation group on its n roots. Going from polynomial to Galois group is easy — feed it to Magma, Pari, or Sage. The inverse direction — given a transitive group, find a polynomial with that Galois group — is unsolved in general. It's known up to degree 22. At degree 23, there's exactly one open case, the Mathieu group M23. Tao's project skips that famous open problem and attacks degree 24 instead, where there are roughly 25,000 transitive permutation groups on 24 elements (permutation groups acting on 24 objects, not groups of order 24, which would mean something different), and — prior to the competition — the LMFDB only had polynomials for 286 of them, about 1%.
The framing is an Easter-egg hunt: every polynomial you submit gets tagged with which of the 25,000 "patterns" (Galois groups) it hits, and the game is collecting one egg per pattern, where some patterns are extremely common (S24 falls out of almost any random polynomial) and some are vanishingly rare.
About 180 teams are currently in a blind competitive phase, submitting polynomials to a verifier that reveals only a discriminant and some signature data, not the polynomial itself. The scoring rule is the interesting design choice: if you're the sole team to find a given Galois group, you get a full point; if K teams have found the same group, everyone gets 1/2^K, not 1/K — a deliberately steep penalty for redundancy that uses the competition itself to reveal which groups are hard, since the organizers didn't actually know in advance and their prior guesses turned out wrong.
A screenshot from a week earlier showed 804 of the roughly 25,000 groups still uncovered, with 24,117 already matched to an explicit polynomial; Tao noted the live count had since dropped to about 390. In August, the blind competitive phase ends — Stage 1 runs June 16 to August 15 — and gives way to a collaborative, Polymath-style phase where teams share techniques openly to mop up the hardest remaining holdouts.
Closing frame and Q&A
Tao's summary line: we're moving from an era of proof scarcity to proof abundance — from "proofs are precious because they're hard to get" to "we have too many proofs and must choose which to engage with," which he compares to moving from food scarcity to food abundance: you no longer have to eat everything on your plate. The practical ask is to explicitly segregate which workflows stay human-centric (and deliberately AI-limited) versus which are redesigned from scratch to absorb AI at scale — and to stop rewarding "first to solve" as a proxy for everything else we actually care about, replacing it with real credit for digestion and exposition.
The Q&A ranged widely. On whether AI/formalization can help the existing refereeing crisis: Tao thinks certificated correctness (via Lean or otherwise) can shift referee effort toward judging impact rather than checking correctness by hand, but stresses it's "not a complete panacea" — one layer among several, requiring a lot of experimentation with new journals and editorial models, some of which will fail. Asked about formalizing the notion of a "stable" proof — one that can answer follow-up questions reliably — Tao floated the idea of the "AI complexity" of a proof: the size of the smallest prompt that reliably reconstructs it, suggesting that for AI-generated results, the prompt itself might become the artifact worth preserving, more than the proof text. Pressed by Melanie Matchett Wood on concrete incentive fixes — what journal editorial boards or hiring committees could actually do — his answers were modest: give referees explicit rubrics (we currently just tell people "check if it's correct and interesting" with no more guidance than that), and start having open panels about what "good mathematics" actually means, since right now that's transmitted privately, mentor to student, rather than discussed as a field.
The last question drew out a distinction I liked: proof by exhaustive search or counterexample (the classic one-line refutation of an Euler conjecture — "I searched on my computer and found this number") feels different from a constructed proof, and AI is disproportionately good at the former. Tao's answer reframes this as a difficulty-calibration problem: we've historically measured problem difficulty along one axis (how hard is this for a human), and AI search is revealing a second axis entirely — problems solvable by cycling cheaply through many low-probability-of-success techniques. He expects a genuinely uncomfortable stretch where many problems we assumed were hard turn out not to be, before things stabilize around a residue of problems that are hard along both axes. "If you view current progress through a one-dimensional difficulty lens, it looks very disturbing. But the situation is more nuanced — we just can't see it yet, exactly what's going on."