What AI Is Missing for Real Reasoning? Axiom Math’s Carina Hong on how to build an AI mathematician

Summary

Carina Hong, co-founder and CEO of Axiom Math, discusses why current large language models struggle with mathematical reasoning despite their impressive capabilities in other areas. She explains that next-token prediction and training on human preferences are fundamentally different from how mathematical reasoning works. While LLMs can serve as “secretaries” for mathematicians by looking up citations and retrieving information, they fail at generating new mathematical knowledge, especially in multi-step reasoning problems where the decision tree gets very deep.

Hong outlines Axiom Math’s vision for building an AI mathematician through three core pillars: a prover system that generates verifiable mathematical proofs with checkable intermediate steps, a knowledge base that can track what’s known and introduce new theorems and concepts, and a conjecturer system that proposes interesting new mathematical questions. These components work together in a self-improving loop, with auto-formalization bridging natural language mathematics and Lean (a formal proof language). She emphasizes that human-AI collaboration remains crucial because humans and AI excel at different aspects of mathematical reasoning.

The conversation explores the distinction between AGI and superintelligence, with Hong preferring the latter term. She uses a “plate” analogy: AGI tries to expand from easy problems at the center toward all hard problems at the edges (curing cancer, solving Riemann hypothesis, writing Nobel-worthy novels), while superintelligence picks a specific goal and goes directly toward it. Axiom bets on building a domain-specific superintelligent AI mathematician that serves as the “algorithmic pillar” for AI in science, leaving real-world testing to companies like Periodic Labs.

Highlights

”Next token prediction isn’t how mathematical reasoning works”

yt-dlp --download-sections "*1:14-2:10" "https://www.youtube.com/watch?v=3qGBMkgR6Ko" --force-keyframes-at-cuts --merge-output-format mp4 -o "3qGBMkgR6Ko-1m14s.mp4"

“Current models are trained by next token prediction. That isn’t exactly what’s going on when you’re doing mathematical reasoning. If you are a human mathematician, you don’t give an answer just because other people say that it’s correct.” — Carina Hong, 1:14

”100,000 times data gap”

yt-dlp --download-sections "*21:35-22:30" "https://www.youtube.com/watch?v=3qGBMkgR6Ko" --force-keyframes-at-cuts --merge-output-format mp4 -o "3qGBMkgR6Ko-21m35s.mp4"

“While there are more than one trillion tokens of Python code, there’s only probably about like 10 million tokens of Lean code. That’s 100,000 times data gap.” — Carina Hong, 21:41

”Superintelligence can be domain specific”

yt-dlp --download-sections "*23:56-25:10" "https://www.youtube.com/watch?v=3qGBMkgR6Ko" --force-keyframes-at-cuts --merge-output-format mp4 -o "3qGBMkgR6Ko-23m56s.mp4"

“I like the word superintelligence better always better than AGI… Superintelligence can be defined as domain specific. So I can be a super intelligent AI mathematician, right? It’s very hard for this super intelligent AI mathematician to fold laundry the best.” — Carina Hong, 23:56

”Mathematicians are truth seekers, messengers”

yt-dlp --download-sections "*28:08-29:05" "https://www.youtube.com/watch?v=3qGBMkgR6Ko" --force-keyframes-at-cuts --merge-output-format mp4 -o "3qGBMkgR6Ko-28m08s.mp4"

“Mathematicians are almost like truth seekers, messengers. They climb ladders to pick on the sweetest apples and then spread it to humanity… What Hardy used to apologize for in A Mathematician’s Apology, a sarcastic apology that ‘well my math’s just totally useless,’ turned out to be quite useful in fact for war.” — Carina Hong, 28:35

”Math and intuition is closer to arts than to science”

yt-dlp --download-sections "*30:50-31:40" "https://www.youtube.com/watch?v=3qGBMkgR6Ko" --force-keyframes-at-cuts --merge-output-format mp4 -o "3qGBMkgR6Ko-30m50s.mp4"

“I always aspire for art, for artistic expressions and creations. And I think that math and intuition is closer to arts than to science. How do we sort of scientifically understand that? It’s fascinating.” — Carina Hong, 30:58

Key Points

• Why LLMs fail at math (1:14) - Next-token prediction and human preference training don’t match how mathematical reasoning works; models struggle with multi-step reasoning as problem trees get deep

