The recording picks up mid-introduction, as the host runs down the roster: Ralph Abboud from Renaissance Philanthropy, Carina Hong from Axiom Math, David Spergel from the Simons Foundation, and Shida Wang from XTX Markets — moderated by Brendan Hassett, professor of mathematics at Brown and director of ICERM, the NSF-funded math institute there.
Hassett opens with a simple prompt: introduce yourself, your organization, and what you hope formalization gets you.
Who's actually on this panel
Carina Hong goes first: founder and CEO of Axiom Math, "AI for mathematics and for verified reasoning," based in Palo Alto with small offices in London and New York, roughly 50 to 60 people, venture-backed with two funding rounds, founded July 15 of last year — "about exactly a year ago." Formalization is the company's bread and butter: a full technical staff on autoformalization, automated theorem proving, search tooling, and Lean infrastructure, plus code-verification work leaning on transfer learning from Lean into other formal languages used in industry.
David Spergel: theoretical physicist, longtime Princeton faculty, now president of the Simons Foundation. He credits Yuri Tschinkel, who leads math and physical sciences at Simons, with steering the foundation toward supporting the Lean Focused Research Organization (the Lean FRO, launched with Convergent Research), plus panels, workshops, and a Lean summer school. About a year ago he was in Lviv, part of a National Academies program on Ukrainian reconstruction he co-chairs with Marsha McNutt, and in a conversation about building a math department from scratch, "we convinced them that they should focus on formalization." Lviv is now building such a program with Jeremy Avigad and a Carnegie Mellon group, people at Max Planck, and — he believed — XTX support.
Ralph Abboud: Principal Scientist at Renaissance Philanthropy and lead of the AI for Math Fund, an annual open call supported by XTX Markets that reviews community proposals for funding. Formalization is a major share of the fund's allocations: infrastructure exposing interconnections across math and scaling correctness review (conditional on agreed semantics for definitions — "something that has come up a few times already today"); building community practice around formalization; and a throughput advantage over natural-language math for processing large volumes of incoming results.
Shida Wang closes the round: he works at XTX, with a background in theoretical machine learning and mathematics, and is here to discuss XTX's formalization effort — building more accessible infrastructure for the open mathematics community.
Hassett places himself on the record too: by training an algebraic geometer and number theorist, joking his field is "getting appropriate amounts of love from the community" already.
What mathematics do you actually care about?
Hassett's next question is about scope. Shida Wang answers first: XTX mainly funds, and picks "maths infrastructure" deliberately because it's too large a category for one academic group to sustain — hence a community effort to maintain a shared library like Mathlib. Pressed on what "infrastructure" means, he frames it partly as CS infrastructure: Lean as a language whose output can be checked, openly accessible so anyone can audit for bugs, so correctness is "openly agreed instead of just verified once or twice."
Abboud says the fund has no fixed field preference — the target is maximizing "marginal delta per dollar invested," driven by the reviewing community itself. As a marker of how fast the bar has moved, he cites the fund's inaugural cohort project by Kevin Buzzard of Imperial College London, formalizing several Annals of Mathematics papers — far more ambitious a year ago than today, "while it still being extremely challenging." Buzzard's AI-for-Math-Fund grant is a two-year effort to encode research-level theorems from recent journal publications into Lean and assemble a public dataset from them.
Spergel describes Simons' program as broad: support for the arXiv, a new nationwide graduate-student funding program, cross-field collaborations, international reach, and support for several math institutes. He believes Simons is "the largest private funder of mathematics," significant even against NSF's scale, and notes a fall panel to plan new AI-for-math initiatives.
Carina Hong's answer is the most structured: three things that matter when Axiom picks areas to invest in. First, distance to Mathlib — enlarging the library and its foundational definitions; Axiom's team, led by Ken Ono, skews toward number theory and algebraic geometry given who's on staff, but has intentionally pushed into dynamical systems and differential geometry. Second, code quality, not just correctness — formalizations recognizable to the existing Mathlib/Lean community, "as opposed to AI slop," in a human-AI collaboration model where the AI produces things people want to build on. Third, adversarial benchmarking in the ML sense: private benchmark sets targeting suspected weak domains, updated regularly to separate real gains from "performative" ones — including a push into Econlib (a later panel covers economics) and applied-science domains where scholars have told her referee capacity is lacking, hoping a system like Axiom Prover could ease that bottleneck.
"Show me the money": the resources on the table
Hassett pivots with a line worth quoting directly: "I guess I find myself at the show me the money part." He puts Spergel on the spot first. Setting aside his Simons hat, Spergel notes he sits on the DOE's Science Advisory Council, specifically its Genesis subcommittee — a government-wide effort to use AI to advance math and science. At a DOE meeting the preceding Friday in DC, Japan was announced as a new partner, on condition that AI for math be included as a priority area. Spergel raised this with Dario Gil, who leads DOE's Office of Science, discussing progress from AI reaching silver-medal standard at the IMO — DeepMind's systems did so in 2024, and took gold in 2025 — to genuinely new mathematics, adding that even this account was already stale by the time of this panel.
Back in his Simons capacity: an open-call model — annual calls for collaborations, graduate student funding, no more Simons Investigator program, resources redirected entirely into collaborations. Pressed on the biggest obstacle, he doesn't hedge: "my biggest worry about obstacles to advance here is the relatively conservative culture of mathematics departments. They are slow to do hires in this area." Contrast with physics, institutionally not conservative but fast to hire ML-for-physics people — his own last three thesis students went straight from PhD to faculty jobs at Stanford, Cambridge, and Tokyo. He finds it strange that graduate students, at a moment of unprecedented tools, are mostly afraid AI will "prove their thesis" out from under them — his prescription: funders and universities should push to double the number of math PhDs, naming OpenAI, XTX, and Jim Simons's Renaissance Technologies (still hiring for its Medallion funds) as eager employers. Universities, he says, are "incredibly fearful right now... university presidents are generally cowards," though "the vice presidents are not."
Hassett hands to Carina Hong for Axiom's resources, split into general field resources and Axiom-specific commitments. On the landscape: program verification in computer science — languages like Rocq (the proof assistant formerly known as Coq), alongside Lean, Isabelle, and HOL, with transfer learning meaning strength in one carries to the others. She cites AWS "tripling down on automated reasoning" and the CEO/chief scientist of Toyota Research Institute being "very bullish on formal verification for automobile industry," then traces a longer history to aerospace — flight-control and spacecraft verification since "the time of Challenger," when the European Space Agency verified 260,000 lines of code over five years of human effort for one small memory-isolation component of a hypervisor.
Her point: AI can vastly accelerate that class of work, and a wave of private AI-for-math startups, many founded from "pure love and passion for mathematics," are discovering a real business model underneath.
On Axiom's own releases: the standard Lean proof-checking tool is too slow for large-scale RL reward signals, which motivated roughly a dozen infrastructure tools that handle Lean proofs deterministically and symbolically, bypassing an LLM where it isn't essential. Those tools ship as AXL, the Axiom Lean Engine — already open-released and free; a second system, Axiom Prover, is planned for staged community release later this year, also free; a third, more experimental tool she calls "radical," fully open source, targets discovery of examples and counterexamples, described as a much more optimized, end-to-end version of the PatternBoost approach. Axiom also plans search tools for formal (Mathlib) and informal search, via API, CLI, and possibly MCP for AI agents.
Shida Wang: XTX supports Lean 4, Mathlib, the AI for Math Fund (deferring to Abboud on that), and the Artificial Intelligence Mathematical Olympiad (AIMO) — a public competition that maintains a problem dataset and releases results and benchmarks for community assessment. Abboud gives the dollar figures: AI for Math Fund direct grants totaling $10.5 million this year, again with XTX support. This is the fund's second year, building on a first year that "started with what was $9.2 million of grant support" — the figure matching the fund's public December 2024 launch — later increased thanks to additional XTX funding to $18.2 million total; the $10.5 million is this year's direct-grants line.
Beyond core grants — up to $1 million each, four-to-five-month decision process — there's a faster "Seed Grants" track, up to $100,000, roughly four-week turnaround, which Abboud says has felt less like a fast-response mechanism than hoped given the field's pace. Also new this year: a "Summer Fellowships Program" — seven students selected for paid internships at year-one grantee organizations, funded from the AI for Math Fund pool.
Is there still a future in proving theorems?
Audience questions via Slido raise where money for training graduate students will come from, layered on an anxiety Hassett voices plainly: many students perceive that getting paid to prove theorems is itself at risk of automation.
Spergel reframes the fear: a year ago there was broad concern about a proposed 50% cut to NSF funding, but he draws the opposite lesson — a Republican-controlled House and Senate "completely restored NSF's budget," flat from 2024 through 2025 into 2026, with appropriations staffers anticipating another flat budget ahead. His deeper argument: society doesn't fund mathematicians against a quota of theorems per year, so faster mathematics should make mathematicians more valuable — his analogy is a DuPont chemist who, producing twice as many patents with AI help, doesn't get replaced by half as many colleagues but makes the company hire more chemists. Non-federal money is arriving too: three major IPOs this year are about to mint many newly wealthy people, including a former postdoc of his own worth "half a billion because he joined Anthropic early" — one of several "we need more Jim Simons" stories, alongside XTX.
Carina Hong adds her own lineage: Axiom is indebted to Howard Morgan, chairman of B Capital and co-founder of Renaissance Technologies alongside Jim Simons, who seeded Axiom's round. She names another supporter as well, a Stanford applied-mathematics PhD who studied alongside the late Fields medalist Maryam Mirzakhani. Her larger optimism: mathematicians aren't like artists simply disrupted by AI, because "math formalization is on the critical path to AGI," since trustworthy AI deployment requires the guarantees formalization provides — what she calls "verified super intelligence." She's more worried about the early pipeline — high schoolers and undergrads outsourcing exercises to language models — than already-trained PhDs, and floats that the field may need to separate "AI for math" from mathematics proper, or redefine mathematics to absorb it. Concretely, Axiom sponsors the Delos REU undergraduate research program and "almost all" AI-for-math workshops — NeurIPS, ICML, ICLR, AI-for-math-discovery special workshops, and Oberwolfach. She separately worries the mathematical-discovery literature could get sidelined as LLM reasoning goes mainstream, naming the PatternBoost group — Jordan Ellenberg, François Charton, and Geordie Williamson — and arguing this "constructions, not proofs" tradition needs deliberate protection.
Abboud echoes the optimism, describing a shift in the fund's applicant pool: last year's proposals read as "I would like to formalize theorem X for Y dollars," this year's are more conceptual — common threads across formalizations, elegance, meta-properties of the pipeline. His diagnosis of student anxiety: not that opportunities have shrunk, but that PhD structures and rewards haven't caught up to how far research questions have moved — a split between students who've pushed further and are "extremely optimistic," versus those on the beaten path who feel stuck or in "a bit of an existential crisis." Shida Wang closes narrowly: XTX doesn't fund students directly but supports infrastructure like Lean, hoping easier tooling lets younger learners encounter formalization earlier.
Are legacy math departments the bottleneck?
An audience member — Andrew Blumberg of Columbia, who holds appointments in both mathematics and computer science — asks whether institutional inertia in math departments will force change from outside (citing MIT spinning out chemical engineering once chemistry couldn't scale) or whether adjacent disciplines will simply take the lead instead.
Spergel's answer is a comparative case study: computer science, when genetics became a problem CS could contribute to, hired geneticists and broadened its own definition — part, he says, of why CS departments are now the university's largest. Physics, by contrast, threw out astrophysics, geophysics, and material science over time, narrowing itself until, in his words, you'd struggle to "find a physics department with someone solving the Navier–Stokes equation." He predicts math faces the same fork — grow to include formalization, or feed a larger formalization discipline inside CS — crediting the American system's diversity of institutional choices, and, asked whether this reflects math specifically failing as an institutional innovator, demurs: "failures and successes" are mixed everywhere.
Carina Hong takes the philosophical bait: she invokes the Curry-Howard correspondence between proofs and programs, arguing that reducing math to "code is math" undersells it; its actual core, she says, is curiosity, the belief that even a thousand-line Lean proof will still get read and discussed by humans who want to understand it. She describes a pattern she's personally observed linking proof strategies in pure math to unrelated physical/engineering problems — proving something too strong can falsify a later statement, while proving something too weak leaves you unable to say anything — as evidence "there is something more to mathematics to be extended and applied in the real world."
Abboud sees momentum toward departmental change as strongest at the grassroots — better infrastructure easing adaptation — with the deeper question being not whether departments reorganize but whether the community preserves what makes math math: that anyone can still start with pen and paper and work their way up. Shida Wang adds a practical note: the tension should ease "gradually" as Lean becomes more installable and graphical, lowering the barrier relative to today's need to learn "a brand-new complex programming language."
"Math departments are broke": pushback from the floor
Blumberg returns with a sharper, personal version of the point: he sits in both a math and a computer science department, and CS can afford to be experimental about hiring because it hires roughly half a dozen people a year, while a math department is lucky to get one hire every other year — a scarcity he says breeds "intense knife fighting." His example: graduate enrollment in math at Columbia was cut in half and will reportedly stay there "for the foreseeable future" because the arts and sciences division is financially strapped, which he attributes partly to federal-funding disruption — prompting an interjected "No, it's because of Columbia mismanagement," which he pushes back on: "No, this is happening. I asked around." His ask to funders: math departments could plan for this future more easily "if we were not quite so strapped."
Spergel responds as a funder: for Simons, resources are effectively zero-sum — a fixed fraction of the endowment moved between areas — and this year Simons chose not to fund experimental cross-field projects, funding junior faculty positions instead, including, he says explicitly, a math position at Columbia. His lever: OSTP has instructed NSF to make AI a funding priority, and his read is that NSF is sitting on congressionally appropriated money not yet released as grants — money that could fund AI-for-math faculty hires, satisfying the OSTP mandate while easing the hiring scarcity Blumberg described, drawing on his own 30 years watching physics subfields fight over scarce lines. He closes pointedly to anyone from NSF listening: "this is an area of opportunity" in the window between now and October.
Ken Ono takes a deferred question but turns it into an invitation instead: he calls this the "elephant in the room" and suggests it's exactly what tomorrow's breakout session — which Hassett is running — is meant to address, promising a white paper. Hassett pushes back lightly on Spergel's optimism from lived Provost's-office experience, and lands the panel's starkest number: "there are only 70 tenure track jobs in the United States of America in math this year, 10 of which were new to you... but we produce 2,000 PhDs a year."
Melanie Matchett Wood asks a different kind of question: rather than assuming AI-for-math needs deliberate institutional incentives, she draws an analogy to computer algebra systems like Sage — nobody hired mathematicians specifically for using Sage, it just helped some do better math, and hiring naturally rewarded the result. Is AI simply another tool that earns its own incentive once departments hire on output, without special targeting?
Abboud answers partially yes, but resists collapsing hiring criteria to AI-driven output alone — he sees an "epistemic discovery process" in mathematics that AI, used purely as a reward signal, doesn't capture well, and expects a boundary to emerge between "human difficult" and "AI difficult" math. His analogy: genetic algorithms are a powerful CS technique, but nobody has a "genetic algorithm professor" — AI, he expects, becomes embedded similarly, as a tool rather than a distinct hiring category.
Closing: AI for math as its own scientific field
Carina Hong gets the last word, arguing AI for math needs to be understood as a genuine scientific domain with its own canon — she cites a "really seminal paper" from 2022, "Draft, Sketch, and Prove," as foundational, hedging that she might have the year wrong and inviting Alex Kontorovich to correct her. She recalls her own first year at Stanford as largely a self-directed reading course through what she estimates as "roughly about hundreds of papers" in AI for math, and argues the field is still "not even 1%" of where it will eventually go — the world doesn't yet have enough people who are both AI-native and mathematically trained. She singles out Ken Ono, joking he's "joined the dark side," as an example of bringing a mathematician's thinking into ML systems design, and closes with an image worth keeping: prompting a language model is "fast food," but a mathematician engaging with discovery tools directly is closer to cooking for yourself — slower, more scientific, and a field not even at the 1% mark of the work still ahead.
Hassett thanks the panelists — Carina, David, Ralph, and Shida — and calls a short break.