This is the panel where, partway into an abstract question about how mathematical knowledge is currently structured, one panelist mentions — almost as an aside — that a new formalized-math library was released the day before, and then spends the rest of the session fielding live cross-examination about it from the moderator, the rest of the panel, and the audience. That's unusual for a panel, and it's the spine the whole session ends up organized around.
Patrick Shafto, who introduces the session, is a professor of math and computer science at Rutgers, Newark, currently on loan to DARPA where he runs what he calls the exponentiating mathematics program. He frames the shift in emphasis for the afternoon — more panels, fewer straight talks, because the interesting questions now concern new kinds of problems and new connections to other fields, not just solving old ones faster — and hands off to the panel: Andrea Ferrari from the University of Cambridge, joining virtually; Benjy Firester from MIT; Xinze Li from the University of Toronto; and Kim Morrison from the Lean FRO. The moderator is Lauren Williams, the Dwight Parker Robinson Professor of Mathematics at Harvard and a researcher in algebraic and geometric combinatorics.
Four backgrounds, one shared question
Andrea Ferrari describes himself as a theoretical physicist working at the intersection of quantum field theory and pure mathematics — representation theory, vertex algebras — who has also used AI and machine-learning tools to automate the discovery of dualities and symmetries in physics at Cambridge. He's since enrolled in an AI safety fellowship supported by Principles of Intelligence, an AI-safety research organization.
Benjy Firester is a graduate student at MIT in geometric analysis — Calabi-Yau metrics, optimal transport, PDEs tied to geometry — whose recent interest in formalization centers on separating what's created by humans from what's created by AI. Kim Morrison, by his own account, has "gone over to the dark side": trained in quantum topology and operator algebras, he now works at the Lean FRO on automation — "good old-fashioned AI before the large language model world of things," meaning hand-written tactics — and has been a Mathlib maintainer "since day zero". Xinze Li is a graduate student at Toronto in min-max theory and geometric measure theory, and opens with an image she returns to later: a PhD used to be like growing a flower in a garden, but she started hers just as AI arrived — "in the beginning, I just have a little piece of grass, and then AI comes".
How mathematical knowledge is stratified today
Lauren Williams opens with the panel's title question directly: how is mathematical knowledge currently structured in the age of formalization? Kim Morrison answers with a taxonomy: formalization artifacts split into libraries, topic-focused projects, and textbook-formalization projects. Mathlib is the example of the first kind — a single massive, coherent library that avoids duplication and, historically, doubled as the place where the Lean community worked out what was even possible to formalize: "of course, we didn't have AIs then, but it wasn't even clear that it was possible to take some pieces of mathematics and turn them into formal mathematics".
Topic-focused projects split again into two kinds: those pushing the frontier of what's formalizable when the informal mathematics is already well understood, and those doing genuinely new mathematics at the same time as formalizing it — a category that "barely exists" but is just starting to be real. The first kind has a lineage: the four-color theorem, the Flyspeck conjecture, the sphere eversion project, the Liquid Tensor Experiment, and the ongoing Fermat's Last Theorem formalization project. Kim's claim is that this era is ending: no subject matter is intrinsically immune to formalization anymore, and the real obstacle is just the translation work of getting prerequisites into Lean.
Then the numbers. Mathlib currently has, in his words, "1,000 contributors. It's almost, I think it's two million lines of code". It's bottlenecked by reviewer availability, part of why the Mathlib Initiative now pays people to review pull requests — "a whole new category of paid mathematical activity". Even that isn't keeping pace: Kim cites the Erdős unit distance conjecture, where someone formalized all the informal proof's prerequisites and produced, in his description, "a million lines of Lean code as just some engineer at OpenAI that went and did this in his weekends" — a scale equal to half of Mathlib, which took ten years and a thousand people to build. His extrapolation: 100 million lines of Lean code before long, and the open problem is avoiding "a thousand little spiky towers" instead of something coherent.
What makes a theorem matter
Benjy Firester adds a structural argument for why this matters beyond code volume. Once formalized systems exist at scale, you can put a metric on them and ask which results are structurally important — a question mathematicians face constantly ("there are so many things to explore, how do you choose what's interesting to you?") but rarely quantify. His analogy: graphs with constant expansion can be represented as spaces with negative curvature, where the boundary quickly outgrows the interior — the point being that in any sufficiently rich system, human or AI-run, there's always more to explore than resources to explore it, and formalized systems let you actually quantify that rather than just feel it.
Pressed for specifics, Benjy says this is something he's recently started working on with collaborators including Xinze Li, on the panel, and Andrea. The substance: two kinds of theorems matter most. A "bridge" unifies two things that were far apart, letting techniques transfer between them; "opening up a new island" is a definition or technique whose boundary of easily reachable consequences is unusually large, with complex analysis and holomorphic functions as the example of a small set of ideas opening onto a huge, previously disconnected territory.
Xinze Li follows up, describing a project with Benjy where they moved away from writing a paper "line by line" and instead treated LaTeX as a kind of code, managed in a repository with an AI-native workflow — something she says visibly improved their productivity. She then pivots to a specific ask: most mathematical knowledge is still organized as arXiv or PDF papers cross-referencing each other, and formalization projects address this with blueprints — does Kim's new project have a faster or more informative way of building them?
The reveal: a library named after a nearby star
Kim's answer is the centerpiece of the session. He had teased it at the end of his opening answer — a new library "released yesterday" — and now backs up to explain what it is: it's called Tau Ceti, and, in an aside, he notes the name also belongs to "a star that's not so far from our own. It's the nearest sun-like star, about 12 light years away".
The project: a coordinated library of mathematics that doesn't try to match all of Mathlib's goals, but focuses on producing reusable material others can build on top of reliably. It's far more AI-driven than any mono-repo to date — humans write roadmaps and natural-language blueprints, but the pull requests and reviews are done by AI against a set of open rubrics, "adversarially reviewed by other AIs". Lauren's clarifying question nails the relationship: Tau Ceti is like Mathlib but far more automated. Kim's answer: it lives downstream of Mathlib — Mathlib is a dependency, and Tau Ceti occupies the complement of what Mathlib already covers. If Mathlib later absorbs a domain already in Tau Ceti, the plan is to delete it there and re-point downstream dependencies at the Mathlib version. His stated hope is thousands of merged pull requests a day. It's already "shovel ready," with QR-coded cards at the meeting that fit two command lines and, given a subscription account or frontier model, will start making PRs immediately — though you can bring your own tooling and models.
He draws the historical parallel behind the design: Mathlib's high bar for coherence has always pushed people to work outside it on faster, experimental projects, with reusable pieces migrating back via pull request — his example being the homological algebra library, whose first version he wrote ("the lame and badly written version"), later rewritten by the Liquid Tensor Experiment and merged back into Mathlib. What's missing, he says, is the equivalent feedback loop for the new wave of AI-driven projects going off in a thousand directions at once — the corner Tau Ceti is meant to fill, ideally without requiring humans to work in it directly; the aspiration is that people doing their own AI-assisted projects tell their AIs to PR the reusable parts back up to Tau Ceti.
Who bears the cost when Mathlib changes underneath you
Lauren pushes on mechanics: if Tau Ceti becomes a hundred times the size of Mathlib and a breaking change ripples through, who pays to fix things? Kim's honest answer: "that remains to be seen." There's already an automatic process — the commit log shows regular PRs bumping the Mathlib dependency to new daily releases, some requiring real refactoring — currently running on a "completely shoestring budget," after Jesse Han earlier "outed" him for running multiple personal Claude Max and Codex Max accounts. His longer-term hope: significant contributors pay their own way, donating money or compute tokens or running their own review agents, with tooling already built into Tau Ceti for comparing review models against each other. He also credits the separate Mathlib Initiative with building general tooling for this class of problem — automatic downstream fixes triggered by breaking changes, with deprecation labels as the simplest example.
Asked how to point Tau Ceti at a specific area of mathematics, Kim explains the system is entirely roadmap-driven: every reviewer agent checks whether a PR points at a specific item in an existing roadmap in a separate repository called Tau Ceti Roadmaps, rejecting anything that doesn't. To request a new area, write your own roadmap there; get one approved and you can approve others'.
As of the panel there were, in his words, "13, 14 roadmaps written already," with another 10 or so in pull-request form — "let's have 100 next week". He's unbothered that the roadmaps show visible signs of LLM authorship, provided a human has read them; his example is a representation-theory roadmap he built by telling Anthropic's Claude Fable agent to read twelve graduate-level representation theory textbooks and distill them into a roadmap, which he says did "a pretty good job".
A later audience question adds one more piece of the map: the ecosystem runs across four repositories, not two. Alongside the three main ones — the core Tau Ceti library, its Roadmaps repo, and the repo where agents push their work — Kim names a fourth, Tau Ceti Worker, containing a sample harness for interacting with the pieces.
What changes for the people doing the math
Lauren broadens the question: how will AI change the structure of knowledge and the standard pipeline of producing it? Xinze Li returns to her flower image with a twist: previously, a mathematician's tools were pen, paper, blackboard, and chalk, and "finishing" a piece of work was really a social bar — two collaborators agreeing they'd solved what they set out to solve. Each paper was a flower whose root wasn't very deep, so the infrastructure to grow it was simple. Formalization projects like Mathlib and Tau Ceti need a much deeper pipeline, and she describes feeling, after first getting AI access, "so ambitious" about both mathematical problems and software products that the field now needs to consciously set working boundaries and protect its energy for what matters.
Benjy Firester frames it as continuity plus addition: pure research driven by curiosity won't change, and mathematics developed to solve concrete practical problems will keep emerging and getting solved — what's new is a layer of non-expert AI users, and the open question of how to compare the human-made corpus of mathematics against an AI-generated one to decide resource allocation.
Andrea Ferrari takes the discussion toward incentives: AI and formalization together will reshape reward systems — how formalizers get credited, how AI systems and their builders are rewarded — and pressure standard PhD-level projects if AI can solve them quickly. He calls for broader discussion of how to "normalize the existence of these new tools and new players in the form of private companies," framing the socioeconomic question of how mathematical knowledge production and distribution will work as one we should be asking now. Asked how this has changed his advising, he says he now encourages students to get comfortable with cutting-edge models and hands them problems near the frontier of what those models can do, so they stay "morally speaking, at the cutting edge." Blunter about the cost: there are papers he wrote with students he "would not suggest as projects anymore," since the same result might now come from feeding the setup into an LLM. The level and style of problems he assigns has shifted — "not dramatically, but slightly".
No plan, and that's the plan
A Slido question asks whether there's an actual strategy for which topics go into Mathlib versus Tau Ceti. Kim's answer is flatly no: Mathlib has never worked from a plan, growing wherever contributors wanted to take it, and he doesn't want to be prescriptive about Tau Ceti either. His hope is that Tau Ceti can quickly build foundations in areas "almost entirely missing" from Mathlib because of historical accidents of contributor interest, and he invites anyone from an underrepresented field to write the roadmap that gets it in — "you haven't missed your chance". Low-dimensional topology and PDEs are named as underrepresented, and he points to a coming meeting at SLMath — the Simons Laufer Mathematical Sciences Institute in Berkeley (formerly MSRI) — in November on formalizing PDEs, adding dryly that it'll take fifty such conferences to fill in the whole map.
Will this actually change how mathematics is done
A second general question: will AI and formalization lead to a fundamentally different way of doing mathematics? Andrea takes it first and is measured: human-curated mathematics is driven by our interaction with the world and what we find beautiful, and that won't change; what will change is the speed at which things get proved. The harder problem is recognition — if "numberless agents" produce mathematical knowledge at superhuman scale, how do we recognize what's important or deep in a landscape humans haven't curated? He suggests this is already studyable using existing human-curated mathematics as a dataset — including, he says, the discussions of how humans converge on which statements matter that play out on the Lean community's Zulip chat.
The last few minutes: visual proofs, a fourth repo, and a pushback
With time short, Lauren opens the floor. The first question asks whether the panel is thinking beyond strict formalization toward less formal but still valuable ways of conveying mathematics — visual proofs, thinking of Mirzakhani's drawings of hyperbolic surfaces, which "obviously" aren't complete proofs but convey understanding a formal translation can lose. Kim answers with a Lean FRO project called Verso, "just a LaTeX killer" — a markup language fully integrated with Lean that produces typeset documents linking or embedding Lean code, generates documents directly from Lean code (Lean, he notes, is a genuinely pleasant general-purpose programming language, not just a theorem prover), and is expected to support Lean-native computer algebra in the spirit of Mathematica or Maple, feeding the same underlying mathematics into animations and diagrams.
The next audience member, after praising the project, says they'd understood Tau Ceti to span two repositories — one for roadmaps, one where agents push finished work — and suggests a third for harnesses that help write roadmaps. This is where Kim reveals the fourth repository, Tau Ceti Worker, mentioned above.
The final exchange is a real disagreement, with an audience member introduced only as "Adam" pushing back on deleting material from Tau Ceti once a better version lands in Mathlib: if a contributor makes something, he argues, it should just stay there — the incentive to contribute depends on it. Kim holds his ground on the technical point — duplication should be intentional, not accidental, and the Mathlib version will simply be better-made — while conceding the incentive question is worth thinking about; someone off-mic notes deleted material still lives on in the GitHub history, where the exchange settles. Lauren calls it there — "this seems like a great place to wrap" — and the room breaks, the Tau Ceti conversation clearly still going in the hallway.