The panel is Stella Biderman (EleutherAI), Alexander Hicks (Ethereum Foundation), Jared Duker Lichtman (Stanford), and Bernie Wang (NTT Data AIVista), moderated by Ravi Vakil (Stanford, and president of the AMS). It shared no slides — the photos below are documentary shots of the room, and the projector carried only a Zoom gallery of the remote participants throughout. Since the transcript doesn't tag speakers, attribution is reconstructed from self-introductions, the moderator's calls, and each panelist's subject matter; a few turns I mark as best-guess.
Four introductions, four relationships to "infrastructure"
Vakil frames the session — introductions, then a discussion among the panel, then the floor opens to the audience and Slido.
Stella Biderman goes first. She runs EleutherAI, a non-profit specializing in large-scale open source AI; in 2021–2022 it trained what were, at the time, the most powerful open source language models in the world, aimed at researchers doing science with and on AI systems. That scale of training now costs more than EleutherAI's annual budget, so the organization has shifted toward research it's excited about while maintaining "a meaningful fraction" of the widely used open source AI ecosystem — and, most relevant here, doing work funded by Renaissance Philanthropy on formal verification, auditing, auto-formalization, and AI theorem-proving pipelines.
Bernie Wang introduces himself next: currently a member of technical staff and distinguished scientist at NTT Data AIVista, previously a principal scientist at AWS and Amazon for nearly 13 years. He's explicit that he isn't a mathematician by training ("I managed to do a couple of papers in applied mathematics") and that his work has been building ML systems for supply chain optimization, resource allocation, capacity planning, and recommendation systems. More recently he's focused on open source software that automates ML systems at scale — the most popular being AutoGluon, the AutoML toolkit that came out of his AWS work — plus open-weight foundation models for tabular and time-series prediction, one of which, Chronos, recently surpassed one billion downloads on Hugging Face. He closes with a self-deprecating bit about asking ChatGPT what to talk about and being told to "stay in your swimming lane", to which Biderman replies that she also lacks a graduate math degree and was recently "overjoyed" to learn she'd been cited in a math paper because of a Stack Overflow post.
Alexander Hicks leads program verification at the Ethereum Foundation, where the group formally verifies across the entire stack — RISC-V assembly, cryptography, distributed systems. They maintain five libraries touching formalized cryptography, from polynomial functors down to zero-knowledge proofs; he mentions prize money attached to some of the conjectures involved and frames the goal as eventually covering "essentially all of cryptography".
Jared Duker Lichtman is a Szegő Assistant Professor at Stanford, trained as a number theorist. Over roughly the past year, he says, it's become clear that infrastructure, formal methods, and AI will matter increasingly not just to his field but to all of mathematics — citing recent solutions to Erdős problems and, "even this past week," a solution to the Jacobian conjecture in algebraic geometry. He credits Pat Shafto (the meeting's organizer) for convening events like this one, and mentions having appeared with Vakil on a panel at a recent Stanford conference on the future of mathematics.
What worked before: arXiv, Mathlib, CERN, and NetworkX
Vakil's first substantive question: examples of successful human-built mathematical infrastructure from the past, and what made them work.
The first answer (Hicks) names arXiv: openness, and making it easy both to publish and to access knowledge, was a "huge boost," with real uptake from non-professional mathematicians who read but don't publish pure math and build downstream software — in finance, cryptography, physics, engineering — that depends on it. He then calls Mathlib "an incredible example of core knowledge infrastructure that everyone can use," noting that the five or six libraries his team maintains all import Mathlib and "none of them would be possible without" it.
Vakil calls on Lichtman, who reaches outside mathematics: the LHC at CERN in physics, and the Human Genome Project in computational biology — both central resources built for a long-horizon project that ends up serving the public good.
Wang picks up with NetworkX, the graph-theory library, as a boon to applied graph theory in domains like social-network analysis and epidemiology; he recalls it was ported between R and Python but can't remember which direction.
Why it worked: openness, consensus, and "moral authority"
Vakil follows up: which characteristics of those successes should guide what gets built next?
Wang points to open access — anyone can submit, everyone builds on the same codebase, pull requests get merged, and there's infrastructure to check submitted artifacts. Biderman agrees on openness but adds a second axis: consensus among experts, particularly where trust matters. If every cryptography expert wrote their own encryption library, she says, she wouldn't trust any of them; broad consensus on which libraries to rely on lets her use "the collective wisdom of cryptographers" without personally out-thinking nation-state adversaries. Her operative principle is "many eyes make all bugs shallow," especially for trust-critical things like the core of Lean itself.
Lichtman, "from the mathematician's hat," adds a recent example: about a year ago DeepMind released a list of formalized problem statements — not proofs — inviting third parties to fill them in, which he frames as setting both a standard and a shared vision of what the community wants proved.
Hicks gives the longest answer, built around "moral authority" — people with decades of experience in a niche branch of mathematics, who know all the ways of exposing that piece of math. When a library like Mathlib gets imported, you can trust you're getting a canonical formalization, with helpful lemmas well-integrated with the rest of the library. He contrasts this with Isabelle's Archive of Formal Proofs, which he finds comparatively poorly organized — duplicate formalizations, confusing usage. A subtler property: feeling safe using a library even in mathematics you don't personally understand. His example — the right way to model interactive protocols turned out to be a polynomial functor over the free monad, a piece of category theory none of his team knew until a PhD student surfaced it, and one Mathlib already had prior work on, letting them build rapidly instead of reading a textbook end to end. He adds maintenance guarantees (Mathlib ships a release alongside every Lean release) as underrated, and draws an industry parallel: formally verified cryptography libraries still cause bugs — not because the library code is wrong but because interfacing with it is hard. Packaging knowledge well, he argues, matters as much as what's proved.
Biderman urges the community to talk to library scientists sooner rather than later — something EleutherAI has been doing "as a matter of catch-up." One library it maintains — its LM evaluation harness, used by roughly 500 labs worldwide to evaluate large language models — is kept up by two people. Her recommendation: invest in scalability and interoperability before something becomes load-bearing, not after — prompting Vakil's aside that "the word load-bearing now has a different connotation".
Wang picks the thread back up, citing a point from the day before (he attributes it to Scott Kominers) that infrastructure needs an accompanying protocol or culture change to actually get used, alongside a question Dan Spielman had raised about every arXiv paper coming with a formalized code submission. His analogy: machine learning didn't always have a norm of submitting code with every paper, but over ~15 years that became the common — if not strictly required — protocol, and he expects something similar in mathematics, framing the effort as building toward a system that eventually makes everyone's job easier rather than as overhead.
Hicks returns to ease of contribution: libraries like his are "extremely live," version bumps move things around (in the sense of improving), and while the time to upstream to Mathlib is "maybe a bit long" right now, initiatives like scaling Mathlib — and the Tau Ceti library launched at the Day 1 panel — can help. He then makes a point about generality: Mathlib's tendency to state things very categorically can look like overkill to someone doing pen-and-paper math, but in practice it enables better tactics and automation. His live example: generalizing coding theory from linear codes to modules, done so that cryptography researchers can ask Claude to generalize their own papers accordingly, producing new lemmas that get proved "one-shot in Lean". He calls this "very exciting" and predicts it will lead to "very new exciting cryptography... by the end of the year".
Biderman adds a caveat: generalization isn't just about a theorem's statement but its proof — she's overheard two separate conversations where someone wanted a Mathlib theorem in a different context and the existing proof simply wasn't valid there. Lichtman closes with a "mathematical point": Mathlib's coverage reflects contributor preference (historically more category theory and algebra), which snowballs as more surface area makes further contribution there easier — though this doesn't preclude underrepresented areas from being built up over time.
Where pure and applied math actually diverge
Vakil, describing himself as "a pure mathematician... aware that I'm seeing things from [a] narrow point of view," asks how the needs of applied mathematics differ, and what formal mathematics can learn from applied math's longer history of infrastructure-building.
Hicks answers that the boundary is "actually kind of fuzzy" and getting fuzzier, using cryptography: a crypto paper describes a program and states purely mathematical properties of it, sitting between applied math, computer science, and — once formalized in Lean — pure math, since the underlying coding theory is applied while some associated conjectures are close to algebraic geometry, and the whole chain ties down to an executable program with computable polynomials. For his team there's "no distinction" anymore, which he considers a feature: it lets people rely safely on intuition about pure mathematics they don't fully understand.
Wang gives the panel's other extended technical answer, on numerical mathematics specifically. He argues it's a distinct case: an algorithm like conjugate gradient converges in exact arithmetic, and Lean could formalize that — you could even formalize the floating-point convergence behavior — but the boundary conditions, condition numbers, and practical behavior of an iterative solver aren't things you know without actually running the system. He calls this "very intrinsic to the compute fabric" of applied mathematics, an area where the numerical-software community has spent decades learning what the durable interface between library implementers and users looks like: the internals evolve for a long time, but the interface doesn't, and that stability is itself a form of infrastructure worth studying.
Biderman brings in an AI analogy: for years a subfield tried to explicitly build symmetries into neural networks, until people brought in mathematical machinery any math PhD learns in their first year and "completely revolutionized the field." She learned, from people involved before she became an AI researcher, that this mostly came down to sitting with people whose interests were more applied and translating their motivations into ideas already standard in pure mathematics — evidence, in her framing, that open lines of communication alone (not necessarily co-authored papers) can produce breakthroughs.
Hicks adds that even in an AI-heavy world, more people means more ideas — and describes concrete steps his team takes to make libraries "agent-friendly": an internal knowledge base and wiki, markdown summaries of papers targeted for formalization, and documented GitHub issues that let contributors of varying expertise point Claude Code or Codex at an issue and get a usable contribution. Biderman follows with her own version: spinning up fresh instances of Claude Code and Codex and pointing them at libraries she's worked on to see if they can implement an evaluation framework unassisted — sometimes it works, sometimes not — which she frames as a rapidly growing fraction of how code interacts with libraries going forward.
Getting concrete: three orders of magnitude in a year
Vakil pivots toward specifics: what infrastructure or ideas merit investment over the next few years, not blue-sky long term — inviting Slido questions alongside panel answers.
Lichtman opens with a "level set." A year ago there was very little auto-formalization — everything was manual, a slow and heroic effort by people, some in the audience. Over the past year, code-generation capacity has scaled rapidly: before, models could solve a competition problem worth a few hundred lines of Lean; more recently, in projects he's been involved with at Math, Inc., formalization efforts have reached tens of thousands and then hundreds of thousands of lines — a three-orders-of-magnitude scale-up in roughly a year, with "no wall" in sight. He projects two to three more orders of magnitude a year out, against the ~two-million-line figure cited for Mathlib itself — meaning libraries 100 to 1,000× Mathlib's current size are the scale the field should plan to interface with.
Hicks follows with concrete recommendations. First, smoother contribution integration: pointing a fresh Codex or Claude Code instance with limited context at a library far larger than its context window tends to produce duplicate definitions, misused interfaces, and style violations; a partial fix is internal wikis, maintained by agents for agents, that can be exhaustive precisely because a human won't read them but an agent will. Second, "100%" of incoming PRs for his team — he immediately revises to "maybe 99%" — are agent-generated, so a library should ship, on git clone, with a harness tailored to it. Third, and more structurally: better review infrastructure, because Mathlib, "incredible" as it is, has "kind of stalled" relative to the volume of contributions proposed versus what can be reviewed. AI-assisted review is "fairly sound with good enough harnessing" but struggles with completeness on very large PRs — he personally receives PRs of 60,000 lines, "sometimes multiple of them a day". His prescription: understand which parts of a library are foundational (kept rigorously safe) versus which can tolerate more noise, and recognize that in a big enough library, the marginal value of one more proved theorem is often lower than the value of a new set of `grind`-style automation tactics that makes existing and future proofs more maintainable. He wants a tool that can be pointed at ten files and asked to generate exactly that automation.
Hicks then pivots to public infrastructure beyond libraries, citing community-driven "auto research" as an emerging category.
His example: Google published a quantum-computing result "last month or two months ago" describing a more efficient circuit — fewer Toffoli gates — for breaking elliptic-curve cryptography, but published only a zero-knowledge proof that they knew such a circuit, not the circuit itself, which he calls "not open science... kind of shameful." A community effort, organized informally over Slack and Telegram and involving people with varying (non-quantum-expert) levels of expertise and their own Claude or Codex subscriptions, ran an "auto research loop" and reproduced the result anyway — his point being that with a clear cost model or target to aim at, citizen-science-style contribution can move surprisingly fast.
Lichtman closes this stretch with two more asks: measurable metrics for library "coherence" and compactness, so refactoring agents and harnesses can be benchmarked and optimized against them; and, more programmatically, he recounts attending his first National Academies workshop on AI and mathematics three or four years ago, discussing two Google DeepMind projects — Minerva, for mathematical reasoning, and a companion effort aimed at formal theorem proving — that claimed significant improvements but worried him at the time because they'd never be made available to working mathematicians, a centralization-of-power concern. The years since, he says, have gone better than feared — thanks partly, in his "strong belief," to internal advocacy by specific people at major labs — to the point where these capabilities are built into standard frontier tools rather than kept as bespoke non-public systems.
Access, safeguards, and centralization of power
Lichtman pivots to a specific worry: multiple people have told him in the past week they can't use Claude Fable (Fable 5, in Anthropic's Claude 5 family) to help find bugs in formal theorem statements or proofs, because safeguards misclassify that work as offensive cyber activity. He connects this to live US-government conversations about regulatory regimes restricting or banning access to Chinese open source models — which he characterizes as "the complete list of all of the most powerful open source models in the world today". His ask is two-sided: advocate for safeguard fine-tuning or capability inclusion so the most powerful models stay usable for this community, and separately invest in open source tools as a hedge — since in his view there are no powerful open source models trained in the US and haven't been for years, "mostly... a funding problem," not a capability problem, in contrast to China, where companies and the government have been the de facto funders of the open source frontier "for well over a year".
Wang responds by returning to infrastructure layering. The bottom layer — agent-generated code review — is solvable either by borrowing best practices from existing software foundations and governance, or simply by continued LLM progress; it's "not too much of effort" to build harnesses compensating for today's models' instruction-following limitations, since that gap will likely close within a couple of months regardless. The harder problem, in his view, is that mathematics is vast and involves "the art of giving many, many names to the same... mathematical object." He locates formalization as an "atomic layer" that validates correctness, but argues there's a missing semantic layer above it — an ontology connecting arXiv, MathOverflow, and Wikipedia (the top layer) to formalized, verified proofs (the bottom layer), tying the knowledge base into something like "a living world model" of mathematical knowledge. That layer would help interpretability and let results propagate through shared infrastructure, breaking down field-to-field barriers — though he's candid that he doesn't know how to build it, only that he believes it's needed, and notes that cross-domain models like ChatGPT already function somewhat like this, able to explain the same object at whatever level a user wants.
Biderman is blunt: she "cannot choose Fable 5" even to contribute code used to formally verify Signal — which she frames as a good national security use case for the US — because the safeguards say no, adding that she's "very happy that we have Chinese models" as an alternative. Hicks adds a final distinction: there's a gap between frontier models and Chinese open source models, but also a separate gap between the frontier models the public can access (even when prompts aren't flagged) and internal models still under development at labs — both belong in the conversation.
Vakil notes the overlap with a Slido question from Talia Ringer about ensuring researchers retain access to state-of-the-art models, then moves to a submitted question on incentives: who builds and maintains this infrastructure, and how does it get paid for?
Incentives: benchmarks, tenure, and Erdős problems
Biderman answers first: you motivate the AI research community the way you'd motivate an optimization algorithm — give it a benchmark and it optimizes for that benchmark (for better or worse, so the benchmark has to track the thing you actually care about). AI conferences regularly run public challenges with cash prizes and dedicated workshops; organizing these is comparatively easy, and the AI community has a strong desire to be seen engaging cross-disciplinarily — she points to an AI-for-mathematics workshop at "at least one of the three biggest AI conferences every year since before I joined this field in 2020". A candid observation: only a strong minority of people she meets at AI-for-math workshops are working mathematicians (mostly it's AI people interested in math, or mathematicians who became AI people) — a contrast with AI-for-physics workshops, where she says the majority are active physics postdocs.
Lichtman picks up the benchmark thread with the Erdős problems. Erdős was extraordinarily prolific both as a mathematician and as a conjecturer, producing a large, heterogeneous problem set that sat publicly online for years before Tom Bloom consolidated all of it into a single site, erdosproblems.com, a few years ago. His takeaway: pairing a large centralized repository with a compelling narrative around a single historical figure focused community attention in a way that produced progress at scale.
Hicks adds that resourcing contribution matters as much as the incentive — his suggestion of shipping an agent alongside a library so contributors don't need their own tokens — and argues, again via the Erdős problems, that there's already a large population of people with math or STEM PhDs outside academia who want to contribute and barely need incentivizing; what they need is infrastructure: review, leaderboards, and — his example — "send them a T-shirt." His team gets many PRs from people simply excited about cryptography, Ethereum, or Signal being formally verified, and at least one contributor parlayed library contributions into a job interview at Anthropic, where the deliverable was itself related to formally verifying Signal in their library — something Hicks says he "discovered yesterday".
Wang returns to a structural gap: in academia, nobody gets tenure for building a library — "everybody celebrates findings," while infrastructure work risks being dismissed as "the IT guy wrote the code" — whereas in industry, infrastructure is valued because it becomes IP or a trade secret. His ask: academia should give infrastructure-building "first-class citizen treatment," with real credit-sharing and credit assignment, so the same career incentives that reward a result also reward the system that made it possible.
Biderman adds that incentive structures vary by field: open source contribution volume is a real reward signal in software engineering, and citation count plays a similar role in AI, but both are "significantly less valued" in theoretical mathematics — so any cross-field program needs to account for what actually motivates people locally rather than assuming one incentive works everywhere.
Hicks closes with a broader point: much of the incentive problem in academia is broken independent of any of this AI conversation, and the panel probably shouldn't over-constrain itself trying to retrofit new infrastructure onto incentive structures already widely considered dysfunctional.
Audience questions: labs, funding, and specialized models
Vakil opens the floor. The first questioner — Dimitri Shlyakhtenko (UCLA) — draws a parallel to older experimental sciences — microscopy and similar fields — where credit is given for building better instruments, where technical support staff and heavy lab-equipment investment are normal, and where that infrastructure ultimately underwrites where "the truth comes in"; he asks how apt the parallel is and what can be learned from how those departments have operated. Vakil paraphrases the underlying concern as one about talent pools: if certain fields are starved of resources in the US the way math sometimes is, other countries — he mentions China and Europe — end up building the ecosystems of young researchers instead.
Hicks doesn't think the funding situation is "dire of this stature," though he grants the point, recalling that his own PhD group had to move offices because UCL had recruited a medical-imaging researcher with a large budget and unlimited space. He argues pure mathematics is comparatively well set up in one respect he envies: it rewards people for finding simpler proofs of already-established results, unlike cryptography or CS more broadly, which tend to prize only what's new. You can't currently get an NSF grant to maintain Mathlib, he concedes, but you likely can get one to do research that streamlines things and produces new proofs of existing results along the way; the current moment may be "a phase transition" the community will work through, aided by industry and AI-company funding for things like formally verified cryptography — though he calls those "really one-offs" rather than a stable base, and argues the community has real influence to signal what's fundable, especially on behalf of junior colleagues.
Biderman follows with an anecdote about reframing research for funders: she wanted to build pairs of language models trained on substantially similar data with a small amount withheld, to make progress on machine unlearning, and spent a year and a half unable to get anyone to fund it — until she reframed the same project as an AI-safety problem, specifically preventing models from retaining hazardous information related to advanced bioweapons, at which point she secured a UK government grant without difficulty; the resulting paper has been influential in both the AI-safety and ML communities. On rewarding infrastructure directly, she describes a standing EleutherAI policy: anyone who contributes a significant feature to one of the org's libraries automatically gets authorship on the next paper that depends on it — she currently has six people on such a list, tied to particularly important kernels they wrote for the training library. The policy came from directly asking contributors what reward they'd value; sometimes it's financial, sometimes it's just wanting their name listed, which is why the org keeps and periodically updates an authorship blurb at the bottom of its training and evaluation libraries.
The second questioner builds specialized models and asks whether we need specialized Lean-focused models at all, versus general frontier ones. He cites Inkling — Thinking Machines Lab's open source model — as strong generally but "horrible at Lean" on the miniF2F benchmark, and asks: if a well-funded effort (he directs this at EleutherAI) built a genuinely strong open source Lean model, would people actually use it, given that existing specialized systems like Aristotle reportedly see less use than general-purpose tools despite large in-house training corpora (he cites "100 billion tokens")?
Biderman's answer is short: success for a specialized model means adoption, not benchmark scores — if a specialized Lean model saw no use, she'd call that a failure to build a good one, not evidence the idea was wrong — and defers the rest to a follow-up conversation. Hicks gives the longer answer: he experimented with fine-tuning Lean-specific models back in 2024 and considers it, in retrospect, "a bit of a waste," since gains from new frontier releases (Llama 2/3 were the open source state of the art then) outpaced what fine-tuning delivered, and today's frontier tools already have Lean-specific sub-agents built in. He describes himself as an early user of Aristotle and another automated prover, and says he personally prefers terminal-based workflows over these tools' web interfaces. His central point: for most practical work — proving lots of non-Fields-Medal-level results quickly rather than one extremely hard proof — "the floor is far more relevant than the ceiling," and the frictionless UX of tools contributors already have installed (Claude, Codex) beats the marginal quality gain of a separate specialized account; his team has anecdotally seen Aristotle-aided contributions phase out over time as general frontier-model quality improved. He still thinks fine-tuning retains value, but targeted at a corpus of specific libraries and problem domains (his example: cryptography formalizations went from bad to good once the team rewrote proofs over free monads, at which point general models became fluent at it) rather than "Lean" as an undifferentiated target — floating an idea he calls a "Hermes agent," open source agent profiles attached to specific libraries, that he's "very enthusiastic about." He pushes back on the idea that a specialized moat is durable at all, since frontier labs can simply absorb any generally useful specialized capability into their own harnesses.
He begins a further pushback — "I will slightly push back on that" — but Vakil cuts the panel off for time, thanking Lichtman, Hicks, Wang, and Biderman before breaking — the return time pushed from 11:15 to 11:20.