• LLMs as mathematician secretaries (1:50) - Current AI excels at retrieval tasks like looking up citations from ancient papers or German mathematicians’ notebooks, but fails at generating new mathematical knowledge

• Three pillars of an AI mathematician (2:50) - Axiom’s architecture includes a prover system, knowledge base, and conjecturer system that work together in a self-improving loop

• Verifiable intermediate steps (3:26) - Unlike LLMs that give numerical answers, formal math systems verify every reasoning step, not just the final answer

• Auto-formalization (4:54) - The ability to translate between natural language mathematics and Lean code is critical for connecting human mathematicians with formal verification systems

• Human-AI collaboration (5:50) - AI and humans are good at different things in math; this asymmetry creates valuable synergy rather than replacement

• AlphaGeometry as eureka moment (7:11) - Google DeepMind’s paper showed synthetic generation of creative geometry problems by working in vector-based language, proving machines can create new mathematical knowledge

• Machine-generated objects guiding intuition (8:46) - Researchers at Axiom generate mathematical objects that help human mathematicians formulate de novo conjectures by observing underlying patterns

• Hybrid approach: LLMs + formal verification (10:22) - Combining informal LLM reasoning with Lean’s formal verification is the key timing advantage now; neither pure formal nor pure neural approaches are sufficient

• Specialist vs generalist models (11:24) - Axiom and Periodic Labs bet on specialist scientific models rather than waiting for general models to solve all domains

• AI compressing scientific timelines (12:13) - Fundamental breakthroughs that used to take 100 years to trickle into real-world economics can now happen faster with AI diffusing ideas across fields

• Benchmark scarcity problem (15:27) - While IMO-level benchmarks are abundant, PhD-level verification costs $1000+ per problem; theory building and library learning capabilities lack good benchmarks

• Natural Numbers Game for learning Lean (17:22) - Beginners can learn formal proof language through this Duolingo-style game; experienced users can contribute to Mathlib in underserved areas like topology

• Enterprise applications (18:09) - LLMs + formal verification is promising for regulated industries needing compliance; also useful for legacy code verification and hardware circuit testing

• 100,000x data gap (21:41) - There are over 1 trillion tokens of Python code but only about 10 million tokens of Lean code, creating a massive bottleneck for training

• Chicken and egg problem (22:19) - Auto-formalization is difficult because models haven’t seen enough Lean; manually coding proofs doesn’t scale

• AGI vs superintelligence plate analogy (24:24) - AGI expands the plate of capabilities toward all edges; superintelligence picks one point and goes directly there, like building an AI mathematician that might not write poetry

• AI for math as algorithmic pillar (26:06) - Axiom sees mathematical AI as the reasoning platform for all AI science applications

• Pattern Boost and mathematical discovery (31:06) - Codebases like Pattern Boost generate interesting mathematical examples that help researchers form new beliefs about problems

Mentions

Companies

• Axiom Math (0:35) - Carina Hong’s company building full-stack machine-checkable mathematical reasoning
• Google DeepMind (7:27) - Created AlphaGeometry paper that demonstrated synthetic geometry problem generation
• Meta FAIR (8:21) - Former employer of François Charton and Alberto Afarino, now at Axiom
• Periodic Labs (11:21) - Company founded by Liam that focuses on AI for real-world scientific testing
• OpenAI (11:09) - Mentioned as an example of a pure LLM company approach
• AWS (18:36) - Has its own neurosymbolic reasoning that enterprises use for compliance
• Stanford (9:29) - STP (Self-Play Theorem Prover) work using Lean workbook dataset
• Rubrik (17:00) - Previous Turing Post guest Anaka Gupta discussed enterprise security

Products & Technologies

• Lean (4:57) - Programming language for formal proofs; only ~10 million tokens exist vs trillions for Python
• Mathlib (17:36) - Largest math library in Lean; good coverage in algebra and analysis, needs work in geometry and topology
• AlphaGeometry (7:24) - DeepMind paper that synthetically generates creative Euclidean geometry problems
• AlphaProof (11:03) - Purely formal system approach that Axiom differs from
• Natural Numbers Game (17:22) - Duolingo-style beginner game for learning Lean
• Lean Workbook (9:36) - High school level math dataset used in Stanford’s STP work
• Pattern Boost (31:19) - Codebase by François for generating interesting mathematical examples
• Mini F2F (15:36) - Benchmark for high school/IMO level math problems

