Short answer: Carina says Axiom is building a prover and a conjecturer that form a self-play loop, plus auto-formalization that turns math into Lean, a programming language, so results are verifiable like code.
Watch this answer from Episode 22 (starts at 9:26) · Episode 22 notes and transcript
From Episode 22: Let's do the Math!, starting at 9:26.
Jordan Metzner [9:25]: Okay, Carina. So obviously, super young entrepreneur, super excited about your new round of investment, but let's start from scratch. Tell us, like, how did this whole thing come about? What is Axiom? And what are you guys doing every day?
Carina [9:38]: Axiom is, I think, the coolest AI for math company
Jordan Metzner [9:40]: Awesome.
Carina [9:41]: In my opinion. We are building an AI mathematician, a model that can not only do do really well on benchmark problems, those Olympiad math problems that we just saw, but also develops capabilities that are like a research mathematician, including the ability to conjecture, which is to propose new problems, unseen problems, hypothesis, and the same system can then try to prove and verify in addition to solving these problems. So a prover and a conjecture talking to each other, forming the self play loop like we talked about in our vision blog. Additionally, this system can also auto formalize, which is to convert the massive amount of math corpus data into lean, turning math into programming language, which, have a lot of great technical advantages because we have seen reinforcement learning, all verifiable domains like coding, having achieved incredible breakthroughs. So by combining AI, math, and programming language, all three pillars together, we believe to see the same sort of step function jump in math capabilities, especially real mathematics, serious mathematics beyond the benchmark that a lot of models have seen.
Jordan Metzner [10:58]: So that's obviously incredibly interesting. Math, obviously, historically was run on CPUs. Right? So the movement of running math equations onto GPUs is really this big jump. Right? And the ability to essentially kind of find new opportunities within the mathematical field. Is that a good way to say it?
