Day two opens with the same logistics-then-handoff rhythm as day one — a reminder about Slido, Pat Shafto framing the day as "leaning forward" toward futures the community actually wants rather than ones it backs into — and then Andrew Blumberg, professor of math and computer science at Columbia, working in algebraic topology and homotopy theory, plus geometric data analysis on genomic data and verifiable outsourced computation in computer security. He's also part of the "First Proof" project assessing frontier LLMs on natural-language mathematical proof (not formalization) — a project he flags as adjacent to, but distinct from, the day's main subject.
His talk is explicitly structured in three tiers, ordered by how confident he is: background requirements (preconditions he's sure are coming), near-term future impact (things extrapolated from what's already visible), and science fiction (a deliberately speculative medium-term vision). He's upfront that predicting more than a year or two out is hard "especially in this context," that he's mostly synthesizing what's already in the air rather than claiming novelty, and that if you vehemently disagree with some of it, he's done his job.
Background requirement: formalization needs a trust infrastructure
The frame here: formalizing things is supposed to remove the need for trust, and yet trust shows up at every layer anyway. You have to trust the kernel — "these things are compilers, and that compiler had better be right." You have to trust the specification, which is the alignment problem already raised earlier in the meeting: a formalization can compile cleanly in Lean and still not formalize the statement you meant. Blumberg cites this directly from his own First Proof project — submissions that were "correct as far as they compiled in Lean" but didn't formalize the intended problem, sometimes close, sometimes "totally crazy," and not obvious to non-Lean-experts even when Lean experts could tell with effort. And you have to trust the libraries of proofs you build on — echoing the review-bottleneck discussion around Mathlib from the day before, plus a harder question: if there are 17 competing proofs of something, which do you trust? Proofs, he argues, may not all be fungible.
The reason this is hard: incentives aren't aligned across the actors involved. Academic mathematicians mostly are — "I don't think Brendan's out there sending in adversarial papers" — and math's culture of correctness rests partly on a reputation system where bad-faith submissions get caught and the submitter's credibility burns. First Proof surfaced a live example: one (unnamed) company submitted 17 iterations of a proof, the first 16 wrong, each requiring a human to check and reject — behavior that would sink a mathematician's reputation if repeated in journal submissions, but has no equivalent cost yet in an anonymized, high-volume, AI-generated-proof world. Beyond individual researchers, there's private enterprise (which sells "correctness certification" as a product and doesn't always care whether it's true), state actors, and outright bad actors — plus a fifth category on his slide simply labeled AI, covering "all of the above" and flagged as possibly indifferent to actual correctness. It's under that AI bullet, specifically, that a term new to me appears: adversarial proofs — proofs that exploit real bugs in the Lean compiler to compile successfully without actually proving the intended statement, often by smuggling in contradictory axioms and deducing anything from the contradiction — and which tend to be shorter than honest proofs, which is exactly the wrong incentive gradient for an AI system optimizing for brevity.
His analogy for how to build the fix: computer security did this already. Decades of cryptographic infrastructure, a "robust community of public, private, and governmental entities," NIST recommending elliptic curves and running cipher contests, a private industry of security providers, red teams paid to break things. Formalization is going to need the equivalent.
A second requirement: formalization has to come with interpretability
Blumberg calls this "interpretable formalization" and admits he doesn't have a crisp definition, but insists on the property: a wall of machine-verified 1s and 0s ("the Riemann hypothesis, that one's true — so what?") isn't what anyone actually wants from mathematics. He ties this explicitly back to Tao's "digestibility" framing and Ono's talk about extracting ideas out of a formalized proof, and states his own bias plainly: mathematics and science are a human enterprise whose goal is human understanding — "a religious view," in his words, that he's going to stick with regardless of where the technology goes.
Near-term: applied science as the easy target
Assuming the trust infrastructure exists, where does formalization land first outside core mathematics? His answer: applied domains where the underlying math is comparatively simple and arguments are shorter — "there's just less math in population biology than there is in algebraic geometry" — so formalizing proofs that already underpin applied results should be tractable soon. A second motivating point: mathematics' hundreds-of-years-old culture of correctness makes it an unusually good benchmark domain for testing whether LLMs are actually reliable, a standard many other fields lack (sometimes for good reasons, sometimes not). Concretely: mathematical economics (already underway, citing Scott Duke Kominers' EconLib work from the prior day), hardware verification and SMT solvers in engineering (already a mature culture, a natural fit), genomics (whose mathematical foundations are trusted but never actually checked), and computer security (already living in formal-methods land).
But formalizing theorems is only half of it — he separates out formalizing computation: proving not just that an algorithm is the right one, but that a specific run of it on specific data produced the claimed output. He makes this concrete from his own field: genomics runs on code written by graduate students "under conditions of extreme pressure" who then leave and can't be reached to fix bugs — exactly the kind of legacy pipeline that verified refactoring and verified execution (not merely unit tests) could fix. Also on the table: verifying that numerical preprocessing was applied correctly (data provenance), outsourced verifiable computation (proving an untrusted cloud actually ran what you asked without re-running it yourself), and verifying that a statistical test's assumptions actually held before applying it — "usually doesn't," he notes dryly, on how often that check is skipped today.
He grounds the cost of this with a war story from his own subfield, verifiable outsourced computation: the PCP theorem (proofs can be checked probabilistically by looking at only a tiny number of bits) is, unrolled via Cook's theorem into an arithmetic formula for something as pedestrian as multiplying 100×100 matrices, a formula with more variables than there are atoms in the universe, using the textbook construction. His field's whole existence has been shaving that overhead down toward something like 10⁵–10⁶ — "every paper for a while had two orders of magnitude improvement... but then it's like, yeah, it went from 10 to the 30 to 10 to the 28." (These figures were spoken asides; the slide on screen was the "Payoffs" slide below.) The lesson generalizes: formalization overhead is a real, recurring cost, and we don't yet have good ways to formalize programs — control flow and stacks remain hard.
Science fiction: formalizing contact with the physical world
The most speculative tier is about formalizing the integration of math and algorithm with the physical world — instrumentation, robotics, experimental protocol — not just proofs on paper. He frames the ambition with a line from The Departed ("I don't want to be a product of my environment, I want my environment to be a product of me") and references a remark Carina Hong (Axiom Math) made on the previous day's panel that formalization is "on the road to AGI," reinterpreting it as: verifiable, predictable interaction with the physical world might be a precondition for that road, not just a slogan.
Concretely, this means formalizing experimental protocol and data collection — a camera that produces a cryptographic proof it took a specific picture of the sky at a specific time, a motor that proves how far it actually turned — and formalizing "scientific hygiene": proof that you didn't peek at data before forming your hypothesis, that causal-inference assumptions actually held. He's candid that this is hard and has failed before: he worked at the MIT AI Lab years ago among people trying exactly this kind of formalization "without a tremendous amount of success," while "the clowns doing neural networks down the hall... are laughing all the way to the bank" — a joke very much aimed at his own younger self's confidence about which approach would win.
His extended example is C. elegans neuroscience: worms with ~300 neurons, fully genetically determined and symmetric enough that you only need to record half, whose behavior researchers still can't explain beyond the input (eye) and output (motor) neuron layers — "and this is kind of true for people too, but with people there's an excuse." A cutting-edge project he was part of recorded 16 worms for four minutes each; two "went insane" mid-experiment and produced unusable data (a precise technical term here — moving toward stimuli they should find aversive), leaving 14 usable runs, because each run needs a ten-person team and neither federal nor private funding pays for generating thousands of such data points. No computer vision, no ML, no AI tooling compresses the analysis stage at all yet.
He draws the DARPA Grand Challenge analogy directly: the 2005 self-driving desert run looked like robotaxis were two years away; twenty years later Waymo can operate on LA's flatlands but still can't handle the hills, not for regulatory reasons but because the actual driving problem there is unsolved — "robotics is harder and progress is slower." His bet: even mediocre robot-collected data, at 100× the volume, processed with modern signal processing and ML, could match what a smaller set of careful, expensive, human-collected data gives you today — with the added benefit that all of it could be formally verified for provenance.
He tempers the science fiction with a counter-example from drug discovery (a talk he heard from someone at Regeneron): AI hasn't sped up drug discovery as much as expected because, after AI helps predict binding, you still have to physically synthesize enough compound to form a droplet and test it — and "if that droplet has the consistency of honey, when I inject it into my arm, I'll die," a step nobody can predict from molecular structure alone, costing roughly a month and $10 million per attempt. Failed attempts stay locked inside companies hoping a competitor repeats the same expensive mistake, so there's no shared training data for the physical step itself. "This does not change the laws of physics" is his summary line — the frontier for formalizing physical-world contact is real, but narrower than the fully Panglossian version.
Conclusions and Q&A
His stated conclusions: formalization needs a trust infrastructure to matter for science, and this seems already underway; "formalization without interpretability is not science" (his stated religious view); formalization of math and computation will likely accelerate science productively for human flourishing; and he's genuinely anxious about training the next generation of scientists — not anxious about the tools, but about the fact that you can't use any tool responsibly if you don't understand the mathematics underneath it, the same way an MIT mentor once told him you need to know what the electrons are doing to really understand what a compiler is doing. His closing line: the next real transformation is formalization of scientific process integrated with the physical world, however that ends up looking.
The Q&A ran long and touched several threads. Asked to draw a line for "interpretability," he leans on Justice Stewart's "you know it when you see it," extending Tao's "no one's ready to give a talk on this proof" point to the four-color theorem as his own example of a result he believes but gets no insight from — and predicts the standard for "enough explanation" will always vary by field and by person. Asked about bottlenecks in a 3–5-year science-fiction timeline, his answer centers on low-level infrastructure — what a verified hardware stack even means and who builds it — rather than higher-level specification concerns. A researcher running ~40 postdocs raised a sharper worry: a "perfect storm" where the brightest postdocs are being pulled out of academic pipelines into hedge-fund offers, driven partly by distrust in how science is currently funded and treated by government — Blumberg agrees "100%," predicts "a rough period for the next couple of years" before things reach some equilibrium, and reaches for an analogy from his own Manhattan neighborhood's industrial scars: a transition can be net-good in the long run and still be genuinely brutal for the people living through the ten-year span in the middle of it.
On whether new fields need entirely new formalization tooling versus extending Lean: he defers ("I don't actually work in formalization most of the time") but relays a point he credits to Emily Riehl — that a plausible future has multiple competing formalization ecosystems side by side, because some geometry and topology is currently much easier to state in homotopy type theory than in Lean, for reasons that may just be Lean's dependency stack not yet reaching deep enough into that territory. On trust and standards across open- and closed-source AI systems, he again reaches for the computer-security analogy — NIST's elliptic-curve recommendations, and the historical suspicion that government influence shaped which curves got recommended — and floats, uncertainly, a future with something like "a NIST-standardized Lean kernel," or possibly the opposite, an open-source-only equilibrium; he doesn't resolve which. Pressed on why he's optimistic about verifying physical robotics at all, given that sensors can't cover the whole state space, his answer scales the ambition down explicitly: not "verify all of physical space," but verify specific invariants — "I can say something about what the gyroscope did while it was doing it" — the same modest ambition already at work in verified software, where formal-methods people mostly prove properties and invariants of programs, "but no one really proves that a program's correct, even in cases where we could."
The last question, from an audience member who introduced themselves as coming from an open-learning/MOOC background, asked about bridging formalized mathematics with mass, citizen-scale math education — "reaching a billion learners." Blumberg's answer reaches for two personal anecdotes instead of a technical claim: Ulysses Grant's memoir describing borrowing his father's horse to ride to the only town selling an algebra textbook, and his own childhood memory of combing used bookstores near Harvard and MIT hoping to find a copy of Strang's Linear Algebra. His hope, stated without much elaboration, is that open coursework already lets far more motivated people worldwide participate than access to physical books ever did, and that formalization tooling will extend that same effect rather than gatekeep it further.