People

• Carina Hong (0:29) - Co-founder and CEO of Axiom Math, former research mathematician, attended Stanford Law
• François Charton (8:16) - Axiom colleague, formerly at Meta FAIR, works on mathematical discoveries
• Alberto Afarino (8:18) - Axiom researcher, formerly at Meta FAIR
• Thomas Wolf (13:40) - Author of “The AI Einstein” blog post about research vs competition skills
• Liam (11:41) - Founder of Periodic Labs, friend of Carina Hong
• Hardy (12:30) - Historical mathematician who worked with Littlewood at Cambridge
• Littlewood (12:31) - Hardy’s collaborator at Cambridge
• Erdos (28:21) - Mathematician who said “God has a book of the best mathematics”
• Grothendieck (27:17) - Mathematician whose theory building approach influenced Hong’s understanding
• Mitch Polinsky (29:24) - Hong’s professor at Stanford Law for law and economics seminar

Surprising Quotes

“Current models are trained by next token prediction. That isn’t exactly what’s going on when you’re doing mathematical reasoning. If you are a human mathematician, you don’t give an answer just because other people say that it’s correct.” — 1:14

“While there are more than one trillion tokens of Python code, there’s only probably about like 10 million tokens of Lean code. That’s 100,000 times data gap.” — 21:41

“I like the word superintelligence better always better than AGI… Superintelligence can be defined as domain specific. So I can be a super intelligent AI mathematician, right? It’s very hard for this super intelligent AI mathematician to fold laundry the best.” — 23:56

“Mathematicians are almost like truth seekers, messengers. They climb ladders to pick on the sweetest apples and then spread it to humanity… What Hardy used to apologize for in A Mathematician’s Apology, a sarcastic apology that ‘well my math’s just totally useless,’ turned out to be quite useful in fact for war.” — 28:35

“I think that math and intuition is closer to arts than to science.” — 30:58

Transcript

0:00 That fundamental science and fundamental mathematical discoveries are going to have transformative power. We are functioning in a space where we can create new knowledge to use the sort of machine generated object to guide human intuition.

0:23 Hello everyone and welcome to the Inference show by Turing Post. I’m very excited to be joined today by Carina Hong and she’s co-founder and CEO of Axiom Math, a fascinating new company that builds a full stack for machine checkable mathematical reasoning by turning math into a programmable verifiable language and using it to push towards self-improving AI which is super hard. Welcome Carina.

0:49 Hi, great to be here.

0:51 So, you know what’s jarring? I’ll start with a simple question. Everyone is talking about AGI and then I’m talking to my model and it says this meal is 400 calories, this meal is 350, the snack is 200 calories and then dinner is 350. Overall it’s 800 calories. You’re totally fine. And I’m just staring at it. So why is math so hard?

1:14 That’s a great question. I think you know current models are trained by next token prediction. That isn’t exactly what’s going on when you’re doing mathematical reasoning. If you are a human mathematician, you don’t give an answer just because other people say that it’s correct, right? Like currently machines are also trained on human preferences. It’s not exactly how human reasoning works. You can have very similar concept in a totally different problem. So just kind of looking at training data relating to that concept isn’t going to exactly help you.

1:50 We do see machines being good at some parts of math. For example, being almost like the secretary for a mathematician to look up citation, for example, to look up what has shown up in an ancient paper or even in a German mathematician’s notebook. That sort of retrieval and searching in the training data is something that machines are good at, but they’re really not great at coming up with new mathematical knowledge.

2:15 When it comes to arithmetics like the examples you give, it’s quite interesting that it gets that wrong or gets some basic linear algebra proof wrong. We also think that it’s reasonable to say that when the problem becomes very complex, when it’s a very much multi-step reasoning problem, when the tree gets very deep, models are going to struggle even more. So yeah.

2:37 Are you trying to build an AI mathematician that will be basically independent from a human? What are the steps that you need to make, what are the main bottlenecks? I know it’s a lot but give me an overview.

