Axiom Math CEO Carina on building an AI mathematician that writes proofs in Lean, why Lean data is scarce, and how formal proofs differ from ChatGPT math.
AI can already prove theorems, and the next step is an AI mathematician that also proposes new problems and checks its own work. That is what Carina, founder and CEO of Axiom Math, says her company is building, as she explained on Episode 22 of Built This Week. Axiom's system writes its math in Lean, a programming language, so every proof can be run and verified like code instead of graded by a person or another model.
Before the interview, Jordan built an LLM math roaster with Axiom in mind. You pick from a set of about 10 problems of different difficulty, or submit your own. The app sends it to four models at once: Gemini 2.5 Pro, GPT-5, Claude Sonnet 4.5 and Grok 4 Fast. Each one writes a formal proof in Lean 4 syntax, and the app shows the response time for each.
Because no model knows which model is smartest, Jordan picked ChatGPT as the judge. It reviews every answer, scores it and posts the results to a leaderboard, with a history of past runs. He also added an API so Axiom's team can generate their own key, send in a question and get every model's result back to compare. His first test was two plus two equals four, which all four models passed.
Watch Carina explain Axiom's AI mathematician in Episode 22 (starts at 9:38) · Episode 22 notes and transcript
Carina picked Fermat's little theorem for the real test: for a prime p and any integer a not divisible by p, a to the power p minus one equals one mod p. The judge gave Gemini the top score, 98, and ChatGPT 70. Carina spotted why one model lost points: it proved the theorem for natural numbers instead of integers, leaving out the negative numbers. She called it a close miss.
She also suggested a cleaner judge. Instead of asking an LLM to grade the proofs, you could paste each Lean proof into a Lean editor and see whether it compiles, which she said should be more painless. Jordan's takeaway was broader: the same setup can compare models on any dataset, whether that is a proof or a lawyer's contract. Run thousands of problems, he said, and you would find each model's weak spots quickly. Carina said that was the first thing Axiom did, back when the office was camper chairs and a plastic folding table.
Carina says Axiom is building a model that does more than score well on Olympiad-style benchmark problems. The goal is a system with the skills of a research mathematician, including the ability to conjecture: to propose new, unseen problems and hypotheses. The same system then tries to prove and verify them. A prover and a conjecturer talk to each other and form a self-play loop.
The third piece is auto-formalization, which turns the large body of existing math writing into Lean. Carina's reasoning is that reinforcement learning has made big breakthroughs in domains where answers can be verified, like coding. By combining AI, math and a programming language, she believes math will see the same kind of step change, especially on serious research math beyond the benchmarks models have already seen. You can read more at axiommath.ai.
Jordan asked whether moving math from CPUs to GPUs was the big shift. Carina said Axiom uses both: the language models run on GPUs while Lean compiles on CPUs, and keeping both busy is a real engineering problem. But she does not see compute as the bottleneck. The hard part is data.
There are more than 1,000,000,000,000 tokens of Python code, only about, like, 10,000,000 tokens of lean code. That's a 100,000 times data gap.
— Carina, Episode 22
She says some companies, especially some Chinese teams, hire large numbers of Lean programmers to write data by hand, which is expensive and does not scale well. Axiom bets on synthetic data instead. It scrapes informal math that already exists and auto-formalizes it into Lean, and it works on ways to take a seed set of formal math and make it many times larger.
Jordan compared AI in math to the jump from no calculator to a calculator, and asked whether students now write proofs in Lean. Carina says many universities teach it. She named the University of Washington, a strong Lean community at CMU that includes Professor Jeremy Avigad, and Stanford's automated reasoning lab led by Professor Clark Barrett, where grad student TAs teach Lean. Many universities in the UK and Europe teach it too.
Mathlib, Lean's math library, started as a teaching effort at Imperial College London by Professor Kevin Buzzard. He wanted the students in his introductory proofs class to write more rigorous proofs by formalizing everything in Lean. It turned out the students who joined were the advanced ones who did not need the class, and they set out to formalize the undergraduate math curriculum in Mathlib. Carina says two or three of them now work with Axiom. She met several through an MIT and Imperial College London exchange around 2019.
Carina says large language models do math in the informal space. They write proofs in English and give multi-step reasoning, and a final numerical answer can be graded. The intermediate steps are the problem:
So it's very difficult for an expert or a layman to know whether there might be a hidden bug among, like, a 3,000 line math proof.
— Carina, Episode 22
Axiom's hybrid prover makes sure its output is verified by a program. There is a Lean program underneath every result, and that program runs.
So in a way, we do not need an LLM judge or a human judge. We just run it like you run a Python computer program. I think that's the biggest difference between these formal models and the large language models.
— Carina, Episode 22
She noted that Google DeepMind's AlphaProof, which earned a silver medal at the International Math Olympiad one point below gold, is a formal system, while this year's strong IMO results from Gemini and OpenAI came from informal systems. Olympiad problems follow a set syllabus, which limits the search space. When proofs get long and require hard math, she believes formal systems will keep scaling where informal ones struggle. We covered a related idea, using formal methods to prove that AI-translated code is correct, in Episode 48.
The episode was recorded the week Gemini 3 launched. Jordan had downloaded Google Antigravity, Google's new code editor, and was being throttled everywhere after burning through his tokens. Still, he said he was very impressed with Gemini 3 for coding and for its design taste. Sam tried it on a personal meditation app and hit some hiccups, which he said might have been user error.
Carina said Axiom likes Gemini 3 and that it is much cheaper to run than GPT. She said it scored 100% on AIME 2025 with code execution, which she read as a sign of how much tools matter, and she said Axiom's own model beat Gemini 3 on one math proving benchmark. Jordan sees Gemini 3 as the first big leap from a hyperscaler, with Google able to put it into Workspace, search, YouTube and ads.
The episode also covers Jeff Bezos's Project Prometheus and Suno's latest raise. Carina hopes that one day people with mathematical talent but no training in formal proofs could use Axiom to turn an idea into a real theorem, the way Suno lets people without music training turn a melody into a song. Watch Episode 22 of Built This Week, where the full transcript is also on the page.
