The tape picks up mid-sentence, right after a break in the recording. Ken Ono is finishing a thought about some conjecture he isn't personally an expert on, calling the news around it "very promising." Whatever the specific news was didn't make the tape, but the framing he wants the room to hold is clear enough: today's graduate students "enrolled in a profession, and they will graduate into another one. They made a bet on a stable discipline, and that discipline has changed underneath them."
A profession that made a bet on stability
Ono stakes out his own position before a single slide. The career bundle that trained him went "prove theorems, you get to teach, apply for federal grants, and, well, you get to referee for free" — resting on three legs: public funding, university positions, and donated labor, all cracking. He hedges: "I do not stand here to tell you that the model is dead because I do not believe that. But I also know that hope is not a plan and nostalgia is not mentorship."
The credentials that follow set up the talk: REU students trained, 10 Morgan Prize winners, 35 PhD students, "a gaggle of postdocs." He's UVA faculty on leave, now full-time inside Axiom Math, an AI company hiring the people this exact pipeline produced: "Melanie, I just hired one of her students full time, also a Morgan Prize winner. And one of Lauren's current postdocs is a resident working with us at Axiom." That's his vantage point — one foot in the university, one in the startup pulling talent out of it. He closes with a gentle pushback on "Terry" (Terence Tao, who spoke immediately before him): Tao's "era of abundance, an overabundance of theorems" is real, "but let's not forget there's always an abundance of questions." What won't survive unchanged, in his view, isn't mathematics itself — it's the old bundle.
Show, don't tell: three modes of "AI"
Ono says he rewrote the talk the organizers wanted from him because he'd rather show artifacts than assert conclusions: "I'm going to show you, and then you'll be able to form your own opinions." He was "a much happier person in 2017" than today, back when his life was "chalkboards, legal pads, and the tearoom conversation"; a year ago he'd have still been the traditional professor who didn't think he needed to know about AI.
He tells a story on himself from 1993: as a postdoc sharing seminar space with a newly hired AI researcher, he joked that "us naturally intelligent people are now moving in" — "well, I think I've had my butt handed to me." The real turn was a benchmark project about a year before the talk: leading Epoch AI's FrontierMath Tier 4 team, alongside Ravi Vakil, Sergei Gukov, and Elliot Glazer. The task was writing problems hard enough that models would fail — easy in the narrow sense, but reading the actual reasoning traces, "these large language models had really come a long way. They started to sound like a graduate student."
From there, the taxonomy the rest of the talk depends on — a slide he wanted to "get right" since "AI" is doing three different jobs in the room, and conflating them is "the fastest way to over-claim": discovery (examples, patterns, conjectures, superhuman search), reasoning (a mathematician's actual interaction with an LLM), and verification (formal statements, proof assistants — what this meeting is nominally about).
Mode one — discovery: PatternBoost and the missing edge
For discovery, Ono points to a 2024 paper by "Francois Charton, who is a colleague of mine at the company Axiom Math," "Jordan Ellenberg, who I hired at the University of Wisconsin many years ago," Geordie Williamson, and Adam Wagner: PatternBoost: Constructions in Mathematics with a Little Help from AI. Its flagship examples didn't personally land for him at first — "none of the examples presented in this paper spoke to me" — until one did: optimal configurations of dots on N-by-N grids where no three dots form an isosceles triangle.
Stronger still: a 1992 conjecture by Graham and Harary giving a lower bound on the number of edges in an N-cube with diameter at least N; in the N = 6 case, a spanning subgraph needs at least 82 edges. PatternBoost found one with 81. "81 is so close to 82, this is the stuff of imagination," he says — you have to rethink the conjecture. Mechanically, the method alternates a search step with a "global transformer step," feeding new candidates back into the loop — reward-driven example-finding, "really the epitome of what is machine learning." Axiom gives a free version away, a tool called Axplorer.
Mode two — reasoning: IMO gold, Erdős problems, and a Jacobian counterexample overnight
Mode two is what most people mean by "AI did math." Ono dates the public turn to July 2025, when Nature reported DeepMind and OpenAI models solving IMO problems — news he found himself "horrified" was news, given that students were competing at the same competitions. A timeline follows: AlphaProof and AlphaGeometry's "first proof" results, problems hard enough that "it's difficult to find a human being that can solve two or three of those problems."
The pace since has been dizzying — "out of OpenAI, seems like every few days, every few hours, something major is happening" — citing "Erdős 1196" (Jared Duker Lichtman, in the room, worked on it), the Erdős unit distance problem, and, the night before his own talk, a claimed counterexample to the Jacobian conjecture that forced him to scramble his slides after already sending them ahead.
He's visibly uneasy treating the Erdős list itself as an AI benchmark — he knew Paul Erdős personally through mentors Carl Pomerance and Andrew Granville, both close friends of Erdős — calling it "kind of hijacked in a way as a benchmark for AI," even while granting it's become genuinely useful for difficult mathematics.
His summary of what LLMs are currently good at: "uncovering known results in the literature," "applying existing techniques with exceptional breadth," and — the two he thinks are new — "impressive mastery of the literature" and "impressively connecting ideas from different fields," which he flatly calls superhuman. He reads a July 19th post from Thomas Bloom on X predicting new model releases produce "a spike of new solutions for several weeks, and then it will slow down substantially" — a pattern he agrees with, while rejecting the implication that models can never originate ideas outside the existing corpus: "I actually don't think so, and I think there's a lot for us as human mathematicians."
Extraordinary librarians (and the 9.11 problem)
Ono's compressed thesis on LLMs: "extraordinary librarians." "You cannot find something a large language model has not read, has not mastered. You put a paper on the archive, a couple hours later, it knows it." He tested this the night before with Levent Alpöge's post announcing a counterexample to the Jacobian conjecture — 30 minutes later, Claude had already "summarized and distilled it quite beautifully."
Two Gemini anecdotes cut the other way. Asked to illustrate the librarian metaphor itself, Gemini returned a "gigantic robot" towering over "itty bitty people with question marks over them."
And a genuine Gemini failure someone else surfaced: asked which is bigger, 9.11 or 9.9, the model answered "9.11 is bigger than 9.9 because of course 11 is bigger than nine."
"You have to wonder where will it be making mistakes," Ono says — "do you want your librarian to be your neurosurgeon? God, I hope not." As editor-in-chief of three journals seeing 60 new papers a day, he wants help but would never hand final acceptance decisions to a model.
What formalization actually is, and why Lean
Ono's "highbrow overview... in service to DARPA": natural-language mathematics must be converted into definitions, types, lemmas, dependency graphs, and "blueprints," then into computer language — raising the question of whether that conversion, human-assisted or auto-formalized, is faithful to the original. Formal language is explicit, typed, checkable — but checkable doesn't mean seamless: he cites known cases where an elementary statement was Lean-verified with no `sorry` left, yet the human who wrote the translation had still gotten it wrong.
On Lean, he credits its trustworthiness to a small, heavily stress-tested kernel and to one person: "It's because at AWS, Leo de Moura made this his life goal" — Leonardo de Moura, the Lean creator, reportedly soon to be elevated to distinguished scientist at AWS.
He credits other proof assistants too, noting some subfields' leaders prefer them to Lean. A Lean proof of the fundamental theorem of arithmetic, he notes, runs to 2,000 lines — bulky not because the math is hard but because of "computer science crap" wrapped around the actual argument. He's also adopted a habit: he no longer says his system "proves" something, but that it "produced the proofs" — a hedge given how hard it is to trace an idea's origin inside these systems.
AxiomProver: from a perfect Putnam to a perfect IMO
Within four days of joining Axiom, "with a little bit of retooling," the team got a perfect Putnam score, solutions formalized in Lean — no human checker needed. A year after the 2025 IMO-gold headlines, last week's IMO produced perfect scores across models, paired with fully formalized solutions, he says: "not only can we solve the IMO, we can check it ourselves, and it's not even news to us."
He also points to the Lean formalization of the sphere-packing problem as a story that "made world news", citing the arXiv paper and its linked GitHub artifacts as the kind of transparency he wants from AI companies generally. On staffing: Sidharth Hariharan (his intern this summer), Siwu (an intern all year), and Bhavik Mehta (a consultant) — Hariharan and Mehta both appear as co-authors on the sphere-packing arXiv paper — plus a shout-out to Jesse Han and Math, Inc., whose autoformalization model "Gauss" handled the final verification push, credited by name in the paper's abstract.
The broader point is silos breaking down — at UVA "the tearoom conversation was, I would talk to the three or four mathematicians that knew my area," while at Axiom that circle has expanded well past that.
Watching the dependency graph turn green
The workflow description is the most vivid part of the talk. His day-to-day: LaTeX files, personal notes, and "my system AxiomProver" open side by side, a dependency graph of a theorem's proof on screen, the prover checking each step in real time — nodes flipping "from gray to green" against a scoreboard reading "80% of the things have been solved, 90%." "I can sit there for three hours and watch it... And when it gets to 100%, I usually scream in the office." Sometimes he already knows the proof; sometimes the system gets stuck and he learns new mathematics watching it resolve. The stated goal, against the "ask AI, get an answer" caricature, is to "eliminate the sorry" — not just one, potentially 400 in a single proof.
He's blunt about authorship: "AI is not writing a word of any of our papers, and if you try to do the faithful one-to-one correspondence between the LaTeX code that I've written and the Lean code, you're going to be very disappointed." After a Lean proof lands, he spends up to two weeks drilling into it before writing the paper himself, and not everyone adapts equally fast — Evan Chen is the exception: "not everyone is Evan Chen. In fact, I know almost no one else at that level."
Why this matters beyond mathematics
With time running down, Ono adds a quick aside on education (he and Robbie sit on the Mathematical Sciences Education Board at the National Academy, calling out Amy Stephens, who directs it, to stand up in the room) and states the stakes bluntly: "the brutal truth is mathematics is the language of engineering and science. I could prove the Riemann hypothesis and maybe I'd get famous, but the world will not pay much attention for long." What's changed is that the world has caught up to why rigor matters — calculus students who never wanted delta-epsilon arguments now live in a moment where "rigor and formalization might actually matter in the universe," backed by photographs of software, hardware, and cybersecurity verification, including "the capture-the-flag incident that Claude Mythos broke."
Rather than chase Erdős-style benchmarks, Axiom set out to see whether its systems could produce genuinely new theorems via AxiomProver, planned for release later this year. He counts 18 papers as current output — 7 accepted or published, 4 recommended for publication, and 7 further preprints — singling out "Parity of k-Differentials in Genus Zero and One," accepted that morning by the Quarterly Journal of Mathematics at Oxford — a problem at the interface of differential and algebraic geometry that "should've been solved maybe 40 years ago," stuck on a technical lemma the system resolved on its own "using ideas that were modified from a paper in the 1860s." Other venues: Mathematische Annalen, Advances in Applied Mathematics, and Geometry & Topology, producing at this level "since February." He's candid he's "not an expert in half of these fields," crediting AI with letting him enter research areas he'd never have tried a year earlier.
Two proofs he didn't expect: partitions and lattice triangles
With minutes left, Ono picks two examples against the "ask a question, get an answer" caricature. First, George Andrews — "former president of the AMS and a member of the Academy" — who, with a professor at the University of Florida, proved in December that for non-exceptional N, a partition function he calls C3 is exactly one-third the size of another, D3, and asked for the actual combinatorial bijection witnessing that relationship — not just the numerical equality.
Ono's system found the disjoint three-way decomposition of D3 almost immediately, via a generating-function argument he likens to "Dirichlet orthogonality of characters" — analogous to Dirichlet's theorem on primes in arithmetic progressions — without the problem ever having been posed that way. The bijection itself was harder: a composition of four maps; in the N = 15 case, the first and last columns sum to 15, but the middle column sums to 14, meaning the system invented an intermediate step that changes the partition size and "puts one back later in a magical way."
By his count, roughly 6,000 steps are involved in checking the bijection in the Lean compiler. "I don't want you to be impressed like this is the Jacobian conjecture... but I want to show you what the AI can do."
Second, a tribute in passing to Maryam Mirzakhani — Ono is making a film about her, having previously made The Man Who Knew Infinity with Manjul Bhargava, with the same team's seed raise now closed. The math: a March email from Alex Wright, a professor at the University of Michigan, posing a problem in Teichmüller dynamics about "lattice triangles" — triangles whose billiard surfaces carry arithmetic symmetry, related to Veech surfaces.
Wright's message, quoted directly on the slide: an elementary criterion developed by Anne Larsen — whom Ono called a former student, part of "the most incredible family of mathematicians" and a daughter of Indiana University's Michael Larsen — with Chaya Norton and Bradley Zykoski isn't sufficient to classify all lattice triangles alone, "but it should be possible to get surprisingly close."
Ono's team didn't prove the full conjecture but confirmed Wright's speculation, showing counterexamples "tend to zero along a density one subset of denominators." "We didn't have the proof, and I am very grateful that AxiomProver was able to finish it... I was in the loop, but I wouldn't have been able to write this paper by myself."
Six to twelve rocky months, then a plateau
Ono's closing turn is candid: "the next six to 12 months is going to be very rocky... and then there will be a plateau, and I can't wait to get to that plateau, because at that point, the AI will be accepted." Academia, from his own experience as a former STEM advisor to the Provost at the University of Virginia, moves on a timescale of years — but he expects new ideas to remain "largely human," in collaboration with AI, with conjecture generation increasingly automated as "honestly good news" for engaged practitioners. He closes by disclosing he signed the Leiden Declaration on AI and Mathematics on its first day — an imperfect document that nonetheless "does a lot of things right."
Q&A: infrastructure inside a startup
The one audience question captured on tape is pointed: startups fail, so what happens to mathematical infrastructure built inside one — not just Axiom? Ono offers his own numbers: the company "went from, like, 20 million to 1.6 billion in a matter of months." His answer on durability leans on transparency over guarantees — publishing everything, hoping the GitHub repositories "live forever," expecting a pivot toward outreach as its tools mature. He's candid about the risk of leaving a tenured position at UVA — "I would be lying to you if I wasn't waking up every day through early February wondering, 'What the hell did I do? Am I really doing the right thing?'" — while standing by the decision. He closes without fully resolving it: "I'm not sure I completely answered your question, but I can't predict the future."