2:50 100%. At Axiom we believe there are some pillars that are important to the AI mathematician. We want a system that’s a prover system that can give mathematical proofs when it’s asked questions, that can do that very well, which is almost like the focus of some other formal math research work. To have a system that can come up with proofs that’s different from informal models - large language models give you just the numerical answer.

3:26 When we talk about math as a verifiable domain, what we want to see is it’s not just the numerical answer is verifiable because machine can grade that 957 is 957. What that misses is the intermediate steps. We want all the intermediate steps, the reasoning process to be verifiable as well. So that’s the prover system, number one.

3:48 Number two, we want the model to have a great knowledge base - know what’s already in the knowledge base and what is not. To be able to introduce new notes to the knowledge base as the prover generates more correct proofs, turning conjectures into theorems and even bringing in new definitions and concepts that are useful for coming up with new problems in the knowledge base. This knowledge base could have a graph structure, a citation-based knowledge graph.

4:20 Number three, we really want to have a conjecturer system, a model that can propose interesting new math questions. And then this conjecturer model is going to give the challenge to the prover model and the two of them can just talk and that forms a self-improving loop. The conjecturer can look at what the prover gets right and wrong and come up with entirely new curriculum of problems to help the prover model hill climb.

4:54 So these are the three parts and there’s also auto-formalization or the ability of turning natural language math into Lean, the programming language for proof, sort of intervening all these different parts. For example, one might have a really good knowledge base of informal mathematics - we need auto-formalization to turn that into a Lean knowledge base. One may have a good conjecturer that’s able to give some high-level intuitions, and also auto-informalization for example turning Lean code back into English.

5:28 I think that will be needed for the conjecturer. If it conjectures something in formal language and the prover may prove it in formal language, turning that adds to the existing human mathematics by kind of auto-informalizing it back into English and human mathematicians might find inspirations in that.

5:50 I would say just one final thing on the AI mathematician point is that while we believe this model is going to have incredible capability, having the model being able to collaborate with human mathematicians is also a really important part. We think that the human understanding and mathematical capability are sometimes different from what is difficult, what is easy from what a machine, an AI mathematician may think.

6:10 So there’s definitely a lot of collaboration space, right? Because if they’re good at exactly the same thing, they’re bad at exactly the same thing, then you might argue that when the AI mathematician becomes really super intelligent, why is there need for human mathematicians to exist? And the answer is like they’re good at very different things. So therefore, the collaboration and the synergy becomes incredibly interesting.

6:34 That’s incredibly interesting because I want to go back to this conjecture model and how even are you going to create this conjecture model because math is so endless and it’s just how it’s going to turn and just narrow that to conjecture. And also it’s somehow related I think to an intuition that a mathematician, a human mathematician can have. So I think it’s a very important topic of conjecture creation and also what role intuition plays here and how and even can you build it into a model.

7:11 Yeah 100%. I think my eureka moment, which is kind of “wow this is so amazing” that we are probably functioning in this space where we can create new knowledge, is the AlphaGeometry paper. AlphaGeometry paper by Google DeepMind. They have all the Euclidean geometry figures like triangles, circles, lines, intersection points turned into the symbolic language. They turn that into the vector-based language and then in fact generate de novo geometry problems by functioning in the vector-based language.

7:51 So they generate code snippets and what they do is they turn these into the geometry representation after they are done generating these new problems. So almost like extremely creative geometry problems are generated synthetically. That’s an incredibly powerful idea.

8:08 We have also seen in the line of mathematical discoveries work by my colleagues François Charton and Alberto Afarino. These are researchers that were previously at Meta’s super intelligence lab FAIR but currently at Axiom. They are able to use machine learning to generate very interesting constructions and examples that are not conjectures but these are just mathematical objects. And if you observe the underlying pattern of a family of them, the human mathematician they work with actually was able to come up with de novo conjectures.

8:46 So use these sort of machine-generated objects to guide human intuition. That’s what they do at discovery. The question of intuition is very big, it is very broad. It has I think one important part - the ability to generate these examples and constructions - and then the other parts be able to sort of synthesize them with the human, synthesize them and formulate interesting conjectures.

9:14 Or you could say that the model in the formal language space can generate synthetically new problems and statements by taking in a couple seed statements. And this is what people have been trying. For example, in STP, Self-Play Theorem Prover work from Stanford. They are looking at seed statements from a data set called Lean Workbook, a high school level math data set. And then they try to generate conjectures that are fully in Lean.

9:45 Then they have the prover model to actually try to give reward to the conjecture model. But obviously there are certain additional designs they need to do because one can easily imagine a case where the prover-conjecture system didn’t get anywhere - well is it the prover is too bad or is it the conjecture is too bad? This sort of difficulty troubleshooting or disentanglement is something that a lot of research is still in the works. I do think that by combining formal language, which is a different abstraction level, with informal, one has more space for conjecturing.

10:16 So Lean is a symbolic language, right?

10:17 Yeah.

10:20 Is it the return of symbolic machine learning?

10:22 That’s a great question. I think back then in the 1980s when people were quite excited about formal verification, we don’t have LLMs yet. Right now we do. We have large language models being good informal reasoners about general sort of high-level intuitions. They are able to kind of give rough sketch - like the paper “Draft, Sketch and Prove” is still good and sound. And then you have amazing code generation capability - that’s on the programming language side. And then you have Lean.

10:49 So I think three things coming together makes now a really good timing to build an AI mathematician using a hybrid method of formal verification and also informal reasoners. It’s not we’re not kind of taking the approach of AlphaProof, a purely formal system. We’re also not obviously a large language model company like OpenAI. We are sort of taking the strength of these two worlds and two abstractions, put them together.

11:16 Mhm. That’s very interesting. I also see a trend because you launched basically within days with Periodic Labs and both companies just blew my mind because of the problems that you try to solve. Do you see it as a trend that’s about specialist scientific models or will giant models eventually swallow all these domains? How do you think about it?

11:39 Yeah, I think that’s a very interesting question. I know Liam well, we’re friends and I am really excited about what they’re doing at Periodic as well. Periodic and Axiom build in a way on a similar philosophy that fundamental science and fundamental mathematical discoveries are going to have transformative power in the world.

11:58 In the past, fundamental science is almost overlooked because each fundamental breakthrough, it might take about 100 years to sort of trickle through to the real world economics, to have those implications in the commercial world. Now, because AI is compressing the timeline of everything, and the additional reason that a lot of the ideas in the past kind of stay in that narrow field, they don’t diffuse into other adjacent fields.

12:25 So if I’m a mathematician in the past, if I’m Hardy, I will work with Littlewood and I would stay at Cambridge University and never go see the world. I will not talk to this physicist or definitely not talk to that molecular biologist. So the top minds in mathematics and the ability to make fundamental theoretical breakthroughs are constrained within the academia’s ivory tower. They don’t even necessarily collaborate with other human mathematicians. Definitely, they’re not going to collaborate with applied scientists or even AI scientists.

13:04 We think of AI for math as also the algorithmic pillar of AI for science. We make the radical breakthroughs and then real world testing, which is something that I think Periodic and other companies are doing incredible work. They’re going to put the theory into empirical environment and then get the real world testing result and I think that cycle is going to be incredibly exciting.

13:26 The things that you’re going to build, how are they going to be evaluated and benchmarked? Because everyone is excited about IMO but I don’t think it applies to what you’ve built, right?

13:37 Yeah 100%. So I strongly recommend everyone to read a blog by Thomas Wolf called “The AI Einstein.”

13:44 I read it. Yeah, a fascinating blog. I mean the idea is Thomas is obviously a great, you know, like straight A student. He was talking about it in the blog and he realized that research and discovery sometimes are much longer cycles than say the exams or the competitions you have in school and it requires different skills - like besides just sort of character like grit and resilience. It requires different skills as well.

14:08 The ability to connect different fields, to think broadly in addition to deeply, the ability to sort of analyze close misses - like all the things that I think might work and it didn’t - like how can I perturb that idea a little bit and then get something else that’s useful, rather than like for example in an academic environment sometimes you’re not given that opportunity to do another shot.

14:31 I am actually quite fascinatingly the other kind. I was a horrible - I think like if I go to the IMO I would not be the top tier student. I mean I did win some Olympiad like I think the USAMO or the AIME level but not IMO level. On the other hand I was a reasonable research mathematician. I think the skills required are indeed different.

14:55 I would say that when it comes to building an AI research mathematician, capabilities such as theory building, such as library learning - which is introducing new concepts that will be helpful to construct the following lemmas or theorems - that becomes incredibly important. Theory building, as I mentioned, like over long context reasoning, instead of each problem as an isolated thing but rather a node in a big graph - these kinds of abilities become very useful.

15:27 And I think you’re right, we are lacking benchmarks. We are totally lacking benchmarks. We know that at the IMO level, the high school math level, the benchmarks are pretty much abundant. You have Mini F2F, you probably can have the model take the IMO exam, you can scrape some other country’s math Olympiad problems.

15:46 But when it comes to PhD qualifying exams, first of all, the cost of doing those benchmarks increases dramatically. Each problem’s proven solution costs something like $200 and then $300 and then PhD qualifying exam is going to be like a thousand, right? The cost is like 4x. The question of taste becomes relevant - how to construct the right curriculum of benchmarks.

16:12 Especially measuring serious mathematics ability is something that Axiom definitely aspires to do and then to be sort of a community leader in the space. We want to be able to have AI mathematicians that can do research in addition to winning, you know, bright high school kids’ competitions.

16:28 So you also plan to work on benchmarks in the world.

16:31 Mhm. That’s interesting. I always try to find something practical for my readers from every person who I talk to. So, what can it be from Axiom Math? I’m not sure because it feels very theoretical right now, but what can you offer that people can do related to math?

16:49 Yeah. So in previous episodes, what are these sort of practical discussions you’ve had? I would love to know more.

16:55 I just started but the previous interview was about security and reliability. So Anaka Gupta from Rubrik was telling me how for the enterprise what steps they need to consider first to be able to choose what to do next with security.

17:12 Yeah 100%. So I think two baskets. One for the individual audiences. If you are new to Lean, you haven’t heard about it, there’s this very good beginner starter game called the Natural Numbers Game that can pretty much like learning Duolingo but for the language of Lean to try and play with these exercises and learning.

17:31 If you have some familiarity in Lean, I think pick your favorite results in math and then just build it out. Like Mathlib currently has so much wonderful coverage in domains such as algebra and analysis, but in other domains such as geometry and topology and partial differential equations it’s not that many yet. So if on the way of formalizing your theory result that turns out to be say something in low-dimensional topology, you might be able to help build these dependencies that other people will find incredibly helpful.

18:03 That’s I think for the math audience. We are passionate about or curious about what you would do on the enterprise side. I think that the technology of large language models times formal verification - the “times” as in this intersection - is going to be incredibly promising in the coming years.

18:21 We know that a lot of the companies serving large enterprises, especially enterprises in heavily regulated industries, do need formal verification to sort of pass compliance regulatory checkmarks. And that’s actually why a lot of customers I think chose AWS which has its own neurosymbolic reasoning. I also know that there are a lot of unexpected applications of the technology of proving formal math proving and auto-formalization applied in these other areas.

18:58 So we at Axiom are very much excited to chat with folks who think there might be a synergy. We can definitely have conversations around it. We think formal verification for both software and hardware are going to be incredibly strategic areas to work on.

19:11 And so if you have, for example, legacy code that you want to replace, want to upgrade, and you want to make sure that they still cover all the critical business areas - like there’s no edge case that’s important missed - let’s definitely talk about what that looks like. If you think that there are certain hardware, like circuit property testing or hardware design, let’s definitely talk as well.

19:37 I think these are on the formal verification side. On the mathematical discovery side, which doesn’t involve Lean but it’s mostly the practice of generating interesting constructions, examples, mathematical objects that are incredibly relevant to some very deep research open problems and also deeply relevant to the real world like graphs. If you are having a particular kind of graph theory problem in mind in logistics routing, let’s definitely talk as well.

20:06 So I think there are a lot of things to be sort of defined and that is not opening new use cases and market - that is just scaling the power of LLM-assisted formal reasoning in these existing areas. Scaling more reasoning in these existing markets to win, and then there will definitely be new use cases but that’s kind of like a second phase.

20:25 That’s very interesting. From what I hear it feels like you do a lot of sort of cross combination of different sciences. So in your company in Axiom Math, is there a space for experimentation in that sense? How do you do that? Do you like invite people from machine learning, from computer vision, from there, from symbolic? How do you experiment? If you do.

20:49 So we don’t do any wet lab experiments, right? The sort of real world testing part - we don’t do that. We’re focused on developing the algorithmic pillar of this pretty exciting brand new world. So our technology is focused on building a really strong AI system that can do formal math and apply to other areas really well. That’s kind of how I would say we define it. The experiments you’re talking about, what I think I understand, are like partnerships or…

21:17 No, I mean like you use symbolic machine learning, you use neural networks, so it’s already a combination of things to build what you’re building. Maybe we should talk about bottlenecks then - to build what you’re building and the roadblocks that you have, what are they first and how do you solve them?

21:35 I think there are a few bottlenecks. One is data scarcity. So while there are more than one trillion…

21:41 Yeah there are more than one trillion tokens of Python code. There’s only probably about like 10 million tokens of Lean code. That’s 100,000 times data gap. So I think that’s one problem that one is actively navigating as a sort of corollary of that because models have not seen much Lean.

22:03 The ability to auto-formalize - translating, or I guess translating is always not the right word because it’s such a technically stubborn problem - the process of converting the natural language math into Lean is going to be difficult just because they haven’t seen much. So you have a cold start problem, almost chicken and egg.

22:21 So I think data scarcity, and we definitely do not want to just pay Lean experts to manually code all the proofs into Lean - that does not scale that well. So I think that’s one bottleneck.

22:36 We are facing at Axiom, we have three pillars we believe are important to the vision: AI, programming languages, and math. So therefore on the talent side, when you talk about the folks who are working in other parts of computer science, we have very much good applied AI people and we also have very good programming languages, compilers people. We also have great mathematicians - both informal mathematicians, as in mathematicians who do work with English, and mathematicians who are the pioneers of building out Mathlib, the largest math library in Lean.

23:11 So that’s kind of the crowd we have to climb this pretty difficult challenging mountain. Besides data scarcity, I think that there are also other bottlenecks. For example, as I said, the problem of conjecturing and intuitions is very, very much difficult. It requires very good experiment design. The startup sort of environment - we definitely want to accelerate all these different directions with the constrained resources we have. So it’s all very exciting. Things are very fast-paced and even creative sometimes.

23:45 That might be crazy pace. I wanted to get back to AGI. What is your thinking about AGI and superintelligence? Do you think formal reasoning is essential for AGI?

23:56 I like the word superintelligence better, always better than AGI because…

24:01 I don’t know really the difference. They are so similar in a sense.

24:04 I think superintelligence can be defined as domain specific. So I can be a super intelligent AI mathematician, right? It’s very hard for this super intelligent AI mathematician to fold laundry the best. I think it’s not quite general in a way.

24:21 The thing with AGI is I don’t quite know what it means. And I think the difference could be that if you think about the world of problems, that’s like a plate. And then in the middle you have the easy problems like 1 + 1 equals 2, print “hello world.” And then at the edge you have many different points - maybe the north point is “cure cancer” and the west point is “solve the Riemann hypothesis,” the south point can be “write a novel that’s going to win the Nobel Prize in literature” or you know be the generational fiction work.

25:00 Folding laundry - it’s a very hard task!

25:02 Sure yeah! But something even better than that - like the sort of ultimate question of physical intelligence. The AGI concept seems to be that from the center you enlarge the plate slowly, and you’re betting on the system that does really well in writing the Shakespeare equivalent work that can also solve the Riemann hypothesis and cure cancer. That to me feels like AGI - like the plate just keeps being enlarged to the edge.

25:34 I think for me superintelligence is: hey I pick a point in the middle and then I pick the goal and I just go there - like I just go there in one line. And that’s what Axiom is doing. We’re very much bullish in building a super intelligent AI mathematician, but I’m not bullish about my model being good at poetry. Like in fact, I see my model might not be very good at poetry. So I think that might be sort of the difference.

25:55 Yeah, that’s kind of related to the question about Periodic Labs and Axiom Math and the bet on specific models or general models. So you definitely bet on the specific models.

26:06 Yeah, I bet on the specific model. I also bet on AI for math being the algorithmic pillar, the reasoning platform of AI for science. And that’s going to be - I believe that both Axiom and Periodic, like these two companies, are working on incredibly important things and that’s going to be the future. I think that’s going to be the next frontier in AI - AI for math, AI for science.

26:28 That’s very interesting. So my last question is usually about books. So what book has formed you or influenced you recently? It can be either your childhood or something recent as I said.

26:41 That’s a wonderful question. I read perhaps too many math books for better or for worse. So they are not the most interesting to talk about. Okay, let me answer this for math books and not math books because this is going to be fun.

26:56 For the math books, I think algebraic geometry textbooks. So some people use Hartshorne, some people use Ravi Vakil’s “The Rising Sea.” I use The Rising Sea just because I’m not smart enough to understand the Hartshorne one - like The Rising Sea has a lot more very illustrative examples. It’s a book that sort of formed me - it helps me understand what Grothendieck means by theory building.

27:19 Once you introduce the concept of schemes, you’re able to understand things in a completely different perspective. And algebraic geometry is I think a perfect example of a theory building rather than problem solving type of mathematics.

27:32 On the other hand, I think there are books such as Davenport on analytic number theory that introduces a lot of tricks to help you problem solve, to help you set bounds. There are Gauss sums kind of arguments, Weyl inequality type of arguments to help you calculate. When you see an inequality in analytic number theory, they’re almost like reflexes in your brain - “what next?” In that way it has sort of changed math to a more finite search space like Go and chess rather than an infinitely exploring one.

28:08 So I think these two books, each teach me a very different lesson. And when I was a kid I loved “Proofs from THE BOOK” - it was wonderful. The idea that God has a book - and this is an Erdos quote - that God has a book of the best mathematics and then there are like proofs from THE BOOK that we can now read feels almost like a very spiritual experience for me.

28:30 In that mathematicians are almost like truth seekers, messengers. They climb ladders to pick on the sweetest apples and then spread it to humanity - to bolster these mathematical truths into different things. Plant a really great number theory breakthrough and then you have implications in cryptography. What Hardy used to apologize for in “A Mathematician’s Apology,” a sarcastic apology that “well my math’s just totally useless” - turned out to be quite useful in fact for war. That’s just fascinating to me.

29:08 On the non-math side, I love actually a lot of humanities and social science things. I did law school for two years before I took the…

29:15 That’s why you like Thomas Wolf.

29:19 Yeah. Yeah. I love reading about law and economics. I think Mitch Polinsky’s work is really wonderful and having him as my professor in the law and economics seminar at Stanford Law was a great experience - like learning from those who write the textbooks and modeling the effect of certain laws and policies on deterrence versus retribution. That’s just fascinating to me.

29:46 On the literature side, there’s this book about a generation of Chinese writers and artists. They all live in the same hutong complex in Beijing and it’s almost like the French salon in Renaissance time. These people communicate ideas and bridge between different fields. The one who’s an architect can say something that somehow inspires the one who produces beautiful artworks and the craftsmanship that flows through this conversation.

30:23 And how they were almost kind of collectively having pain and suffering during the Cultural Revolution. I think that was another book that sort of shaped my personality in that I always aspire for art, for artistic expressions and creations. And I think that math and intuition is closer to arts than to science. How do we sort of scientifically understand that? It’s fascinating. The book is called something about the hutong - it’s about specifically that location, that address. So I think it’s a very interesting book.

30:54 I love these recommendations. I came up with the question about practical stuff. As a human mathematician, can you give an idea how to use AI so everyone can do that, math related?

31:06 There are code bases for mathematical discoveries. The way to interact with them is not exactly how you prompt a large language model but instead to work with people who are developers of these toolkits to really ponder very hard open math questions.

31:23 These two code bases I want to highlight are work of my colleague François. He has been collaborating with many mathematicians and theoretical physicists on using Pattern Boost to generate interesting examples - which is generative methods. And the other one is the translative method - translate problems to solutions. The other ones can generate a family of interesting mathematical objects and then the purpose is for this to be very interactive.

31:55 So if I’m a mathematician and I see a lot of graphs being generated, I might have beliefs about the problem that I didn’t know before. I would encourage folks to just try to get in the mix. And there are AI for math conferences throughout the year - like since Oberwolfach to I think the next one is going to be JMM and after JMM there’s like Aarhus - that some of them Axiom is co-organizing.

32:22 So I think get in the mix, talk to people who are doing frontier work in AI for math discovery and see what problems that previously felt not tractable are suddenly perhaps within the grasp.

32:33 That’s amazing and very fascinating. And thank you so much. It was very interesting. And I love it.

32:44 [music]