验证式 AI：通过形式验证扩展智慧

但我觉得，这是第一次，验证式 AI 是为了开启协作。要么是人机协作。之前，蓝图阶段是人人协作，而 Lean 是基础，是验证的形式化语言。然后是人机协作，就像我们现在看到的，未来是智能体与智能体之间的协作。我认为验证式 AI 是为了开放，不是为了满足封闭行业的需求。而且我觉得验证不应该是——哦，我记得有篇文章说聊天机器人会编造数学答案、产生幻觉。对我来说，验证不是关于损失，而是关于扩展 brilliance、复合 brilliance。所以回到协作这一点，就像拉马努金成为一个更强的数学家。他本来就很强，但验证帮助他扩展了 brilliance，既向上扩展也向外扩展。

But, for the first time now, I think verified AI is to open up collaboration. Either it's human-AI collaboration. Before, with blueprinting, that was human-human collaboration. And Lean was the grounding, was the verification formal language. And then human-AI collaboration like we're seeing now, future AI agent-agent collaboration. I think verified AI is for openness. It's not for meeting the requirements of closed industries. And I think verification should not be about, oh, I remember there's an article about chatbots making up math solutions, hallucination. Verification to me is not about lossiness. Verification to me is about scaling brilliance, compounding brilliance. So, going back to the collaboration point, it's about Ramanujan being a much stronger mathematician. He was already a really strong one. But verification helps him extend the brilliance. Like both scale up and scale out.

欢迎收听 Latent Space AI for Science 播客。我是 Brandon Anderson，在 Atomic AI 从事 RNA 疗法研发。同台的还有 RJ Honicky，Mira Ox 的 CTO，专注于空间转录组学。很高兴邀请到 Axiom Math 的 CEO 兼创始人 Karina Hong。Axiom 在多个领域引起了轰动。首先，他们去年 12 月在 Putnam 竞赛中获得了满分。他们还声称是第一个使用形式化验证证明研究猜想的 AI。而且我很兴奋，他们昨天刚刚宣布了一轮相当大的 A 轮融资。欢迎来到节目。

Welcome to the Latent Space AI for Science podcast. I'm Brandon Anderson. I build RNA therapeutics at Atomic AI. And I'm joined by RJ Honicky, the CTO of Mira Ox, working on spatial transcriptomics. It's a pleasure to have Karina Hong, CEO and founder of Axiom Math. Axiom has made a splash in several different areas. First, they got a perfect score in the Putnam last December, I think. They also have the claim of the first AI to prove research conjectures using formal verification. And I'm very excited they just yesterday announced a quite a large series A. Yeah, welcome to the show.

谢谢邀请。

Thank you for having me.

你们刚刚融资 2 亿美元，正如你的一位同事所说，这基本上相当于美国每年数学研究的全部预算。这是真的吗？

You just raised $200 million, which as one of your colleagues said, this is like basically the entire US math budget for math research each year. Is that true, actually?

根据他的 LinkedIn 帖子，是的。

According to his LinkedIn post, yeah.

显然每年数学预算是 2.5 亿美元。我们应该在数学研究上投入更多。

$250 million is apparently the annual math budget. We should spend more on math research.

是啊，有点可悲，但我知道。

Yeah, it's kind of sad, but yeah, I know.

但无论如何，作为一个热爱数学的书呆子，这真的很酷。但这让我震惊。比如，什么？当我听到这个，我就想，好吧，2 亿美元对应 16 亿美元的估值？我不知道。

But anyway, as a nerd who loves math, it's really cool. But that kind of blew my mind. Like, what? When I heard that, I'm like, okay, so how is that $200 million against $1.6 billion valuation? Yeah, I don't know.

嗯，非常高兴来到这里。而且，我觉得这是 A 轮融资，所以这是一个非常及时、有趣的播客。我们是一家成立七八个月的公司，所以这对我们意义重大。这是一个很酷的里程碑。我们目前大约有 30 人。所以，这笔资金将为我们提供所需的燃料，加速我们迄今为止强劲的执行势头。我认为人们以多种方式看待我们。有人认为我们是一家数学初创公司，一家 Lean 初创公司。我们做的另一件显而易见的事情是形式化验证。我们认为验证是数学的一个非常好的第一市场。所以，我认为这笔资金将让我们探索一些应用领域，正如我的同事 CTO Shumo 在发布视频中所说：它让我们拓宽梦想。

Yeah, well, super excited to be here. Also, I think this is a series A, so it's a very interesting, timely podcast. We are like a 7-8 months old company, so it definitely means a lot to us. It's a really cool milestone. We're currently about 30 people now, right? So, going into this amount of funding will give us the fuel we need to accelerate the strong execution momentum we have so far. I think people think of us in many ways. People think of us as a math startup, a Lean startup. The other obvious thing we do is formal verification. We think verification is a really good first market for math. And so, I think this funding will let us explore some of the applied domains, as my colleague CTO Shumo said in the launch video: it lets us broaden our dreams. So, yeah.

但 2 亿美元和 16 亿美元的估值，这怎么会有市场呢？我的意思是，显然你们不只是为了证明东西的乐趣而做这件事，尽管我确信其中有很多乐趣。

But still, $200 million and a $1.6 billion valuation. How is there a market for that? I mean, obviously, you're not doing this just for the fun of proving things, although I'm sure there's a lot of that.

那么，让我们回到 2024 年。当 o1 类模型刚出来时，Anthropic 当时在秘密做什么？是编程。每个人都知道他们在做编程。OpenAI、Meta、Anthropic，所有人都完全知道 Anthropic 在做编程。但他们忽略了。他们想，“哦，他们在做 B2B 玩法，他们只想要一个垂直领域。”人们认为编程是一个垂直领域。现在看看我们今天的位置。编程从编程到推理有很强的迁移学习，基本上到了推理的未来。我认为这非常令人震惊。当时做编程的人相信一些我们现在对数学和 Lean 同样相信的东西：如果你有更结构化和形式化的数据，它会比我们正在处理的特定垂直领域更具水平性。所以，如果我们今天以形式化的方式做数学，比如标准的思维链数据，基于人类偏好训练一个数学模型，那么我会说，也许我们只是一个数学初创公司，对吧？但在我们追求数学的同时，我们也在做对其他领域有迁移学习的事情。所以，我认为这是更大的图景：虽然公司的 DNA 仍然是数学，我们所有人都是数学书呆子，这是一个非常强烈的文化声明，每个人都有让 AI 成为超人数学家的伟大使命，就像我们在 Putnam 和研究猜想中看到的那样。事实上，我们还有另一批成果即将到来。我们也认为这将是验证式推理的基础。我们谈了一点验证式 AI。接下来我想多谈谈验证式 AI，因为我觉得你还有另一个……

So, let's bring us back to 2024. When o1-like models just came out, what was Anthropic kind of secretly working on back then? It was coding. And everyone knows they're working on coding. OpenAI, Meta, Anthropic, everyone had full knowledge that Anthropic was working on coding. And they just overlooked it. They thought, "Oh, they are at B2B plays. They just want one vertical." People think of coding as one vertical. And now look at where we are today. Coding kind of had strong transfer learning from coding to reasoning to basically, in the future of reasoning. And I think that's really shocking. The people who were working on coding back then believed in something that we believe similarly with math and Lean now, which is that if you have more structured and formal data, it's going to be a lot more horizontal than the specific vertical we're tackling. So, if today we are doing math in a formal way like the standard chain-of-thought data, train a math model based on human preference, then I would say, perhaps we're just a math startup, right? But while we are pursuing math, we're also doing things that do have transfer learning to other domains. So, I think that's the broader picture: while the DNA of the company remains math and all of us are math nerds and this is a very strong cultural statement, everyone has a great mission of having AI be a superhuman mathematician like we're seeing on Putnam and research conjectures. In fact, we have another batch coming. We're also thinking that this is going to be fundamental to verified reasoning. And we talked a little bit about verified AI. I want to talk a little bit about verified AI next, because I think you have another...

是的。我想听听关于验证式 AI 的内容。我确实想深入一点。那么，我们是否知道 Anthropic 和 OpenAI 以及其他所有人没有在做形式化验证，并将其用于他们的发布等？

Yeah. I want to hear about the verified AI. I do want to dig in a little bit. So, do we know that Anthropic and OpenAI and everyone they're not doing formal verification and using that for their rollouts and whatever?

我认为我有很多小道消息，可能不应该公开记录。我觉得研究人员会交流，他们打牌，等等。但无论他们做还是不做，都有非常有趣的原因。我认为我得到的要点是，如果你在一个前沿实验室，方向实际上会因为很多你无法控制的原因而改变很多。所以，我想带我们回到 AlphaProof 的时刻。AlphaProof 是一个如此惊人的成果。2024 年 42 题中答对 28 题的表现对我来说是 IMO 时刻。不是 2025 年的围棋，因为在 2024 年和 2025 年，AI 模型可以解决所有非组合数学的问题。唯一的区别是，如果你解决了所有非组合数学的问题，2024 年得 28 分，2025 年得 35 分，因为 2025 年只有一个组合数学问题。在 AlphaProof 之后，我们没有看到 Google DeepMind 很多形式化数学的结果或进展，这实际上是因为一些不一定是技术上的原因。

I think I have a lot of rumor mill that probably shouldn't put on the record. I think researchers talk, they play card games and yeah. But there are really interesting reasons if they are or are not doing it. I think that's the takeaway I have, which is that if you're at a frontier lab, the direction actually does change a lot for lots of reasons beyond your control. So, I want to bring us back to the AlphaProof moment. AlphaProof was such an amazing result. The 2024 28 out of 42 performance was the IMO moment for me. It was not Go in 2025 because across 2024 and 2025 AI models could solve all the problems that are not combinatorics. The only difference is that if you get all the problems that are not combinatorics, you get 28 in 2024 and 35 in 2025 because there's only one combinatorics question in 2025. After AlphaProof, we didn't see a lot of formal math results or progress from Google DeepMind, and that's actually because of reasons that are not necessarily technical.

但如果你在一家初创公司，专注于形式化数学和验证 AI，那么你就能长期研究一个非常酷的问题，并且在取得进展和突破方面，成功的可能性要大得多。

But if you're at a startup and you have very singular focus that is formal math and verified AI, then you get to work on a really cool problem for a long time and you have a much higher likelihood to get to where you want to be in terms of progress and breakthroughs.

那么，请为我们定义一下。

So, yeah, just define that for us.

是的，很多人认为形式化验证是一门古老的学科。它早在深度学习之前就存在了，在基于规则的计算机科学时代。自 1980 年代以来，形式化验证一直受到大力推动。有一些有趣的历史轶事，比如巴黎工会要求地铁系统的自动切换必须经过形式化验证以确保安全。所以，工会对技术的要求相当有趣。

Yeah, a lot of people think about formal verification as an ancient subject. It existed way before deep learning, in the time of rule-based computer science. There's been a strong push for formal verification since the 1980s. There are interesting historic anecdotes, such as the Paris trade union demanding that the automatic switching of the subway system be formally verified for safety. So, quite interesting trade union for technology.

嗯。

Yeah.

在挑战者号事件前后，欧洲航天局都在使用形式化验证来验证阿丽亚娜航天器。这也很引人注目。波音和空客也使用形式化验证。近年来，亚马逊云服务（AWS）大力推动自动化推理，因为他们有很多企业客户，这些客户要求 100% 验证，不能遗漏任何边缘情况。常规测试无法满足需求。所以，很多人认为验证很烦人，像税收和合规一样，只是为了确保一切就绪。但事实并非如此。我们谈到验证；我认为我们的竞争对手在推出产品时，在幻觉时代谈论了形式化预推理。对他们来说，形式化验证是关于损失和幻觉的。对我们来说，验证 AI 是关于卓越——它是关于 Scaling（规模扩张）和复合超级智能。这是一个深刻的观点，有时需要一点解释。

Around the time of Challenger, both before and after, the European Space Agency was using formal verification for the Ariane spacecraft. It's also interesting. Boeing and Airbus use formal verification. And in more recent years, there's been a lot of push about automated reasoning at AWS because they have many enterprise customers that really require things to be 100% verified, with no missed edge cases. General testing doesn't satisfy the need. So, a lot of people think about verification as something annoying, like tax and compliance, making sure we are good to go. That's really not the case. We talked about verification; I think our competitor, when they launched, talked about formal verification pre-reasoning in the time of hallucination. For them, formal verification is about lossiness and hallucination. For us, verified AI is about brilliance—it's about scaling and compounding superintelligence. This is a deep point and sometimes takes a bit of explanation.

如果你想想卓越，比如拉马努金。他是一位杰出的数学家，在学会证明之前，仅凭直觉就能发现许多有趣的公式。他去了剑桥，与哈代和李特尔伍德合作。在著名电影《知无涯者》中，有一条故事线讲述了哈代如何艰难地迫使他不再依赖直觉，而是去做证明。学会写证明后，他成为了一位更强大的数学家。他的直觉变成了定理，后代的数学家在这些定理上继续构建。所以，这是一种 Scaling（规模扩张）和复合我们已有智能的方式。

If you think about brilliance, for example, Ramanujan. He was a brilliant mathematician who could find many interesting formulas just by intuition, before he knew how to do proofs. He went to Cambridge, worked with Hardy and Littlewood. In the famous movie "The Man Who Knew Infinity," there's a storyline about how hard it was for Hardy to force him to no longer rely on intuitions and to do proofs. After he learned proof writing, he became a much more powerful mathematician. His intuitions turned into theorems, and future generations of mathematicians built on those theorems. So, it is a way to scale and compound the intelligence we already have.

另一个例子：数学家们几千年来一直在用英语或各自的语言写代码。为什么我称之为写代码？因为有一个严格的逻辑推演社区标准。每一步都必须正确，否则你会被数学界排斥。

Another example: mathematicians have been writing code in English or their respective natural languages for thousands of years. Why do I call it writing code? Because there's a community standard of rigorous logical deduction. Everything has to be step-by-step correct, otherwise you get ostracized by your math community.

社区里规则更多。

More rules in the community.

所以这很有趣，因为那是人类数学家强制执行的，对吧？这是一个纯粹的评审过程。目前一篇论文的同行评审需要两年时间。但像 Lean 这样的证明助手和形式化证明检查器仍然找到了自己的位置。为什么？如果我是一名数学家，我的工作可以由其他人类同行评审，为什么数学家还要玩 Lean？为什么我们要谈论基于 Lean 的辅助定理证明？因为它处理的是底层细节。例如，我们甚至不是在谈论 AI。我们谈论的是 Lean 中的一个策略，叫做“grind”。它目前可以在非常低的层次上处理许多数学证明。这相当令人震惊。我看到另一家在同一领域工作的公司，他们的一些演示实际上完全可以由 Lean 中的 grind 策略处理。

So it's interesting, because that is human mathematician enforced, right? It's a pure review process. Peer review of a paper currently takes two years. But proof assistants and formal proof checkers like Lean still found their place. Why? If I'm a mathematician and my work can be peer-reviewed by other humans, why do mathematicians even play with Lean? Why do we talk about Lean-based assisted theorem proving? It's because it handles the low level. For example, we're not even talking about AI. We're talking about a tactic in Lean called "grind." It can currently handle a lot of math proofs at a very low level. This is pretty shocking. I've seen another company working in the same space, and some of their demos can actually be completely handled by grind, which is a tactic in Lean.

你能向非专业人士解释一下什么是 Lean 吗？

Can you explain what Lean is to non-experts?

好的。我觉得顺序有点不对。Lean 是一个计算机程序，有点像用于数学证明的。它是一种形式化语言，就像它的同类 Isabelle、Coq、Rocq，以及其他一些远亲如 Dafny、Agda——这些形式化语言，整个领域。

Yeah. I think our order is a little wrong. So, Lean is a computer program, a bit like for math proofs. It is a formal language, just like its cousins Isabelle, Coq, Rocq, and some other further cousins like Dafny, Agda—these formal languages, a whole sector.

它做什么？

And what does it do?

基本上，如果你在 Lean 程序中写了一个证明，并且假设没有奇怪的事情发生——比如意外使用了“sorry”这个策略，它让你想当然——假设一切安全，那么一旦你执行那个程序，一旦它编译并告诉你它是正确的，那么这个证明就确实是正确的。

It basically, if you have a proof written in the program in Lean, and assuming there are no weird things happening—like unintended use of "sorry," which is a tactic that lets you take things for granted—assuming everything is safe, then once you execute that program, once it compiles and tells you it's correct, then the proof is actually correct.

所以，它就像一个类型检查器。

So, it's like a type checker.

是的，它基于一个叫做 Curry-Howard 同构的结果，它将证明转化为程序。所以，我想谈谈 Lean 的魔力。为什么我认为它是一个非常好的编程语言，因为一方面，如果你完全不在乎形式化部分，不在乎逻辑部分，你只想用 Lean 写代码，你可以。我们有候选人目前在 Lean FRO 工作，他在我们的面试过程中用 Lean 写了 AutoGrad。

Yeah, it's based on a result called the Curry-Howard correspondence, which turns proofs into programs. So, I want to talk about the magic of Lean. Why I think it's a really good programming language is because, on one hand, if you don't care about the formal part at all, if you don't care about the logic part, you just want to use Lean to write code, you can. We have had candidates who currently work at the Lean FRO, and he wrote AutoGrad in Lean during our interview process.

那么，它是一种图灵完备的语言吗？

So, is it a Turing-complete language?

没错。所以，你可以用 Lean 做很多事情。它是一种函数式编程语言。你也可以用它来做代码和数学。二合一。

That's right. So, you can do a lot of things with Lean. It's a functional programming language. And you can also use it to do code and math. Two in one.

好的。

Okay.

回到我之前的观点：如果数学家已经在强制执行大多数证明是正确的——也许不是所有数学家，但象牙塔和学术界的人——为什么我们还需要 Lean 这个模型检查器？这是因为 Lean 有策略可以帮助他们处理底层的计算或推演，这样他们就能在高层次的直觉空间中导航。这就是我的观点：形式化验证或验证 AI 不仅仅是为了处理或剔除损失、幻觉和错误。它是关于 Scaling（规模扩张）卓越。

Going back to what I was getting at: if mathematicians are already enforcing that most proofs are correct—maybe not all mathematicians, but the ivory tower and people in academia—why do we even need Lean, the model checker? It's because Lean has tactics that help them handle the low-level calculation or deduction, so they can navigate in the high-level intuition space. This is my point: it is not about formal verification or verified AI just handling or kicking out the lossiness, the hallucinations, the mistakes. It's about scaling brilliance.

这是关于超级智能的。

It's about superintelligence.

实际上，陶哲轩有一个很棒的视频，关于使用 Lean 作为一种协作方式，因为你可以用它……抱歉。

I actually Terrence Tao has a great video also about using Lean as a way you can collaborate because you can use it... Sorry.

没错。这正是我想谈的另一点。很多人认为我们的市场必须是某个非常小众的工业安全关键领域。不，那不是 TAM。TAM 是所有代码。TAM 是对所有 AI 生成代码的优先选择权。优先选择权意味着你可以选择是否要验证它。所以这是我想强调的重点——人们认为形式化验证很痛苦，因为它有各种严格的要求。

Exactly. That's another point I want to talk about, right? A lot of people think about, you know, what is our market? It has to be some really niche industrial safety-critical area. No, that's not the TAM. The TAM is all code. The TAM is a right of first refusal on all AI generated code. Right of first refusal meaning, you know, you get to choose whether you want to verify it. So this is the important part I want to kind of come across, which is that people talk about formal verification as almost like painful because it has all these stringent requirements.

到目前为止确实如此。

Up until now it has been.

嗯，是的。对我们来说，验证生成实际上意味着性能提升。它意味着更高的样本效率。意味着像我们这样的初创公司——虽然我们融了一些钱，但算力预算和数据预算都比前沿实验室少——能够匹配甚至超越超人类任务的性能。事实上，在 2025 年 12 月我们实时参加的 Putnam 考试中，MASS Arena（一个评估许多 LLM 的组织）发现最好的 LLM DeepSeek 得了 103 分（满分 120 分）。最好的人类——我们现在知道是来自 MIT 或芝加哥的学生，具体哪个不确定，因为他们不公布前五名的分数——得了 110 分，而我们得了 120 分。这是第一次，我记得我们刚开始时人们问：一个形式化数学系统，数据量少几个数量级，怎么可能匹配或超越非形式化 LLM？Putnam 是第一次它赢了。所以我们不只是考虑痛苦和挑战。我们考虑的是验证生成的性能提升、改进。就像你会期待 RL 对 Lean 有改进一样，因为看到了 RL 编码的证据。所以这是我想说的第二点：如何看待验证型 AI。

Well, yes, yes. And to us it's actually verified generation means performance gain. It means higher sample efficiency. It means a startup like us with, you know, still we raised some money but lesser compute budget, lesser data budget than frontier labs will be able to match and even exceed, you know, performance on superhuman tasks. In fact, for the Putnam Exam that we just competed December 2025, which we did in real time, MASS Arena, which is this organization that evaluates a lot of LLMs, found the best LLM, DeepSeek, got 103 points out of a 120 point exam. The best human obviously we now know is a student from either MIT or Chicago, we don't know which one because they don't announce the top five winner score, got 110 and we got 120. So it's the first time actually I remember when we were starting this people were like, is it even possible that a formal math system with so much orders of magnitude less data can match or beat an informal LLM and Putnam is the first time it beat. Right? And so we're not thinking about it just about the painfulness, the challenges it poses. We are thinking about the verified generation performance gain. The improvement. The fact that you can, you know, just like you would expect RL for Lean to have improvement because of seeing evidence of RL encoding. So, this is the second point I want to make about how to think about verification verified AI.

那么，也许我们可以谈谈为什么。你能描述一下你们所做的与前沿实验室——至少在他们构建标准 RL 增强型 LLM 时——有什么不同吗？你们做的有什么不同？

So, maybe we can talk a little bit about why. Can you describe what is different about what you do versus what the frontier labs, you know, at least when they're building their standard RL enhanced LLMs? What's different about what you do?

是的。我们严重依赖一种叫做 Lean 数据的数据。我们谈到 Lean 是指我们拥有的所有 Lean 证明数据，你知道，它是正确的。所以你知道它是否正确，这很重要。所以我们有一个模型系统。这些模型是经过后训练的，使用 RL 或 FFT。

Yeah. So, we heavily rely on kind of data called Lean data and we kind of talked about Lean as all the data that we have that's Lean proofs, you know, it correct. So, you know it's correct or not and that's quite important. So, you know, we have a system of models. These models are post-trained and using RL or FFT.

所以，LLM 就像是某种现成的基础模型，你拿来进行后训练或持续……

So, LLMs found like some sort of foundation model that you get off the shelf and you post train it or can continuous...

是的，显然倾向于开源基础模型，比如……

Yeah, and there's obviously inclination for open source, you know, base models like...

它懂英语吗？

Does it speak English?

是的。

Yeah.

可能还会编程。

Probably knows how to code.

是的。

Yeah.

但你也对它进行微调或持续……

But it also you fine tune it or or continue...

是的，基础模型可能和其他人用的类似。如果他们不进行预训练的话。是的。

Yeah, and the base model may be similar to what everyone else is using as well. Right. If they're not kind of pre-training their model. Yeah.

然后我们基本上做这个，就是针对形式化数学的 RL。我认为有一个标准流程或行业技巧。我们尽量创新。我们发现推理的 Scaling 几乎没有规律，递归地将证明目标分解成许多子目标，并学习回溯。

And then we basically do this, you know, RL for formal math kind of. There's I think a standard pipeline or like, you know, tricks of the trade that people use. We try to innovate really kind of as much as we can. I think that we found scaling inference to have almost no law recursively decomposing you know, a proof goal into many sub goals and learning to backtrack as well.

是否存在这样的风险：你从某个领域的数据集开始，然后递归地展开，但所有训练数据都局限在某个领域，可能只是从初始训练数据对数增长到更大的空间。所以你可能会被困住——你可能非常擅长这个，但你只是创造了一个巨大的锯齿状前沿，其他领域离得很远。

Is there a risk that like you start out with this, you know, what you know in a certain domain of data sets and so on and then you start rolling out, you know, recursively in a space but now all of your training data is localized in some domain that you still is only so like maybe logarithmically in some large space growing from your initial training data. So, you could get trapped essentially in that you know, you could be really good at this, but you just created a big jagged frontier where some other domains are just far from them.

我们在讨论分布偏移。所以，一个在数论上表现很好的系统是否也能在另一个数学领域表现很好，这是一个开放问题。嗯，确实。实际上，我认为我们思考的方式是：这取决于。取决于拓扑学是否有很多现有的定义，就像数学基础设施一样。

Distribution shift we're talking about. So, yeah, so you know, it is an open question whether a system that can do really well in numbers or you can do well in give me you know, another another field of math. Yeah, exactly. Well, actually I think this the way we think about it is it depends. It depends on whether topology has a lot of the existing definitions as almost like you know, the the math infrastructure.

嗯。

Mhm.

现有的。因为过去人们发现，当构建 math lib 时，比如对于代数教科书内容，他们可以……

Existing. Because what people have found in the past is when people were building out math lib like you know, for the algebra you know, bookwork um like they they can just...

所以 math lib 就是 Lean 的本科数学库。

So, math lib being the Lean like undergraduate library.

没错。没错。

That's right. That's right.

所以它就像你在本科数学中学到的所有证明，它们都在 Lean 中。

So, it's like all the proofs that you learn in undergraduate math and they're all sort of in Lean.

是的。例如，我的一些朋友现在在 Axiom，这有点疯狂，像是一个循环。Kenny 我们认识五六年了，他是第一个告诉我 Lean 的人。他和 Kevin Buzzard 一起构建 math lib。在 math lib 中编码代数比分析容易得多。这很有趣，因为分析中很多关于收敛、极限等的定义变得棘手。所以我认为今天的 math lib 中没有太多拓扑学内容，比如微分拓扑、微分几何之类。所以我们的系统可能在这些领域表现不佳，因为它甚至没有可依赖的定义。在已有定义的领域，我们在分布多样性和性能方面做得相当不错，比如解决了数论、交换代数、代数几何、一些离散数学（组合学和概率论）中的开放研究问题。

Yeah. So, for example, some of my friends who currently are at Axiom is you know, crazy like four circle back moment. Kenny um we're like friends for like you know, five, six years and he was the first one to tell me about Lean. He was working with Kevin Buzzard to build out math lib. It's a lot easier to codify algebra in math lib than for analysis. So that's interesting because for analysis a lot of the definitions around convergence, limits, etc. becomes tricky. And so, I don't think there's a lot of like topology in math lib today in terms of like differential topology, differential geometry kind of stuff. So, you know, our system likely will not do very well on those domains because it doesn't even have definitions to build off on top of. For the places where the definitions are in, we actually are doing quite okay in terms of distribution, diversity. We have good performance, you know, saw having solved open research questions in number theory, commutative algebra, algebraic geometry, some discrete math that combinatorics and probability.

那么，之前你说在 2024 年的 Putnam 考试中，AlphaProof 没有答对的所有问题……

So, earlier you said that with the Putnam exam, the 2024 version when all of the questions that were not that AlphaProof did not get right.

是 IMO，国际数学奥林匹克。

The IMO, International Math Olympiad.

对于 IMO，他们答错的所有问题都是组合数学。在那个特定领域是否存在弱点？

For the IMO, all of the ones they got wrong were in combinatorics. Is there a weakness there in that specific domain?

我会说是的。对于奥林匹克数学，人们发现组合数学有点棘手，因为步骤非常具有创造性。就我个人而言，我有人类朋友非常擅长组合数学，而我从不认为自己处于组合数学的顶尖水平。

I would say so. For Olympiad math, people are seeing combinatorics being a little bit more tricky. Since the steps are quite creative. So, for I'm a human and you know, when I have friends who are really good at combinatorics, which I never consider myself really the top of combinatorics.

我比较擅长数论，但我认识一些人，他们 IMO 金牌满分、Putnam 研究员满分，一路下来，当他们玩组合技巧时，我就想，我不知道你是怎么想到的，但你知道吗，一旦你给出那个构造，它实际上就变得容易追踪多了。我认为基于 Lean 的系统会在那些非常需要创造力的地方遇到困难，这就是为什么我们 Axiom 实际上也投资了一个叫做“数学发现”的东西。它不使用 Lean，而且我们几周内会有重大消息。基本上，数学发现的整个代码库即将开源。

I'm kind of better in number theory, but I know some people who are just their IMO gold perfect score, Putnam fellow perfect score and like all the way and then when they do like tricks in combinatorics, I'm like I don't know how you thought of that and but you know, after you give me that construction, it actually becomes a lot more trackable. I think a Lean based system will struggle in those very creative places, which is why we at Axiom actually also invest on something called mathematical discovery. It does not use Lean and we have some major news coming weeks. Basically, open source entire code bases of mathematical discovery coming up.

你想跟我们透露一点吗？

You want to tell us a little bit?

是的，当然。我们目前正在开源两个代码库。目标是，如果你是一位数学家或理论物理学家，有一个想要解决的问题，例如你想找到一个非常复杂的图构造，那么我们会建议你按照我们为数学家编写的非常详细的手册来运行我们的代码。这是一个供数学家进行数学发现的工具。数学发现，这个想法是，证明对数学来说是不够的。事实上，在你开始证明某件事之前，你不知道从哪里开始。所以你会尝试构造一些有趣的例子。这些通常可以是序列，对吧？如果你想了解一个序列的性质，你会写出前几项。也可以是图。所以，如果你想弄清楚你正在寻找的图应该具有某个性质，那么你会从图的更简单版本开始。现在，构造不能由 Lean 完成。所以我们相信用 AI 进行数学发现。我们在这个领域有一位元老，François Charton，他是 Axiom 的 Ken Houston Abbott 的成员。他之前做过模式展台和端到端的工作，比如试图通过寻找反例来推翻一个 30 年历史的猜想，找到了一个 130 年历史问题的解——全局 Lyapunov 函数，这是一种出现在三体问题中的数学对象。所以我们认为数学发现工具应该向数学界开放。因此我们正在开源整个代码库。

Yeah, yeah, sure. So, we are currently having two code bases being open sourced. So, the goal is for if you're a mathematician or you're a theoretical physicist and you have a problem that you would like to solve. For example, you want to find a construction that is a very complicated graph construction, then we would suggest you follow the very detailed manual supposed intended for mathematicians to run the code that we write. It's a tool for mathematicians to make mathematical discoveries. Mathematical discoveries, this is idea that, you know, proof is not enough for math. In fact, before you kind of start proving something, you don't know where you want to start. So, you will try to construct some interesting examples. These can be usually say sequences, right? If you want to understand the property of a sequence, you will write out a few of the first terms. This can also be graphs. So, if you want to, you know, figure out what the graph that you're looking for should have say a certain property, then you will start by doing some simpler version of the graph. Now, constructions cannot be done by a lean. So, we believe in having AI for math discovery. And we have, you know, one of the OGs in that field, François Charton, member of Ken Houston Abbott at Axiom. And he previously have done pattern booths and into end, you know, set out to disprove a 30-year-old conjecture by finding a counter example, found a solution to a 130-year-old problem, the global Lyapunov function, that is a kind of mathematical object showing up in the three-body problem. So, we are thinking that mathematical discovery tools should be open to the math community. So, we are open sourcing entire code bases for them.

那么，发现是指它提出新的猜想，还是……

So, discovery meaning it gives it makes new conjectures or it...

是的，实际上它是猜想前的步骤。

That's a Yeah, it's a pre-conjecturing step, actually.

好的。哦，我明白了。

Okay. Oh, I see.

是的，所以你开始形成直觉。

Yeah, so you start to form intuitions.

嗯。

Mhm.

对吧？如果你是一位数学家，目标是解决一个非常难的猜想，Axiom Prover 不能直接为你解决。你可能想尝试制定一些引理、猜想，然后交给 Axiom Prover。如果你是人类数学家，你会从想要制定那个猜想开始。你不知道往哪里走。你想找到构造。现在，我们要开源的代码库将帮助你，希望是显著地。

Right? If you're a mathematician and your goal is to solve a really hard conjecture, Axiom Prover can't just solve it for you. You might want to try to formulate some sort of lemmas, conjectures that you want to say then give to Axiom Prover. If you're a human mathematician, you will start by wanting to formulate that conjecture. You don't know where to go. You want to find constructions. Now, the code base that we're going to open source is going to help you, hopefully significantly.

那么，有一件事，可能有很多计算机科学家在听，当你们谈到形式化验证等时，会立刻想到 Rice 定理、可判定性、不完备定理，以及一些关于 LLM 计算复杂性的论点。所以，我很好奇，Rice 定理说，你不能对所有程序证明关于程序的非平凡性质，对吧？那么，你们是如何在这个领域导航的？显然，形式化验证能够做一些事情。

So, one thing that maybe there's a lot of computer scientists listening and one of the things that will immediately kind of come up and especially when you're talking about formal verification and so forth is Rice's theorem and decidability and incompleteness theorem and maybe some arguments about computational complexity in LLMs. So, I'm curious to hear Rice's theorem says you cannot prove non-trivial things about programs for all programs, right? So, how are you navigating this space? Obviously, formal verification, you know, does is able to do some things.

是的。所以，我认为很明显，有理论结果告诉你不能形式化验证所有程序，对吧？但是，我认为形式化验证大多数有用的程序是好的，对吧？所以，我记得有一个 MIT 的小纪录片，或者不是纪录片，是给录取学生的广告，里面有 MIT 吉祥物 Tim the Beaver 的一句名言：“理论给了你什么？”这有点像，它不会阻止我们尽可能去推动。所以，我们未来的目标是，假设你在做编码。你想为一个非常复杂的任务写代码。你知道，目前是前端网站，但未来我们可能想为更复杂的东西写代码，甚至整个分布式系统。然后，我们希望能够分解它。可能有一个高级的草图计划。我们可以做，其他人也可以做。但是，假设你让 Claude 把它分解成 10 件事。在某个时刻，它会决定调用 Axiom。Axiom 会给你一个你知道是形式化验证的计算机程序。或者它会说这对我们来说仍然太难了。

Yeah. So, yeah, I think like it's very clear that there's theoretical result telling you cannot formally verify all programs, right? But, I think it's good to formally verify a majority of the useful programs, right? So, you know, I remember there's this MIT little documentary or not a documentary, like an advertisement for people who are admitted students and then there's this famous line by Tim the Beaver, the mascot of MIT, saying that, "What does theory give you?" Which is kind of like it doesn't stop us from trying to push it as much as possible. So, the goal that we have for the future is suppose you are doing coding. You want to write code for a really complex task. So, you know, currently it's front-end websites, but in the future we might want to write code for much more complicated things, whole distributed systems even. Then, we want to be able to say decompose it. There's maybe a high-level kind of like sketch plan. This we can make, other people can make. But say, you know, you have Claude to give you like, you know, kind of break it down into 10 things. And at one point, it will decide to call Axiom. And Axiom will give you a computer program that you know is formally verified. Or it will say this is still too hard for us.

那么你写程序，把它交给 Axiom，它可能会对它进行修改？

So you write the program, you give it to Axiom, it makes changes to it maybe?

所以我们谈论的是两种不同的方面。

So we're talking about kind of two sort of faces.

嗯。

Mhm.

有可能我们是验证伙伴。所以你已经有计算机程序，想要我们验证它。事实上，GPT 找到了一个未解决的 Erdős 问题的证明，我们的竞争对手 Harmonic 验证了它。但我们可以做，我们想做验证生成，对吧？我们可能会说：“嘿，这个小组件，我们生成并提供给你的一切都是形式化验证的。”

It is possible that we are the verification partner. So you already have a computer program and you want us to verify it. In fact, like, you know, GPT found a proof to an unsolved Erdős problem and our competitor Harmonic, you know, Aristotle verified it. But we can do, we want to do verified generation, right? We might want to say, "Hey, you know, this little component, everything that we generate and provide for you is formally verified."

我明白了。所以这个想法是，你生成，你共同生成两者。所以我可以想象这符合“承诺”或“sorry”的概念，然后一个 sorry。

I see. So the idea would be you generate, you co-generate both. And so that and I can imagine this fitting into the idea of a promise or a sorry sorry and then a sorry.

这是一个 Lean 的 sorry。

Which is a lean sorry.

Lean 的 sorry 意思是它是一个未证明的引理，但你只是把它当作已知，直到你有时间证明它，对吧？这是思考 sorry 的好方法吗？

A lean sorry meaning it's a lemma that is unproven but you're just taking it as given until you can take have the time to prove it, right? Is that a good way to think about a sorry?

这是思考 sorry 的好方法，但不一定是在编码上下文中。

That is a good way to think about a sorry, but not necessarily in the coding context.

所以我可以想象你可以说，假设这个模块被验证了，那么这个模块就是正确的。这样你就可以把问题分解得足够小，以便验证。这是这里的直觉吗？

It's so I can imagine you can say assuming that this module is verified, then this module is correct. And so that you can decompose a problem small enough that you can verify. Is this kind of the intuition here?

那么假设我们想要，比如，网页代码控制流。

So let's say if we want to, you know, like web code control flows.

是的。

Yeah.

对，那相当困难。你可能会把它分解成多个步骤。然后它会继续把这些步骤分解成更细粒度的步骤。

Right, that's quite hard. You will likely, you know, break that down into multiple steps. And then it will continue to break down these steps into more fine-grained steps.

是的。

Yeah.

并且在某个时刻，你想要一些绝对正确的东西。

And at one point you want something that is absolutely correct.

是的。

Yeah.

这也是很可能实现的事情。我们想要生成一段计算机程序，并且底层保证也生成了证明，告诉你你指定的东西——这个程序——我能为你解决。

And then this is also something that is likely within reach. Then we want to generate a piece of computer program. And underlying is a guarantee that there's also the proof that has been generated, which tells you that the thing that you specified, this program, I can solve for you.

嗯。

Yeah.

所以我们的愿景是：任何可定义的东西都可以执行，任何可指定的东西都可以证明。我的理解是，如果你有一个程序乘以一个陈述或问题，它会映射到可验证性条件乘以一个证明。程序验证社区已经给了你可验证性条件，而我们正试图招募一个非常强大的团队来帮助我们实现这一点，Axiom Prover 将为你提供证明。

So the vision we have is: anything that can be defined can be executed. Anything that can be specified can be proven. So the way I think about it is if you have a program times a statement or problem, it maps to verifiability conditions times a proof. So while the program verification community has given you the verifiability conditions, and we're trying to recruit a really strong team to help us do that, Axiom Prover is going to give you the proof.

那么帮我理解从程序到证明的映射。因为我可以声称，这个两行的 Lean 程序验证了我声称它能解决的一切。我怎么知道它确实验证了我认为它验证的东西？

So just help me map from the program to the proof. Because I could say, you know, this two-line Lean program verifies whatever I claim it solves. How do I know that it actually verifies the thing that I think it verifies?

是的，举个例子，有一个基准测试叫 Code Verifier。它是一个代码验证基准，设计为对 Lean 友好。每个问题都是一个编程问题，目标是生成代码部分和证明部分——两个不同的计算机程序。然后目标是生成带证明的代码：即代码应该解决这个问题，而证明表明这个程序确实解决了问题。

Yeah, so for example, there's this benchmark called Code Verifier. It's a code verification benchmark that's supposed to be Lean-friendly. Every problem is a coding problem, and the goal is to generate a code part and a proof part—two different computer programs. And then the goal is to generate code with proof. So the code that supposedly solved this problem, and then the proof that this program indeed does solve the problem.

我明白了。

I see.

那么人们在这个基准测试上表现如何？我想稍微谈谈这个，因为很有趣。它由伯克利和 Meta 的研究人员在 2025 年编写，他们发现他们评估的任何版本的 GPT 在 pass@1 上只有 3.6%，迭代后大约 22%。那么形式数学系统模型表现如何？Cobra 是一个系统，因为需要迭代和定义，所以 pass@1 不太适用，但他们评估了系统的 pass@1 大约在 11-12%。还有 DeepSeek Prover 和 GoDo Prover，非常强的证明器模型，也是 11-12%。我认为我们的竞争对手去年在仅证明部分发布了 96%。而我们最近，在没有修改 Pan M 系统的情况下，达到了 99%：在 189 个问题中我们解决了 187 个。我们只错过了两个带证明的代码问题。

Now, how do people do on this benchmark? I want to talk about this a little bit because it's interesting. It was written by Berkeley and Meta researchers in 2025, and they found that whatever version of GPT they evaluated passes like 3.6% pass@1, iterative something like 22%. Now, how do the formal math systems models do? Cobra, which is a system because you iterate and define, so pass@1 doesn't quite work, but still they evaluated pass@1 of the system at about 11-12%. And also DeepSeek Prover and GoDo Prover, very strong prover models, 11-12%. And I think our competitor has released last year on the only proof part 96%. And we actually recently, with no modification to the Pan M system, we saw 99%: out of 189 problems we solved 187. We missed only two code-with-proof problems.

所以如果你想训练一个模型来做带证明的代码，并且你想使用强化学习，这实际上很烦人，因为如果你希望证明是非正式的，那就很烦人，因为那就像混合目标函数。你的代码是 Python 之类的东西，而你的证明是自然语言数学证明。你不会得到很强的强化学习性能，对吧？但如果你用 Lean 作为证明，并且代码可以选择 Rust——一种强类型语言，它很智能，转换更直接——那么你会得到更好的性能。

So if you want to train something to do code with proof and you want to do reinforcement learning, it's actually quite annoying because if you want proof to be informal, it's very annoying because then that's like a mixed objective function. Your code is something like Python and your proof is say natural language math proof. You will not have very strong RL performance, right? But if you have proof as Lean and you have code, you can choose Rust which is a strongly typed language, it's smart, it's more conversion. So you're going to have much better performance.

我无法理解你怎么把它们联系起来。我可以声称这个证明解决了费马大定理，对吧？但它是两行 Lean 代码。显然它没有。那么我怎么知道我写的程序与我生成的证明相匹配？

I can't wrap my head around how do you tie it. I can say that this proof solves Fermat's Last Theorem, right? But it's two lines of Lean. Obviously it doesn't. So how do I know that the program that I wrote matches the proof that I generated?

你基本上会查看编程问题，然后看程序，然后尝试看看它是否满足可验证性条件。

You will basically look at the coding problem, and you look at the program, and then you try to see if it satisfies the verifiability conditions.

但我怎么知道？如果我读它，我可以目测，传统上数学家是怎么做的：他们拿起论文读，然后说“我同意这个证明解决了问题”。然后另一个人说“不可能，它没有，看这里”。然后人们有分歧，最终达成共识这个证明解决了这个问题。那么你怎么跨越这个？

But how do I know? Like if I read it, I can eyeball it, and traditionally how mathematicians have done this is they take the paper and they read it, and they say, 'I agree that this proof solves the problem.' And then this other person says, 'No way, it doesn't, look at this.' And then people disagree, and eventually there's consensus that this proof solves this problem. So how are you crossing that?

逐步检查，对吧？

Check it step by step, right?

对，对。

Yeah, right, right.

是的，所以你基本上会查看可验证性条件，看看它是否确实满足。

Yeah, so you basically will look at the verifiability conditions and see if it does actually satisfy that.

这……

This...

假设我们看一段计算机程序，对吧？然后它是否真的解决了编程问题，你会有一个判断，对吧？你不会仅仅依赖测试，尽管那是一种方式。

So suppose we are looking at a piece of computer program, right? And then whether it does actually solve the coding problem, you will have a judgment about that, right? You will not solely rely on testing even though that is a way.

所以有人看了证明然后说：“是的，这确实解决了我们认为它应该解决的问题。”

So somebody looks at the proof and says, 'Yeah, that actually solves the problem that we think it's supposed to solve.'

那么现在你基本上是在生成一个形式验证程序，它满足关于这个程序和这个陈述的可验证性条件。所以再次，这个函数把你从程序和陈述带到可验证性条件和证明。

Then but now you're basically producing a formal verification program that satisfied the verifiability conditions about this program and this statement. So again, the function is taking you from the program and the statement to verifiability conditions and proof.

好的，所以我能看到这在基准测试中如何工作。那么如果我有一个飞行控制系统，非常……

Okay, so I can see how this works in a benchmark. Then if I have a flight control system that is very...

那么……

Then...

问题就变得非常烦人，就是规范。我认为这个词会是，即使我们说成功，我们也有规范问题。

The problem becomes very annoyingly the specification. I think the word is going to be, even if we say successful, we have a specification problem.

嗯。

Yeah.

所以比如银行来说：“请为我做一个非常安全的财务审计，抱歉，财务审计的证明，对吧？”那是什么意思？我们无法指定。人类不擅长指定我们想要的一切。总有一些东西我们没有指定，如果没有指定，它就没有被证明。

So like here comes a bank saying, 'Please do a really safe financial audit, sorry, proof of the financial audit for me, right?' Like what does that mean? We can't specify. Humans are bad at specifying everything that we want. There's always something that we are not specifying, and if it's not specified, it's not proven.

好的。

Okay.

那么你对此怎么做？

So what do you do about that?

嗯。所以我们还没到那一步。

Yeah. So we're not there yet.

好的。

Okay.

目前，再次强调，目前的愿景是：任何可指定的东西都可以被证明。显然，人们在这方面做得很好——这就是非形式推理发挥作用的地方。非形式推理可以，而我想引用测试的文献。测试很棒，因为测试就像在问：“嘿，你考虑过那个吗？”我想强调一项工作：由前 CTO Shuvo 做的基于突变的语言模型单元测试生成，他曾是 Facebook AI 研究的主管。

Currently, again, the vision as of currently is: anything that can be specified can be proven. Now obviously, people have been really good at that—that's a way where informal reasoning comes in. The informal reasoning can, and this is where I want to call the literature of testing. Testing is great because testing is like, 'Hey, have you thought about that?' You want to highlight a work: mutation-based LM unit test generation by ex-CTO Shuvo, and he was at the director of Facebook AI Research.

你可以这样理解：AI 会问“你有没有考虑过这种情况？”这有点像猜想。猜想有助于完善规范。

Like the way you kind of think about it is like the AI will be like hey have you thought about this this this case? Like and so this is a little bit like conjecture. So the conjecture is going to help with the specification.

我明白了。

I see.

然后证明器负责证明。

And then the prover does the proof.

所以这可能是一个交互过程，让人能真正给出好的……

And so this is an interactive process maybe that the person so that when we're actually giving good

我认为这是编码的未来。是的。我认为这是编码的未来。而且我认为，即使假设一切都可以形式化验证，研究自动测试生成仍然很有趣，因为它本质上是在给你一个规范提案。对。

I think this is the future of coding. Yes. Yes. I think this is the future of coding. And I think this is where you know is this where I think even if we are supposed like given the assumption that everything can be formally verified you know like studying sort of like you know automatic test generation is still interesting because it is basically giving you the specification proposal. Yeah. Right.

另一件事是自动形式化，也就是将非正式内容转化为更正式内容的能力。假设我有一个 ICPC 编程问题，用英文写成，比如“Alice 和 Bob 如何如何”。现在我想把它转化为一个形式化陈述，比如形式化规范。我该如何进行自动形式化？因为我还没解决这个问题，所以没有任何信号，没有依据。测试用例的输入输出对将作为形式化规范的依据。

And then another thing is let's talk about auto formalization, right? Which is the ability to to define it. It is kind of convert converting something that is more more informal into a into something that is more formal auto formalization. So, suppose I have a coding problem that is written for ICPC and this problem is written in English like Alice and Bob blah blah blah. Okay, now I want to convert that into a formal statement like a formal spec. How do I do the auto formalization step, right? Now, this is going to be because I have not solved the problem yet. So, I don't have any signal. I don't have any grounding. The test cases input output pair is going to ground my formal spec.

所以我知道我要给出这个输入和这个输出，它必须具有这些特征。于是我写测试用例。那么在 Lean 中有没有类似的东西？就是规范只告诉你期望的结果，而证明是完全未完成的。

So, I know I have to know I'm going to give this input. I'm going to give this output. It has to have these characteristics. And so and so I write test cases and I write a So, is there an equivalent in Lean of this, right? Where the specification where you just know the sort of like outcomes that you are expecting? So, that you like you the statement of the the result and then the but the proof is completely unproven.

实际上 Lean 有点烦人，因为它很多时候是证明，你并没有数值答案来作为依据。

So, Lean is actually quite annoying because it's like a lot of the times it's proof. So, you don't actually have the numerical answers to ground it.

好的。

Okay.

所以自动形式化相当困难，因为通常你无法为语句的自动形式化提供依据。但你可以为证明的自动形式化提供依据，因为你可以运行它，不过还是需要人工检查。

So, auto formalization is a quite quite a hard thing to do because you know what's generally happened is you can't you just it's hard to ground the auto formalization of a statement. You can obviously ground the auto formalization of a proof. But because you can then just run it. But you need human to eyeball it.

一个形式化程序（规模较大）的 Lean 证明有多大？它是随程序规模线性增长，还是超线性增长？

How big is a Lean proof of like a formalized, you know, of a formalized program of significant size? You like it's I mean do do they grow with the size of the program or do they grow super linearly?

实际上，目前每写一行代码，可能需要 20 行证明。

Yeah. Currently actually, you know, for each line of code written there could be like 20 lines of proof.

好的。

Okay.

情况不太乐观。

It's not looking that great.

但这是线性关系吗？还是说随着程序复杂度增加，证明行数也会增长，比如变成 40 行？

But but is that like a linear relationship or is it as the complexity of the program gets greater than it like it you know sort of also grows so that it's like 40 lines.

关于它的缩放定律，我没有很好的答案。

I don't have a good answer to the scaling law of that.

好的。

Okay.

嗯。

Yeah.

因为我知道这是形式化验证中的一个问题，对吧？即使是简单程序也需要非常长的证明。

Cuz I know that that's a problem in formal verification right? Right? Where you have these huge pro like you have to have these very very long proofs for even simple programs.

那么当规模变得太大时，你会遇到 LLM 能力的限制吗？

So then then do you are you going to run into sort of like limitations in in the capabilities of LLMs when you start to get too large larger um

我们从根本上相信我们正在构建一个推理引擎。

What what we believe fundamentally is we are building a reasoning engine.

嗯。

Mhm.

我们看到 action prover 处理了非常大的证明树。

And we have seen action prover deal with really huge trees that are like you know tree of a proof.

好的。

Okay.

我们看到它从 40 个节点扩展到 4000 个节点。

Uh we have seen it scale from 40 notes to 4,000 notes.

等等，action prover 就是那个 LLM 吗？

So wait sorry action prover is the is the LLM?

Action prover 是一个由多个模型组成的集成系统，我们对其进行了后训练。

The action prover is a ensemble system of multiple models that we do post training.

我明白了。好的。

I see. Okay. Yeah.

当然，它还包括我们开源的工具。

And also it also includes obviously the tools that actually that we have um open released.

抱歉。

Sorry.

是的，我们看到它能够处理越来越复杂的任务。

Yeah in words yeah. So so we have seen it being able to deal with more and more complex task.

我明白了。

I see.

我们认为它可能没有上限，但你可以问：它是否只受限于预训练基础模型？

We don't think it's probably bound you you could ask you know is it bounded at one point only pre-trained base model.

嗯。

Yeah.

我认为这是个好问题。中期训练可能非常有趣，因为很多能力提升确实来自那部分。你可以说，即使你试图用强化学习训练一个不太有天赋的人，他的表现也可能远不如未经后训练的拉马努金。你可以这样论证，但现实情况是，我们可能在某一天会考虑这样做。

I think that's a good question. I think you know mid training could be very interesting because it does actually you know a lot of the sort of capability gain does come from that part right? If you could argue that even if you try to reinforcement learn some person who is not very talented that person might behave you know be be be perform a lot less well than an un post trained Ramanujan. You can you can you can argue that way where is that reality of things but so at one point we might consider doing doing that.

那么

Then

但我们认为还有很多可以推进的空间。

But we think there's so much to push.

所以你只是觉得现在有太多开销，或者说有太多……

So you you just feel like there's so much overhead right now or so so much um

增长空间

space to grow

增长空间，以至于目前还没有遇到理论限制。我只是好奇，因为最近有关于 LLM 能解决的问题的计算复杂度的结果，我认为在写 Coq 代码时这还不是问题，但可以想象，在这样的系统中，当有海量 Lean 代码时，你无法把它们全部放入上下文窗口。所以你必须巧妙地处理，进行总结，然后不断总结，很快你就会失去对全局的把握。似乎对于这样一个非常庞大的系统，你可能会遇到……

space to grow that that you're not running into theoretical constraints at this point. I I just wonder because you know, there's been recent results in the computational complexity of the problems that LLMs can solve fundamentally and I don't think that they're really a concern for you know, when I'm writing code with coq code, but I can imagine problems becoming big enough in a system like this where you have a gazillion lines of lean. You can't get them get them into the context window. So you have to like be smart about that and then you have to summarize and then you're summarizing and summarizing and pretty soon you're like kind of losing track of what's going on and I it just seems like with a lar- very large system like that you might run into a

是的，这很有趣。这始终是一个“富足”的问题。简单来说，数学代码发现的复兴已经到来。Action prover 试图证明一切，最终你会得到数万行 Lean 证明。首先，自动非形式化比自动形式化容易得多，因为它没有缺乏依据的问题。每个模型都见过大量文本和 Lean 代码，所以你可以将 Lean 代码转换回非形式化描述。但问题是如何知道是否正确？你可以依赖循环一致性。然后我们再次形式化，并证明程序等价之类的东西。

Yeah, I think this is this is interesting. It's always a problem of abundance. So simply you just like keep really the the math code discovery renaissance has come. Acting prove it does try to prove everything. You end up with like tens of thousand lines of lean prove. So first of all, it's auto informalization is a lot easier than auto formalization minus the problem of no grounding, right? So you know, every every model has seen a lot of text and a lot of lean. So you can always you know, convert that lean back into back into informal and then there's the problem of well, how do you know if you're correct or not? You can rely on cyclic like consistency. So we then formalize again and then like prove like program equivalence something like that. So that's

哦，所以你先非形式化，再形式化？

Oh, so you you like informalize and then formalize

是的，你可以用它来提供依据，确保仍然……

Yeah, yeah, you can use it to ground and make sure that you still

是的，使用它。自动非形式化显然是一个不那么难的问题，所以你可以随时这样做。对于我们输出的很多 Lean 代码，我们可以有一个非形式化总结器，对大量 Lean 代码进行总结。它实际上表现还不错。

Yeah, use it Yeah, yeah, like in auto informalization is you know, obviously less hard a problem. So you can always do that. So for a lot of the you know, the the lean code that we output, we can have an informal summarizer of of like big chunks of lean. It's actually doing okay.

所以，你知道，这确实是个问题。还有一个我觉得非常有趣的问题——去年在 ICML 的 AI for Math 工作坊上有一个小组讨论，Leo de Moura、Jeremy Avigad 和 Shubo 以及 CTO 都在场。他们讨论的是：人类或数学家会不会在某个时候不再试图理解发生了什么？因为假设你是一个非常有雄心的数学家，你想证明黎曼猜想。然后砰的一声，这里有一个 Lean 证明。它实际上是正确的，而且你知道，它有一百万行。

So you know, that's a thing. And there's another question which I think is very interesting. I think there's a panel at ICML in core last year at the AI for Math workshop. There's Leo de Moura, Jeremy Avigad, and Shubo and CTO was there. And they were talking about: will humans or mathematicians at some point stop trying to understand what's going on? Because suppose you're a very ambitious mathematician, you want to prove the Riemann hypothesis. And bang, here's a Lean proof. And it's actually correct and it's just, you know, a million lines.

是啊，这对社区来说不是一个大问题吗？因为通常当有人提出一个重大证明时，很多时候……

Yeah, isn't that like a big negative for the community? Because usually when someone comes up with a big proof of something, often times...

对，我正要说到那里。对吧？问题是：这种负面结果会发生吗？这就是小组讨论的问题。这完全是假设性的。没有任何模型系统能证明黎曼猜想，对吧？所以免责声明，请不要剪掉那部分。

Yeah, I was about to get there. Right? It's like: will that negative outcome happen? That was the question the panel was discussing. It's completely hypothetical. No one's model system can prove the Riemann hypothesis, right? So disclaimer, please don't cut that part.

我刚才做了那个小……但是，人们还会试图理解发生了什么吗？我认为答案通常是肯定的。我认为好奇心以及理解数学或其他领域正在发生什么的渴望，是人类的基本需求。我认为在验证超级智能的时代——假设我们达到了那个阶段——这是一剂乐观药。即使所有输出都以比人类可能消费的更快速度和更指数级的数量产生，他们仍然会试图消费它们。至少他们会试图消费他们认为重要的那些。所以注意力是瓶颈。如果注意力是瓶颈，那么直觉和品味——判断哪个陈述值得人类消费，以及在有限的计算机资源中，计算机资源的支出是什么——人类数学家的品味将始终指引我们。我认为这非常美妙。

I just did that little... but like, will people still try to understand what's going on? I think the answer is usually always yes. I think curiosity and the desire to understand what is going on, mathematically or in other domains, is a basic human need. I think that's a dose of optimism in an era of verify superintelligence, suppose we get there. Even if all the outputs are produced at a much faster pace and much more exponential volume compared to what humans could possibly consume, they're still going to try to consume them. At least they're still going to try to consume the ones they deem important. So attention is the bottleneck. And if attention is the bottleneck, then intuition and taste—of which statement is probably worth the consumption of human and also maybe in the finite computer resource, what's the spending of computer resources—that's where human mathematicians' taste will always guide us. I think that's incredibly beautiful.

是否值得在内部获取你可以用一种方式证明的结果，然后让你的系统走许多不同的路径，以获得正交的、概念上正交的证明，从而得到关于同一事物的多种不同推理方式？因为我认为这非常有价值：如果你遇到一个问题，可以说，这是人类可能会做的蛮力自然方式，然后还有一个更短更优雅的方式。那么你有没有考虑过以某种方式训练你的模型变得优雅？

Is it worth internally taking results you can prove one way and then trying to send your system down many different routes to get orthogonal conceptually orthogonal proofs, so you get a diverse set of different ways of reasoning about the same thing? Because I think it could be very valuable if you're given a problem to say, here's the brute force natural way that maybe some humans would do it, and then there's a much shorter elegant way. So have you thought about training your models to be elegant in some way?

是的，我们最终会谈到那里，因为你知道，这个猜想可能取决于我们对品味和优雅的定义。

Yeah, at one point we're going to get to there because, you know, the conjecture will probably depend on what we mean by taste, elegance.

对我来说这感觉像是一个对齐问题。谁来决定什么是优雅？人类来决定什么是优雅。

Feels like an alignment problem to me. Who gets to say what is elegant? Humans get to say what is elegant.

这就是我的意思。努力工作是关键。你努力钻研的东西，你就会擅长。

That's what I mean. There's something about hard work. What you work on hard is what you're going to be good at.

是的，我们在很多领域也会遇到这个问题，不仅仅是数学。如果你没有经过多年的训练，你怎么能成为那个拥有出色高层理解、全栈理解、高层和底层理解的高级程序员呢？

Yeah, we're going to have a problem about that in a lot of domains as well, not just math. How do you be that senior programmer with really good high-level understanding, full stack understanding, high-level and low-level, if you haven't spent the year of training?

我的意思是，我会争辩说你不需要——这很哲学——但我不需要擅长汇编语言编程。没有多少人擅长那个。少数人擅长是因为这对他们的工作很重要。

I mean, I would argue that you don't—this is very philosophical—but I don't need to be good at assembly language programming. Not many people are good at that. A few people are because it's important for their job.

经验，但还有你的好奇心。

Experience, but your curiosity.

是的。但这感觉有点不同，因为不擅长证明东西，例如，似乎是一个根本性的差距——如果我不做那件事，我的思维可能不会以同样的方式发展。而如果我只是不擅长汇编语言编程，但我擅长高级编程，也许那并不重要。

Yeah. But it feels a little different because not being good at proving things, for example, seems like a fundamental gap that maybe my mind doesn't develop in the same way if I am not doing that. Whereas if I'm just not good at assembly language programming but I'm good at higher level programming, maybe that doesn't matter.

我认为这可能是因为教育系统的管道运作方式：如果你没有早期表现出才华的迹象，有时你就不会经历数学的预训练过程。

I think that's probably because how the education system pipeline works, which is that if you do not show early signs of brilliance, you don't sometimes go through the process of pre-training in math.

是啊，是啊。

Yeah, yeah.

对，所以你可以争辩说，你不需要学习所有东西来培养品味，但有一个你需要达到的门槛。

Right, so you can argue that you don't need to learn everything to develop a sense of taste, but there's a threshold you need to meet.

是的。

Yeah.

所以例如，你可能需要能够编程，即使你不需要理解汇编语言。

So for example, you probably need to be able to code even if you don't need to understand assembly language.

而且那可能会迁移。我从奥数问题中获得的直觉迁移到我尝试从事的其他研究领域。组合数学迁移得更直接，非常相似，数论可能更远，但还可以。当涉及到与奥数非常不同的东西时，迁移就不那么强了，但你需要勤奋，如你所说。你需要勤奋地经历一定量的训练。

And that thing might transfer. My intuition from Olympiad math problems transfers into some other research areas I try to pursue. Combinatorics transfers more directly, very similar, and number theory could be further, but still okay. And when it gets to something a lot more different than Olympiad math, it transfers less strongly, but you need to be diligent, as you said. You need to diligently go through some amount of training.

是的。

Yeah.

如果你只依赖强 AI，那不会发生。

And if you only rely on strong AI, that doesn't happen.

我想换个话题。你提到了软件验证。领域是什么？你打算如何赚足够的钱来证明估值合理？另外，恭喜你。

I want to switch gears. You mentioned software verification. What are the domains? How are you going to make enough money to justify the valuation? And congratulations, by the way.

谢谢。是啊，是啊，是啊，是啊。

Thank you. Yeah, yeah, yeah, yeah.

那么给我们一个高层总结：你向投资者展示的愿景是什么，为什么这实际上能赚很多钱？

So give us the high-level summary of what is the vision you put in front of investors about why this actually makes a lot of money.

是的。首先，这有点先发制人。所以我认为很多投资者对 Axiom 有很高的兴趣。就我们所相信的而言：我们认为编码的未来将在某种程度上受到验证能力的约束。我们相信解决形式化数学是一个非常自然的起点。通过扩展，你可以提高硬件和软件的验证能力。例如，对于硬件来说，这相当革命性。对于大部分验证过的 GPU，没有部分信用。

Yeah. So first of all, this one is kind of preemptive. So I think a lot of the investors have pretty high interest about Axiom. In terms of what we believe in: we believe the future of coding is going to be somewhat constrained by verification capability. And we believe solving formal math is a very natural starting point. And by extension, you can increase the verification capability across hardware and software. For hardware, for example, that's quite revolutionary. There is no partial credit for a mostly verified GPU.

没有。

No.

和美元。

And dollars.

要么全有，要么全无。就是要么全有，要么全无。而且你确实需要一个完美的证明器。

It's all or nothing. It is all or nothing. And you do need a perfect prover.

现在我想强调这一点：假设我是一个热爱解数学题的人。我认为有很多 Twitter 用户喜欢像抓宝可梦一样去解决那些问题。然后我就试着用非确定性的 GPT 来获取完整的证明。

Now I want to stress this point: suppose I am someone who loves solving math. I think there are a lot of Twitter users who enjoy Pokémon-like hunting for those problems. And then I just try to use a non-deterministic GPT to try to get the full proof for that.

嗯。

Yeah.

现在我可以重复做很多次。我可能会成功，也可能不会。而且我可能并不在意是否真的成功。但这对于硬件验证来说完全行不通。所以对于那些我称之为“需要硬核验证”的领域，这是一个痛点。当前的痛点。有成百上千的人和数千个许可证被用来解决一个局部网格问题的验证。

Now I can do that many many times. And I might succeed and I might not. And I might not have a problem with whether I actually succeed or not. This absolutely does not work for hardware verification. So for those kind of domains which I call like hardcore verification needed it is a pain point. It is a current pain point. There are hundreds of humans and thousands of licenses being dedicated to solve one local grid problem verification.

顺便提一下，据我所知，ASIC 项目中设计与验证的行业标准大约是 1 比 3。

Just as an aside, my understanding is that the industry standard for design to verification in an ASIC project is like one to three.

1 比 3 到 1 比 4，没错。无论是在规模还是时间上。

One to three and to four, correct. Both in size and in duration.

嗯。

Yeah.

对。所以我们称之为平方。我认为这是必须覆盖的。而对于软件验证，这很有趣，对吧？因为，可能我们都意识到，我侄子为一个可爱的网站写代码。完全没有必要正式验证那段代码。为什么要呢？

Right. So, if you let's call that square. And then I think it's a must cover. And now for the software verification, it is interesting, right? Because, as probably we all realize, my nephew writes code for a lovable website. There's absolutely no need to formally verify that piece of code. Like, why would you?

嗯。

Yeah.

我听到一个故事，来自《纽约时报》记者 Cade Metz，他告诉我：然而，如果你想想，在智能体时代，比如我的 OpenClaw 可能做各种事情，也可能做一些坏事。比如我的 OpenClaw 可能决定给我的教授发一些不好的短信，对吧？你可能会说，这是否是形式验证的问题？可能仍然不是，对吧？你可以改变行动空间，让它更受限，这样你就不需要依赖形式验证。所以，你可以有很多案例，但你可以想想，也许一个使用智能体处理大量监管事务的企业，他们可能想这样做。这是他们的选择。但我认为，验证能力的提升，无论是在延迟、准确性还是整体性能方面，将决定人们是否依赖形式验证。

Now, I heard a story from Cade Metz, actually that New York Times reporter who told me the story, which is like: however, if you think about, in the time of agents like my open claw can probably do all sorts of things and probably can do some bad things. Like my open claw can decide to text something bad to my professor, right? And you can say that perhaps is that a problem of formal verification? Probably still not, right? You can change something about the action space and make it more limited, so you don't need to rely on formal verification. So, you can have a lot of cases, but you can think about, maybe an enterprise that is dealing with a lot of regulatory stuff using agents, they might want to do something like it. It's their choice. But, I will argue that the improvement of verification capability both in latency and accuracy and all these stuff of the performance holistically is going to determine whether people rely on formal verification or not.

当然。

Sure.

所以，在某种程度上，我们希望把它做得足够好，以至于我们可以把它变成一种选择。

So, in a way we want to make it so good that basically we can make that a choice.

那么，为什么投资者认为你们能做到呢？因为，我的意思是，人们已经在验证领域工作了很长时间，我认为每个人都同意这是一个重要的问题，而且我认为如果我能为我写的每个程序都得到一个验证证明，比如“嘿，Claude，也给我证明”，然后它就直接生成，看起来没问题，我绝对会这么做。但你认为投资者看到了什么，说服他们“好吧，就是现在，我要投入 2 亿美元或更多”？

So, why did the investors think that you could do this, right? Because, I mean, people have been working on verification for so long and I think that everyone agrees it's an important problem and I think certainly if I can just have a verification proof for every program that I write like hey Claude like give me the proof also and then it just produces it and yep looks good to me. I would absolutely do that. But so why is it what was it that the investors saw in your opinion that persuaded them that okay this is the moment I'm going to put in my 200 million or whatever.

我认为在信念方面，你要么有，要么没有。所以你要么和我们一起做梦，要么不。这没关系。因为当我们实现梦想时，公司会价值 100 亿。是的。所以这就是我的感觉：我们相信验证是超级智能的关键关键部分。我们的超级智能版本是绝对经过验证的。我们认为没有其他可能的未来。我们不相信——我要公开说——我们不相信一个非正式的数学系统会成为数学 AGI 的解决方案。

I think when it comes to faith you either have it or you don't. So you either dream the dream with us or you don't. And that's okay. Because when we realize the dream the company is going to be worth 10 billion. Yeah. So I think that's kind of the feeling that I have which is that we believe verification is the critical critical part to superintelligence. Our version of superintelligence is absolutely verified. We don't think there's any other possible future. We do not believe that I'm going to say on the record. We do not believe that an informal math system is going to be the math AGI solution.

为什么不行？

Why not?

我们就是不相信。

We just don't believe that.

我的意思是，反方论点就是“哦，我们只要做很多好的强化学习，我们看到 GPT 解决了一些问题，等等”。那你为什么认为这行不通呢？

I mean the counter argument is oh you know like we just do a lot of good RL and you know we've seen GPT solving you know I think some of those problems and like whatever. So why do you think that that runs out of gas?

是的，你可以说，如果你已经是前沿数学，拥有无限资源，那为什么会行不通？根据定义，没有“行不通”这回事，对吧？如果你认为无限就意味着不会耗尽，但我不认为它能扩展到超级智能。

Yeah so you can say that if you're already frontier math and you have like so so frontier math and you have like infinite resources. Why does that? There's this by definition no running out of gas. Right? If you think like infinite means like there's no running out of gas. I don't think it's going to scale to superintelligence.

所以你认为你会耗尽，基本上就是钱用完了，算力用完了。

So you think that you run out like you run out of money basically you run out of power.

作为一家初创公司，我们首先做不到这一点。作为一家初创公司，我们首先做不到。但我们普遍认为，形式数学，以及通过将数学证明转化为程序、转化为代码，能给我们带来更好的性能。

So we as a startup first of all cannot do that. We first of all as a startup cannot do that. But we generally think that formal math and by sort of converting math proofs to programs to code give us much better performance.

所以这只是你的样本效率论点等等。如果你不使用形式化，你就无法足够地弯曲曲线。

So it's just your sample efficiency argument and so forth. That you just can't bend the curve enough if you don't use formal.

问题是，非形式化的东西在某种程度上对我们也是可用的。如果你真的能同时拥有非形式化和形式化系统，那将是非常强大的。我有点怀疑的是，我们能否仅通过非形式化方法扩展到大规模 AGI。你会一直有 LMS 评判解决方案，或者有人类专家评分，但人类专家无法很好地扩展。如果你真的争论无限，那么当然，你也有无限的钱，可以支付无限的费用，但真的有无限多的人能够理解并证明像 Langlands 纲领中一个非平凡的结果吗？我认为，祝你好运找到那些人。事实上，我认为 Frontier Math 之所以能汇集起来，是因为他们无法通过自己的专家库构建基准，所以他们不得不与 Epoch 合作，对吧？这就是我担心人类部分的原因。所以他们有 LMS 评判，现在又有随机评判。问题在于，有些事情是无法实现的，而有些事情是极其昂贵的，极其极其昂贵，最终这两者会混为一谈。

The thing is the informal stuff is also available to us in a way. If you really can have both informal and formal system. And that is going to be a very strong thing. The thing that I kind of like, I think my suspicion about whether we can scale to mass AGI just by the informal approaches, you're going to keep having the LMS judges solution or you have human experts who grade and the just human experts doesn't scale that well and then if you really argue infinite infinity, then sure, then you also have infinite money and you can pay infinite and there are so many. Is there really infinite number of people who can understand and prove at say about like a result a non-trivial result in Langlands program? I think, good luck finding those people and in fact, I think how Frontier math came together is because they couldn't assemble a benchmark by their expert pool, so they have to collaborate with Epoch to do it, right? And I think that's kind of what I worry about about having the human part. So they have LMS judges and then now stochastic judging. The problem is like whether something is impossible to achieve versus something is incredibly expensive and like really incredibly expensive and incredibly expensive to achieve get kind of like mixed in the end.

然后当然，投资者总是想知道为什么是你。对吧？我读过一些关于你的背景，我认为如果听众没有听到一点你的个人故事，那将是一种损失。

And then of course, investors always want to know why you. Right? So, I've read a little bit about your background and I think we would do a disservice to the audience if they didn't hear a little bit just about your personal story.

我明白了。

I see.

你想稍微谈谈吗？比如你做过一些非常有趣的事情，所以我很想听听你和你的团队。

Do you want to talk just a little bit about like you've done some really interesting stuff so I'd love to hear like you and then your team.

好的。

Yeah.

是什么让 Axiom 如此特别？

What makes Axiom special?

是的，我认为 Axiom 非常特别，因为他们确实是数学专家。基本上，他们是我们正在开发的系统的用户，这个迭代循环非常快，极其快。你拥有一些在研究和奥赛中顶尖的数学家，还有 MathLib 的贡献者、维护者、开发者和语言大师，再加上来自应用机器学习领域的人，来自 Meta Fair 和 Google 等非常强大的组织，以及拥有代码生成专业知识、从事编译器工作（如 Kernel Gen）的人。将这些背景的人聚集在一起，我认为这种跨学科的思考方式非常有帮助。我们认为 AI for math 传统上就是跨学科的。人们从 AI for science、代码生成文献，以及更广泛的前沿应用机器学习中借鉴技术，试图应用于 AI for math 这个细分问题。所以，我们也认为拥有这样一支非常特别的团队是一个差异化优势。我们还认为，正如你所说，没有永久的护城河。我们生成的专有数据和正在形成的飞轮效应是一个暂时的护城河。就我个人而言，我热爱数学。我从很小就开始学数学，当要解决的问题有点超出能力范围时，数学会变得非常困难，有时会令人沮丧。有时我想，如果能有一个 AI 来帮助我就好了。是的，我想为什么不建造这样一个东西呢。

Yeah, I think Axiom is very special because they are really expert mathematicians. Basically, they are users of the system we are developing and that iteration loop is very fast. It is extremely fast. You have some of the strongest mathematicians in both research and Olympiad contests, and you also have people who are MathLib contributors, maintainers, developers, and ling gurus, really, and combine them with people who come from applied ML, really strong organizations like Meta Fair and Google, as well as people who have code gen expertise who work with compilers like Kernel Gen. Having these backgrounds together, I think that sort of interdisciplinary way of thinking about things is quite helpful. We think AI for math has traditionally been quite interdisciplinary. People are borrowing techniques from AI for science, from the code gen literature, and obviously from the broader frontier applied ML to try to apply to the niche problem of AI for math. So, we also think having this very special team is a differentiation. We also think that, as you say, there's no permanent moat. The proprietary data we generate and a little bit of a flywheel we are seeing is a temporary moat. Me personally, I love math. I have been doing math since I was very young, and math sometimes gets really hard when the problems you are solving are just a little bit out of reach, and it gets a bit depressing. Sometimes I wonder if I can just have an AI help me. And yeah, I think why not build such a thing.

你在牛津大学读了神经科学硕士。这对你的思考有影响吗？

You did a masters at Oxford in neuroscience. Does that inform your thinking here?

这是个好问题。我认为我在神经科学方面的经历让你很好地了解什么是困难的，什么是不可能的。这很有趣。我觉得那一年的神经科学让我对什么是困难有了一些感觉，但对什么可能有效几乎没有感觉。但我当时打着神经科学的幌子，在 UCL Gatsby 研究所混，有幸和一些很棒的教授一起做 AI 研究。所以我认为那是非常富有成效的一年，与其说是神经研究，不如说是 AI 研究。

That's a great question. I think my experience with neuroscience is you learn very well about what's hard, what's impossible. It's very interesting. I think that year of neuroscience gave me some feelings about what's hard and almost no feeling about what might work. But I was kind of under the pretense of neuroscience, hanging out at the UCL Gatsby Institute, and was fortunate to do AI research with some really cool faculties. So I think that was a very productive year of AI study, if not neural study.

所以对你来说主要是学习 AI。

So it was mostly for you studying AI.

没错。我认为在英国，回到 20 世纪，如果你把某样东西称为 AI，你就得不到捐款，但如果你称之为脑科学，你就有机会。所以是在 UCL Gatsby，这是一个顶级的 AI 中心，很多人从那里去了 DeepMind，包括 Demis 本人。这是一个非常棒的研究环境。我记得那些茶话会非常精彩，人们基本上就是在做 AI。它叫做 Gatsby 计算神经科学研究所。是的，我认为事情是这样的：我当时在读神经科学硕士，很快意识到你需要杀老鼠，而我不想那样做，计算神经科学听起来更有吸引力。当你看到项目中有 Transformer 时，你绝对想去做。

That's right. That's right. I think in the UK, back in the 20th century, if you called something AI you would not get the donation, but if you called something brain science you might have a chance. So it was at the UCL Gatsby, which is a premier AI hub where a lot of people actually go from there to DeepMind, including Demis himself. It's a very wonderful research environment. I remember those tea time talks were very amazing, and people were basically just doing AI. It's called the Gatsby Computational Neuroscience Institute. Yeah, I think how that happened was because I was in the master of neuroscience program and quickly realized that you need to kill rats and kind of don't want to do that, and computational neuroscience sounds more appealing. When you look at the project and you see transformer, you absolutely want to do that.

我们都对此感到兴奋。

We're all excited about that.

所以在 Gatsby 之后，你在斯坦福开始了数学博士项目。

So after the Gatsby, you started a math PhD program at Stanford.

实际上我先在法学院全职读了一年。

I started actually one year full-time at the law school.

哦。

Oh.

因为 JD 博士项目的结构要求你完成一整年的住校学习。所以那也是非常有趣的一年，学习了一些非常迷人的东西，比如刑法，研究凶杀案。令人兴奋。

Because the JD PhD program is structured in a way where you have to spend one full residency year. So that was also a very fun year of learning things that are quite fascinating, like criminal law, looking at homicide cases. Exciting.

你是否觉得法律体系在某些方面规定不足或过度，也许你可以改进它？

Do you ever feel like the legal system is under or over specified in some way that maybe you could actually rise and improve?

这是个好问题。我认为很多事情确实规定不足。对于其他一些事情，我实际上对从数学推理到这些特定领域的迁移学习感到兴奋。我认为上诉诉讼，那些法律技巧，一些非常优秀的上诉学者和律师正是来自数学训练。虽然不多，但比如 Lawrence Tribe，哈佛法学院教授，左翼民主党中最强的上诉诉讼和最高法院案情摘要头脑之一。我认为还有很多其他领域，比如反垄断，非常流程化。合同法有时也很流程化。破产、税务，更多是公司方面的。我只是喜欢诉讼方面。

That's a great question. I think for a lot of things it's definitely under specified. For some other things I was actually quite excited about sort of transfer learning from mathematical reasoning to those specific fields. I think appellate litigation, the legal gymnastics you see some really good appellate scholars and lawyers that just come from math training. Not many, but like Lawrence Tribe for one, Harvard law professor, one of the strongest appellate litigation and SCOTUS briefs brains on the left Democratic party. And I think there's a lot of other domains such as antitrust that's incredibly flowchart-y. Contract law sometimes also flowchart-y. Bankruptcy, tax, more on the corporate side. I just love the litigation side.

所以，既然我们在谈论诉讼，虽然不是同一回事，但有一个 Erdos 问题，Axiom 遇到了。我不记得是不是 Axiom prover 之类的。对吗？当时有一个争议，因为它声称解决了问题，但实际上证明已经被发现，只是被形式化了。

So, just because we're talking about litigation, it's not the same thing, but there was an Erdos problem that Axiom saw. I don't remember if it was Axiom prover or whatever. Is that right? There was a controversy about it because it had represented that it had solved the problem when in fact the proof had been discovered and then just formalized.

所以，实际上发生的事情是，我们的竞争对手 Harmoni 决定宣传他们解决了未解决的问题，Erdos 编号 124 和 481，然后我们相信了他们的文献综述，认为这些问题确实是未解决的，而我们当时是一家非常年轻的公司。我们想测试我们的系统是否能尝试竞争对手能解决的问题。我们完全没有预料到我们真的会解决它们，但结果是我们都错了，实际上这些问题之前已经被解决了。

So, actually what happened was our competitor Harmoni decided to publicize that they have solved unsolved problems, Erdos number 124 and 481, and then we trusted their literature review, believing that these problems are really truly unsolved, and we were a really young company at the time. We wanted to test if our system can attempt the problems that our competitor can. We fully did not expect that we would actually solve them, but turns out that we were both wrong, that in fact the problem has been solved before.

我明白了。那么……

I see. So then...

这不是我们唯一一次依赖他人的文献搜索，我们应该承认这一点。另一次是这篇名为《无平方行走中的死胡同》的论文。Miller 教授提出了这个问题，结果发现它已经被解决了，但我们确实应该做好自己的部分。

It's not the only time that we relied on others' literature search, and we should own it. The other time was this paper called 'Dead Ends in Square-Free Walks.' Professor Miller had this problem that actually turns out to have been solved, but we really should have done our part.

我想表达的不是你们做错了什么，而是……

The point I'm trying to maybe elicit is not that you guys did something wrong, but rather...

你知道，有一个日本广告，整个公司成百上千的人在广告中道歉。就像‘对不起，我们把价格提高了 5 美分。’就是那个广告。我在想也许我应该就这么做。

You know, there's this Japanese advertisement of a whole company, hundreds and thousands of people, apologizing in the advertisement. It's like, 'Sorry we raised our price by like 5 cents.' That's the advertisement. And I was thinking that maybe I should just do that.

太尴尬了。

It's so embarrassing.

不，我认为信息的来源问题，以及你如何将答案与问题联系起来，这很重要。

No, I think the question of provenance of information and sort of like how do you connect the answer to the question?

是的，这是个好问题。我觉得在 Erdős 事件之后，我们变得非常谨慎。我们没有再去查看其他 Erdős 问题。我相信 Harmonic 仍然声称他们解决了 Erdős 问题，但可能不是真的。我不知道。Terence Tao 和其他人有一个关于所有 Erdős 问题及其状态的数据库。这确实很容易出错，因为有很多 Erdős 问题实际上已经被解决了。搜索和检索是个难题。你不知道那个论证或等价版本是否存在。事实上，那个数据库最有趣的地方在于，很多问题并非直接解决，而是可以通过另一个已解决结果的简单扩展（几乎微不足道）来解决。有时甚至不是结果。在 dead end square free walks 这个案例中，这与 Harmonic 无关，我们当时没有意识到，后来 Kanna Sundararajan 教授向我和 Miller 教授指出，这实际上来自一个 Stack Math Overflow 或 Stack Overflow 帖子。一个用户指出有一个结果。这很迷人。但很难发现。搜索是个难题。

Yeah, this is a good question. I think after the Erdős thing, we were extremely careful. We didn't really look at the other Erdős problems. I believe that Harmonic still continued to claim they have solved Erdős problems. They might or might not. I don't know. There's a database about all the Erdős problems and the status, I think by Terence Tao and others. It's really an easy mistake to make because there are so many Erdős problems that have actually been solved. Search and retrieval is a hard problem. You don't know if that argument or an equivalent version exists. In fact, the most interesting part about that entire database is there are a lot of problems that are not directly solved, but can be an easy extension, almost trivial, of another result that has been solved. Sometimes not even a result. In the dead end square free walks case, which is nothing to do with Harmonic, we didn't realize it, and Professor Kanna Sundararajan pointed out to us and to Professor Miller that it was actually from a Stack Math Overflow or Stack Overflow post. A user pointed out there's a result. It's fascinating. It's hard to find out. Search is a hard problem.

我猜这意味着猜想引擎之类的，它是否将搜索作为其过程的一部分，还是说这是你们人类做的事情，然后输入进去？

I guess that means that the conjecture engine or whatever, does that use search as part of its process, or is that something that you, the human, do and then feed?

我认为知识图谱或知识库是任何公司非常重要的组成部分。而且我觉得这一点没有被充分讨论。

I think a knowledge graph or knowledge base is a very important component of any company. And I don't think it's talked about enough.

是的。

Yeah.

所以你们听起来不想透露太多细节，但你们有一个知识图谱。我还读到你们有一个非常庞大的 Lean 证明数据库，或者某种意义上的合成数据，这可能是你们的竞争优势。

And so you guys with that, it sounds like you don't want to give us too many details, but you guys have a knowledge graph. I also read somewhere that you guys have a really massive database of Lean proofs that you've generated, or synthetic data in some sense, and that may be a competitive advantage for you.

我认为每个人都在试图积累数据，这不是一种模式，只是时间和时间模式。关键在于你是否能足够快地执行，以确保由于数据集积累而拥有一定的缓冲。但这仅仅是一个缓冲。

I think everyone is trying to accumulate data which is not a mode, it's just time and time mode. It's all about whether you can execute fast enough to make sure you have a certain buffer because of your dataset accumulation. But that is only just a buffer.

你有没有想过做类似 AlphaZero 的数学版本，从零开始，让它自己创造公理，看看会发生什么？

Have you ever thought about doing something like an AlphaZero for math where you start from nothing and let it just make up axioms and see what happens?

这是个很棒的问题。我认为这是一个非常有趣的方法。我们相信一点：假设 Axiom Prover 可以成为一个非常强大的数学家，那么它每天证明的东西应该有助于它改进。这种自我改进非常有价值。形式化数学社区里还有其他人。Gabriel Prajs 教授的工作非常有趣。还有一些更偏向猜想型的探索。假设我们改变很多东西；你可以用某些方式做特定的事情，来尝试看看你的系统能否学会猜想并构建理论。

This is a wonderful question. I think that's a very interesting approach. I think we believe in something: suppose Axiom Prover can be a really strong mathematician, and the thing it is proving every day should hopefully help it improve. This sort of self-improvement is extremely valuable. There are other people in the formal math community. Professor Gabriel Prajs' work is very interesting. There are some of the more conjecturing type of exploration. Suppose we change a lot of things; there are specific things you can do in certain ways to try to see if your system can learn to conjecture and build theories.

我认为这个话题非常有趣且重要，因为你声称要达到超级智能，这根本不可能。也许如果你有无限资源，你可以只用强化学习，也许能行。但现实是你无法做到足够样本高效，所以你需要某种验证器在推理过程中介入，而不是仅仅在训练过程中。你在训练过程中有验证器，但在推理过程中却没有。

I think the topic is really interesting and important because you're claiming that to get to superintelligence, it's just not going to be possible. Maybe if you had infinite resources, you could just RL and it would work, maybe. But the reality is you can't be sample efficient enough, so you need some sort of verifier in the loop with the inference process, rather than just during training. You do have verifiers during training, but you don't have them during inference.

是的，我认为很多人都在暗中试图用这个来 grounding 他们的推理。

Yeah, I think a lot of them are secretly trying to use this to ground their reasoning.

是的。我很惊讶，当 o1 即将发布时，每个人都知道它要来了但还没发布。我确信他们会宣布使用 Lean 进行证明的形式化验证，实际生成证明然后验证，从而 grounding 他们的推理。

Yes. I was surprised that when o1 was coming, everyone knew it was coming but it hadn't come out. I was sure they were going to announce that they're using Lean to do formal verification of proofs and actually generate proofs and then verify them, so that they're grounding their reasoning.

当 Ilya 还在的时候，有 GPTf。那是一项很棒的工作。还有 MiniF2F。这些都是 OpenAI 的形式化数学工作。

When Ilya was there, there was GPTf. That was a great piece of work. There's also MiniF2F. These are all formal math work at OpenAI.

好的。那么，那些人大概在做些什么。

Okay. So, presumably those guys are doing something.

不，不，他们都离开了。

No, no, they all left.

哦，他们都离开了，我明白了。

Oh, they all left, I see.

所以，这就是我的观点。如果你是一名初级技术人员，想要花尽可能长的时间去解决一个问题，奇怪的是，人们认为初创公司可能会搞砸并崩溃。但在像 Axiom 这样的初创公司或其他新实验室，你反而更有可能长期专注于同一个问题。

So, that's my point. If you're a junior member of technical staff and you want to work on something for as long as it takes to solve it, weirdly, people think about startup as this sort of thing that can just run to hell and fall apart. You might have a better chance of staying focused on the same problem for as long as it takes at a startup like Axiom or one of the other new labs.

是的。如果你与公司的使命一致，而不是有人决定你正在做的事情不再……

Yeah. If you're aligned to the mission of the company rather than somebody decided that what you're doing is no longer...

大科技公司。

Big tech.

是的，可能是你的副总裁在政治斗争中失利了。

Yeah, it can be your VP lost some political fighting.

是的。绝对如此。

Yeah. Absolutely.

不，显然如果我们成功了，他们都会重新开始做这件事。那么作为人才，也会有更多潜在的地方可以选择。

No, obviously if we succeed, then they're all going to start doing that again. And then as a talent, there are more potential places to choose from as well.

是的。所以你的任务就是快速前进，让他们挣扎。实际上，我们还没谈到这个，但你们刚刚发布了一个用于 Lean 验证的 API。我用 Claude Code 试了一下，因为比搭建自己的 Lean 工具链更容易。我们试图让 Lean 证明一些东西。基础设施并不简单，尤其是在大规模下。你想谈谈吗？

Yeah. So, your job is to go fast so that they're struggling. Actually, we haven't talked about it, but you actually also just released an API for doing Lean verification. I tried it with Claude Code because it's easier than setting up your own Lean toolchain. We were trying to get Lean to prove some stuff. The infrastructure is non-trivial, especially at scale. Do you want to talk a little bit?

是的，是的。

Yeah, yeah.

我们刚刚发布了 Axel，AXLE 代表 Axiom Lean Engine。它是一套为 Lean 语言构建的证明验证和操作工具，用 Lean 语言编写，本质上是元编程工具。元编程人才极其难找，我们很感激有一个非常出色的团队在做这件事。我们希望免费向社区发布这些工具，因为我们认为可能还有其他人在进行大规模的 Lean 操作，这些工具能让他们的工作更稳健、更快速，并且能规模化。Axel 目前包含 14 个这样的工具，从验证证明开始，确保没有奇怪的事情发生，没有通过 Lean 代码作弊。你不会用公理来偷懒，也不会假设奇怪的东西。如果你把 m + n = n 作为公理，就能证明 2 + 2 = 2，这显然不对。还有很多其他生成工具，比如你可以尝试不同的修复方法：输入有问题的 Lean 代码，输出正确的 Lean 代码。目前还有其他基于语言模型的修复方法。希望我们提供的工具能更便宜、更直接。强大的工程能力可以带你走得很远。Lean 社区的很多人已经用 Axel 做各种有趣的事情，才一周时间。我们看到区块链社区的人用它做有趣的事情。我们还听说很多人把 Claude 加 Axel 作为他们目前的标配。这些工具非常有趣。今天有位数学家说，他用 Claude 证明了一个 Ramsey 结果，然后用 Axel 工具形式化了 Lean 证明。我们已经看到人们在使用它了。

So, we just released Axel, A X L E, stands for Axiom Lean Engine. And it's really a set of proof validation and manipulation tools that are built for Lean in the language of Lean. So it's a bunch of meta-programming tools. Meta-programming talents are extremely hard to find, and we're so grateful to have a really cracked team working on that. We want to release it to the community to use for free because we think there are probably other people doing large-scale Lean operations, and these tools will make their stuff a lot more robust and faster and do so at scale. Axel is currently 14 such tools, starting from verified proof, which ensures there's nothing weird going on, no cheating by Lean code. You don't axiom something out, you don't assume weird things. If you axiom m + n = n, you can prove 2 + 2 = 2, which is certainly not the right answer. There are also a lot of other generation tools. For example, you can try different repair attempts: broken Lean in, good Lean out. There are currently other repair methods by LM. Hopefully, what we provide can be a lot cheaper and more straightforward. Strong engineering can get you to a place that's quite far. A lot of people from the Lean community have been using Axel for just a week to do all sorts of interesting things. We've seen people from the blockchain community use it to do interesting things as an actor. We've also heard from a lot of people that Claude plus Axel is their go-to setup for now. We think these are really interesting tools. Today, there's a mathematician who said he formalized the Donald News using Claude to prove a Ramsey result and then formalized the Lean proof, also using Axel tools. So we already see people using it.

我觉得这也是陶哲轩所说的协作的好机会，一旦人们有了通用工具，事情就变得容易了。即使你不是像我这样很强的数学家，只要有直觉，也可能参与证明更大定理之类的工作。

I feel like this is a great opportunity for the collaborations that Terence Tao was talking about as well, where once people have access to the common tools, then it becomes easy to do. If you have an intuition, even not a strong mathematician like myself, you might be able to participate in an effort to prove a larger theorem or something like that.

是的，我觉得这非常有趣。想想数学，它不像软件工程那样协作性强。你不会看到成百上千人一起做一件事。Polymath 项目就是一个例子，非常棒。如果你有好的基础设施和大众化的访问权限，大家都能参与。一些大型形式化项目就是这样做的：把任务分成子任务。但陶哲轩和 Alex Kontorovich 的蓝图编写过程——把任务分配给不同的人，并理清各部分如何组合——这部分极其重要。有一家公司在球体堆积问题上取得了成果，其中八维的蓝图部分仍然建立在球体堆积社区、Lean 社区和人类蓝图的基础上。其他一些结果也是如此。蓝图部分仍然是由人类生成的。我认为自动生成蓝图将成为许多人同时试图解决的技术瓶颈。

Yeah, I think that's very interesting. If you think about mathematics, it has not been as collaborative as software engineering. You don't have hundreds and thousands of people working on something together. Polymath was an instance when that happened, and it was fantastic. If you have a lot of good setup, commoditized access, then people can all participate. That's how some of the large formalization projects have been done: things are divided into subtasks. But the blueprint writing process by Terence Tao and Alex Kontorovich, assigning tasks to different people and figuring out how things fit together, that blueprint writing part is extremely important. There has been a result about sphere packing by one of the other companies, and the blueprint part for the eight dimensions was still built on what the sphere packing community, the Lean community, the humans blueprint. Similarly with some of their other results. The blueprint part has still been human generated. I think auto-generated blueprint is going to be a technical bottleneck that many people are trying to solve around the same time.

那么，作为一个 Claude Code 用户，如果我对数学没有很深的理解，只有高层次的理解，尝试做一些小的 Lean 项目有价值吗？

So, is there value in me, as a Claude Code user, trying to attempt some small Lean or whatever, where I don't have a great understanding of the math? Maybe I have a high-level understanding.

这取决于你想形式化或证明什么。

Depends on what you are trying to formalize or prove.

证明东西。

To prove things.

是的，所以可能是形式化。你显然会从形式化开始，对吧？你知道证明，但就是做不出来。没人能正确形式化。实际上，我确实认识一些人，他们用手工方式使用 Lean 和形式化，不用任何 AI，以此作为学习数学的方法。这很有趣，因为我很多朋友开始研究 Lean 和 mathlib，是因为他们在读博士，过程很艰难。我们经常卡住，想复习一些本科课程，那时我们还理解数学是什么，于是通过做 Lean 来学习。我觉得这很美。但如果你有能形式化东西的自动证明器，你就会失去 Lean 学习过程中的那部分。

Yeah, so maybe formalize. You would obviously start with formalization, right? You know the proof, you just can't get it. Nobody has been able to get the formalization correct. I do actually have some people use Lean and formalization, and they try to do it by hand, not using any AI, as a way to learn mathematics. It's interesting because a lot of my friends who started working on Lean and mathlib were because they were in PhD and it's pretty hard. We get stuck all the time and we want to review some of the undergrad classes, a time where we still understood what the math was about, and we do so by doing Lean. I think that's very beautiful. But if you have access to action provers that can formalize things, you lose that part of the Lean learning process.

是的。

Yeah.

但我确实认为，你和我可以设置 Axel，看看我们能证明什么结果。我觉得这很有趣。多亏了 Axel 让速度更快，你不用等很久。我记得普特南考试那天。我们都在作战室里。那是个星期六。我们都很兴奋，刚拿到官方机构发来的试卷，是疫情期间的监考。我们在看 Axel 完成了多少工作。没有它，我们不可能在规定时间内解决那八个问题。肯定不行。我认为这些工具的一个特点是，它们可能为强化学习提供有趣的奖励。

But I do think that you and I can set up Axel and try to see what results we might be able to prove. And I think that's quite interesting. Thanks to Axel making the speed a lot faster, you don't have to wait very long. I remember the Putnam exam day. We were all in the war room. It was a Saturday. We were all really excited and we just got the exam paper from the official organization, the proctor for the pandemic exam. We were looking at how much work Axel was getting. Without it, we couldn't have solved the eight problems within the time limit. That would definitely not be within the time limit. I think one thing about these tools is that potentially you can have interesting reward for RL as well.

你指的是什么？

What do you mean by that?

例如，验证证明可以作为一个完全正确且经过验证的证明的奖励。

So, for example, verified proof can be a reward for a proof that is completely correct and validated.

我明白了。

I see.

我认为形式化验证工具可以成为强化学习的一个有趣方向。

I think formal verification tooling can be an interesting direction for RL.

是的，所以你的意思是，例如，你可以形式化非形式化证明，然后验证它，并以此作为奖励？还是说……

Yeah, so you mean, for example, you could formalize the informal proof and then verify it, and use that as a reward? Or do you mean...

不，我的意思是把 Lean 程序输入这些形式化工具，你会得到某种分数。

No, as in you pass Lean programs into these formal tools, and you will have some sort of score.

好的，明白了。

Okay, yeah.

我想如果我要构建一个类似的东西，我会在心里用我刚才描述的方法。但你说只是学习如何做 Lean。

I think if I were to build a one or something, I would have in my mind I would have used what I just described. But you're saying just to learn how to do lean.

所以，Frontier Labs 的价值主张有趣之处在于，假设你是一个面向消费者的业务，那么当然，你可以不采用我们的做法。我们看到过比如 DeepSeek，最初有一个形式化团队，后来因为战略方向变化而解散了那个团队。这完全合理。现在，假设你专注于编码，对吧？你有想从事我们正在做的事情的人才，那么你去做代码生成、进一步增强你的优势和护城河就更有意义了。

So, the value proposition which is interesting about Frontier Labs is that suppose you are a 2C business, then sure, you can just not do what we are doing. And we have seen for example, DeepSeek or like originally having a formal team and then later dissolve that team because of strategic direction change. That's all completely reasonable. Now, suppose you are focused on coding, right? And you have talent who want to work on what we are doing, it makes a lot more sense for you to do code generation, further your strength and moat.

是的。

Yeah.

而且你可以与 Axiom 合作，就像 Frontier Labs 与从事搜索的初创公司（如 Exa 和 Parallel）合作一样。没错，只需调用 API 进行搜索。可能，如果你来自这里，我认为你应该调用 API 进行验证。

And you can partner with Axiom just like how for example, Frontier Labs partners with startups that work on search such as Exa and Parallel. Right, just call API for searching. Potentially, you know, if you're from here I think you should call API for verification.

是的。

Yes.

更好的主张是它没有意义。我的意思是，可能问题在于人才、Lean 的挑剔性、数据代码之类的东西，你知道，没有理由这么做。

Better proposition was it doesn't make sense. I mean it just, you know, potentially it's in the talent the finickiness of lean the sort of data code like you know, there's no reason to.

是的，我的意思是设置只花了我 5 分钟。

Yeah, I mean it took me 5 minutes to set up.

你为什么决定创办 Axiom？你是斯坦福的研究生，学数学的。

Why did you decide to start Axiom? Like you were a grad student at Stanford and you know, in math.

是的。

Yeah.

那么，是什么让你决定……

So, what made you decide to...

在数学领域很久了。我觉得几乎一读博我就开始融资了。所以，并不是……

In math for a very long. I was I was a I think like almost as soon as I started the PhD I just started fundraising. So, it wasn't like...

哦，真的吗？好的。

Oh, really? Okay.

是的。

Yeah.

那是计划好的，还是你一开始就几乎立刻意识到这是……

Was that the plan or did you start there and you're like almost immediately realize that this is...

对。对。所以，法学院那一年，对吧？在智力层面上，它对我来说非常非常有趣。但这也是我人生中第一年完全没有科学、技术或数学。那是奇怪的一年，对吧？我读了很多书。我练习写作，学习阅读。但我也很想痴迷于技术方面的东西。那一年也是那样。所以，是的，法学院那一年，对吧？这对我来说非常有趣，因为我想，我需要痴迷于一个技术性的东西，否则我会……我不觉得无聊，因为我真的很喜欢法律的一切。我非常非常喜欢它。它是一门非常有趣的研究学科。但我基本上一直对推理的进展感到非常兴奋。我看了很多后训练的论文。我自学了所有这些。然后到了某个时候，我觉得这肯定会发生。而且我觉得每个周末和 Verve 的 Shubha 聊天也没有平息这些想法。所以我越来越痴迷。到了某个时候，我想：“好吧，如果我每时每刻都在做这件事，无法思考其他事情，那我需要做点什么。”我的意思是，我疯狂地爱上了 AI 会做数学这个想法。然后我想：“好吧，现在我该做数学吗？”那真的很疯狂，我记得当时痴迷到无法自拔。然后我去了一个 Hennessy 之夜活动。那是 Hennessy 学者餐厅举办的各种免费午餐活动，很棒，因为你可以免费吃饭，还能接触到有趣的智力内容。我记得 Julie Zhuo，我想她是 Facebook 的第一位产品经理，来演讲。之后我基本上走到她面前，说：“如果你想创业，但又真的很想做学术，因为你有点喜欢数学，你会怎么做？”然后她说：“嗯，你在这两件事上花了多少时间？”我说：“100% 对 0%。”然后她说：“嗯，你基本上得跟随你的能量。”

Right. Right. So, the year of law school, right? It was very very interesting to me like on an intellectual level. But it's also the first year where I had no science, technology, or math whatsoever in my life. It's a weird year, right? Like I'm reading a lot. I'm practicing well, I'm learning how to write. I'm learning how to read like And but like I'm just kind of I want to like be obsessed about something in technology. Like that was also what's going on that year. So, yeah, the year of law school, right? And it was very very interesting to me because it's like okay, like I just I need to be obsessed with like a technical thing cuz otherwise I get to I don't think I'm bored because I really love like everything about about law. I really really loved it. It was it was something that's incredibly interesting to study. But I just I mean I've been basically like, you know, very excited about like the progress of reasoning. I was looking at a lot of the post training kind of papers. I was I learning all of these like just by myself. Um and then at one point it got to a point where I'm like I think this is for sure happening. And like I think talking to Shubha right at at Verve like every weekend also like it didn't help like soothing these thoughts. So I got more and more obsessed. And at a point I'm like, "Okay, if I'm doing this like literally every minute and I can't think about something else. Like what you know, I need to do something about it." I mean it's like you I I fell madly in love with the idea that AI's going to do math. And I'm like, "Okay, now do I do I do math?" Like I it's really really crazy like at the time where I remember the obsession was quite I just couldn't get out of it. And then um I went to this night Hennessy event. It's night Hennessy scholar dining house like hosts all sorts of like free lunch events and those are great because you get free food and you get interesting intellectual exposure to things. And I remember Julie Zhuo who was I think a Facebook first Facebook PM came to speak. And then after that I just like basically walked up to her and I said like uh like what do you do if you want to do a startup and you really wanted to do academia because you you kind of love math. And then she's like, "Well, you know, what's your time spent on these two different things?" And I'm like, "100% 0%." And then she's like, "Well, you kind of have to follow your energy."

是的，我的意思是如果你完全痴迷于此。

Yeah, I mean if you are completely obsessed with it.

是的，我完全痴迷于此。我认为这将会很重大。而且我认为它必须是一个营利性初创公司，因为它比取得数学突破要广泛得多。嗯。如果你考虑递归自我改进，以及更高级的概念，比如你真的想要一个 AI 科学家。数学推理将是其中相当大的一部分。现在，我认为 Coursera 和 Claw 等人的信念是，就像大规模迁移到代码，代码迁移到数学一样。我认为这是真的。只是，为什么不直接推动呢？我不明白。你需要直接推动。然后还有另一个想法，也许回到协作点，对吧？验证传统上被认为是，好吧，有些行业有很多护栏。所以，如果你在国防、军事领域工作，你需要满足很多进入壁垒来达到那些严格的要求。所以，验证是为封闭行业服务的。但现在是第一次，我认为经过验证的 AI 是为了开放协作。无论是人机协作。之前，蓝图之类的是人人协作，Lean 是基础，是验证的形式化语言。然后是人机协作，就像我们现在看到的，未来 AI 智能体之间的协作。所以，我认为经过验证的 AI 是为了开放性。不是为了满足封闭行业的要求。而且我认为验证不应该是关于……我记得有篇文章说 Trevorrow 提出 AI 是幻觉的数学解决方案。对我来说，验证不是关于损失。验证是关于扩展 brilliance，复合 brilliance。就像回到协作点。就像 Ramanujan 是一个更强的数学家。他已经很强了。但验证帮助他扩展了 brilliance。就像既向上扩展又向外扩展。所以，验证更严谨。对我来说，验证不是关于消除错误、损失。而是关于扩展 brilliance。第三点是，对我来说，验证不是仅仅谈论严谨性。

Yeah, I was completely obsessed with it. I thought this is going to be big. And I thought like it just it just has to be a for-profit startup because like it's so much broader than making mathematical breakthroughs. Mhm. If you think about like recursive self-improvement and like really the the kind of more high-level like concept of like you really want to have just AI AI scientist. Like the math reason is going to be is going to be a pretty big part of it. And now trying like I think that the the sort of belief by by Coursera and claw and other folks is like, okay, like just like mass transfer to code and code coding transfer to mass as well. I think that's true. It's just that like, you know, why why not push it directly? I don't I don't get it. You need to push that directly. And then there's this other like, you know, thought which is that and maybe kind of going back to the collaboration point, right? Um verification has traditionally been thought of as, okay, well, there are some industry where there's a lot of guardrails. So, if you're working in defense, military use, okay, you need to like basically satisfy a lot of barriers to entry to meet those stringent like requirements. So, it's it's something that's verification is for the industries that are closed. But it's for the first time now I think verified AI is to open up collaboration. Either it's human AI collaboration. Well, before a blueprint like that's human human collaboration and lean was the grounding was the verification formal language. And then human AI collaboration like we're seeing now future AI agent agent agent like collaboration. So, like I think verified AI is for openness. It's not for meeting the requirements of closed industries. And I think just like I think verification should not be about, oh, I remember like, you know, there's article like Trevorrow makes the up is AI is a solution to, sorry, is math solution to hallucination. Verification to me is not about lossiness. Verification to me is about scaling brilliance, compounding brilliance. It's like just to kind of going back to the collaboration point. It's about Ramanujan being a much stronger mathematician. He was already a really strong one. But verification helps him extend the brilliance. Like both kind of like scale up and scale out. So, verification is more rigorous. Verification to me is not about, you know, like erasing the mistakes, the the lossiness. It's about scaling brilliance. And And the third point is that like verification to me is um not about like the sort of, you know, just talking about rigor.

这实际上关乎性能提升，对吧？不仅仅是严格的要求和需要克服的障碍，而是实际的验证生成会让它变得更好。

It's actually about performance gain, right? It's not just about the stringent requirements, the hurdles that you need to overcome. It is about like actual verified generation is going to make it so much better.

我认为这三点中，最后一点是很多人觉得你做验证是因为你不信任技术。这在大众中很受欢迎，包括我父母，他们会说“哦，我们做验证是因为技术会犯错”。不，我们做验证不是因为不信任技术，而是因为预期的快速指数级扩展以及技术的部署和创造，技术进步本身要求并推动了这一点。

And I think kind of these three points, I think the last point is that a lot of the people think that you work on verification because of your distrust for technology. Like it sells really well to I think the general public, including like my parents, like oh why we're doing verification because like, you know, technology make mistakes. It's No, we don't think verification is based on it's because of the distrust for technology. It's because that's what like um expected rapid exponential scale up and um the deployment and the creation of technology and technological progress is what that compels and demands.

这是一个非常数学化的视角，对吧？因为你说证明驱动数学，很多数学都基于证明。数学驱动了世界上很多科学和创新，而数学的创新又推动了世界的创新。

It's a very mathematical perspective, right? Because you're saying proofs are proofs are drive math, right? A lot of math is based is is about proofs. And math drives a lot of science and innovation in the world and the innovations in math drive innovation in the world.

但甚至不需要通过“解决数学就解决一切”这种说法。我的观点是，迁移学习是关于弥合数学推理的差距。所以这里有几个叙事：对一些人来说，你解决数学，然后数学是科学的基础，这是从“AI for math”到“AI for sciences”的理论层叙事。我们实际上相信一般的迁移学习。我认为 Axiom 处于基础设施层。

But it doesn't need to even go through like in in terms of, you know, the solve math solve everything thing like obviously stands. Like my point is like transfer learning doesn't like transfer learning is about like closing math math reasoning. It just So so there are kind of I guess like there are a couple narratives here. Like for some people is that you you solve math and then maths are the, you know, fundamentals of sciences. So that's actually the from AI for math the like take the theoretical layer of AI for sciences that narrative. We actually believe in just like general transfer learning. Like I think I think Axiom is Axiom is on the infrastructure stack.

你认为这只是第一步，基本上解锁了科学和法律等许多领域的能力？

And you think that this is just a first step to, you know, basically unlocking capabilities in many domains in science and law, for example.

是的。所以又有多种信念。一种信念是数学和形式验证的力量。假设我们真的解决了数学，有了一个非常强大的非形式数学推理引擎，我们不期望它的效果能像通过形式方式解决数学那样大。

Yes. I think it's So so again, there are like, you know, multiple multiple kind of like beliefs. One belief is that there's math and there is like, you know, formal the power of formal verification. Suppose we actually, you know, solve math and have a really strong informal math reasoning engine, we do not expect that 10 to be as large as solving math through the formal way.

为什么？

Why?

我的意思是，代码虽然是一种语言，但它确实处于更结构化的那一端。

I mean, code as as it is language, but it is indeed on the more structured end.

是的。

Yes.

它连接了非形式和形式。

It bridges informal and formal.

是的。

Yes.

我们做的不是非形式与形式对立，也不是完全形式化的证明方法。它是在非形式和形式之间架桥，在高层次和低层次之间架桥。这是一种通过推理的直接改进，就像迁移学习。它也是间接的，因为数学会解锁很多科学，而这正是我们看到的。

What we are doing is it's not informal versus formal. And we're not taking the sort of like completely formal of approve approach. Like it's it's bridging between informal and formal. It is bridging between high-level and low-level. It is a direct it's sort of like a direct improvement through reasoning so transfer like transfer learning. And it's also indirect in that like okay, well, like math is going to unlock a lot of science and sure. And that is really what we are seeing.

所以你认为它实现了迁移学习？

So you think that it enables transfer learning?

是的。

Yeah.

我明白了。

I see.

我认为这几乎是共识。这是一个被其他人忽视的赌注，因为数学听起来很纯粹，似乎没有任何商业价值。

I think that is that is pretty much a consensus. I think it is a consensus and this is the bet that has been pretty much kind of overlooked by others because of math sounds pure and it doesn't sound like there's any commercial value.

嗯。

Mhm.

我当然理解机会，比如如果你是一个前沿实验室，解决这个问题的机会成本。但我绝对认为，如果你是一个资源充足的初创公司，你应该做这件事。

Well, I do obviously understand the opportunity like the opportunity cost if you're like a really like a frontier lab of of solving this problem. But I definitely think this is a problem that if you're like a well-resourced startup you should be doing.

这是一个有趣的观点。你想说的都说完了吗？

That's an interesting perspective. Did you get everything out that you wanted to say?

我认为，比如问题是 Axiom 是数学还是验证。公司的 DNA 是数学。所以我们认为验证是最好的第一个市场。

I think it's like you know, like the question of like is Axiom math versus Axiom verification. The DNA of the company is math. So we think that verification is the best first market.

是的。

Yeah.

我们认为解决数学，尤其是形式数学，将帮助我们应对验证 AI 这个雄心勃勃的追求。当我们完成这个，我们可能会有第二个市场，包括我们刚讨论的 Alpha Science。但在理论层面，我认为现实世界测试很重要，可能我们可以停留在数字世界和软件领域。而对于其他事情，比如物理或信号，才能获得回报。

And we think that sort of like solving math and especially like formal math is going to like help us like tackle the really ambitious quest of verified AI. Now, when we are done with that, we might have other that second market including Alpha Science we just talked about. But but on the theoretical layer, right? Like I think real world testing is important and potentially we can stay in the digital world and and stuff software stuff. And for other things to be to be to be getting reward like physical or signals.

但你认为，拥有真正强大的推理能力……

But do you think that that the the sort of the capability of doing really powerful reasoning

一样。

Same.

一旦你有了那个强大的验证推理引擎，那一刻我们就解锁了软件验证、硬件等等。但现在，生物学呢？化学呢？

once you have that powerful verified reasoning engine, that that's the moment when okay, now we've unlocked that for you know, software verification and hardware or or whatever. But now okay, so now what about biology? What about chemistry?

一个是这个。另一个是，你离递归自我改进有多远？

be one. The other one is then like really how far are you to recursive self-improvement?

好的，所以就是 AGI。

Okay, so just AGI.

是的。我认为这个问题因人而异，不同背景的人有不同的看法，这取决于你的精力和热情所在。比如我的一些朋友，他们想研究 AGI，因为他们相信解决 AGI 就能解决死亡。另一些有医学背景的人，他们真的相信可以直接解决死亡，而不通过 AGI，他们只是做 AI for science。

Yeah. I think there is this sort of question and different people because of their probably different backgrounds have different it's really where your energy and your passion leads you. Like for some people actually, I have heard just actually, you know, with my friends, they want to work on AGI because they believe solve AGI solve death. There are other people who come from a more like medicine background. They really believe they can solve death and they don't solve AGI and then solve death. They just solve like AI for science.

是的。

Yeah.

现在，哪种方式正确？我不知道。

Now, which way is correct? I don't know.

所以从递归自我改进的角度来看，你似乎在说验证加上非形式语言的组合，能够实现非常好的递归自我改进。

And so you the recursive self-improvement angle, it sounds to me like you're saying that the combination of verification plus the sort of like language which is informal, it's that combination enables really good recursive self-improvement.

递归自我改进无论如何都会发生。我们试图让形式验证占据一席之地。

recursive self-improvement is going to happen anyways. We're trying to have like formal verification Earnest place.

所以，形式验证能否被欢迎、部署并成为共识，取决于我们执行得如何。

So we we like again, the whether um formal verification can be welcomed and deployed and become a consensus depends on how well we execute.

我认为当你把问题归结为执行问题时，就应该直接去做。

And I think when you boil down that problem into an execution problem, you should just go for it.

展望未来，你认为这个领域，对 Axiom 和整个领域来说，最大的瓶颈是什么？

What looking forward, what's the biggest bottleneck that you see in the field for both Axiom and maybe just the field at broad in terms of

碎片化。我认为我们处于一个市场，人们喜欢各自为战，一千个人不联合起来，而是开始一千件事。我认为这实际上是最大的泡沫指标。有些类别是泡沫，有些类别是登月计划。这不是泡沫，只是看起来有点泡沫化。

Uh fragmentation. So um I think we're in a market where people like to start like, you know, that a thousand people they don't join forces start a thousand things. I think that's actually the biggest like kind of bubble indicator. I think there are categorical bubbles and there are like other categories where there are moonshots. It's not bubble, it just looks a little bubbly.

在这个领域，如果那些背景非常扎实、真正有实力的人决定联合起来，为了使命而非为了自我或作为新左派创始人的地位而团队合作，我认为这类情况我非常看好。反之亦然。所以，我认为瓶颈实际上在于——这很烦人，因为我们正处于一个研究的时代，如果你相信深度科技是值得追求的有趣方向。目前的市场条件有好有坏：好的一面是它能让这些长期、长远的赌注获得资金；坏的一面是噪音太多，还有一些非理性的参与者。我们努力与非常出色的风险投资公司合作。他们是我们的合作伙伴，是智力上的伙伴，我们有很多共识。我们长时间地互相交流非常酷的想法，无论是技术还是非技术方面的，而且我们花很多工作之外的时间，包括周末，一起高强度地建设公司。但也有其他人只是想找个地方停放资本。虽然我们不与他们合作，但这些市场条件助长了碎片化。当事情变得碎片化时，没有人能到达终点。我认为每个类别，无论想法多么正确，都处于一种“赢得存在权”的阶段。如果是这样，那么例如伟大的深度科技公司 SpaceX——人们确实会联合起来为那个梦想而工作，可能还有一个非常有魅力的创始人。我个人非常担忧的一点是，对于其他我相当看好的类别，碎片化是一个问题。我们看到教授们被从大学里拉出来去做一些事情，而这确实是一个非常有趣的情况。

In the field, if people who are really legit, with strong backgrounds, decide to join forces and work in a team for the mission rather than for ego or status as a new left founder, I think that category is something I'm really bullish on. Other than that, vice versa. So, I think the bottleneck is actually about — it's annoying because we are in an age of research, if you believe in deep tech as the interesting direction to go after. The market conditions currently are good and bad: good because they enable these long-term, long-horizon bets to be funded; bad because there's too much noise and some irrational players. We try to work with really incredible venture firms. They are our partners, intellectual partners, and there's a lot of alignment. We bounce very cool ideas, technical and non-technical, off each other for long hours, and we spend a lot of time off work and on weekends together to intensely build the company. But there are also other people who just want to park capital somewhere. While we don't work with them, these market conditions encourage fragmentation. And when things get fragmented, no one gets there. I think every category, regardless of how right the idea is, is in a sort of 'earned the right to exist' stage. If that is the case, then for example, great deep tech company SpaceX — people actually join forces to work on that dream, and potentially also a very charismatic founder. A really concerning thing for me personally is that for other categories I'm quite bullish about, fragmentation is a problem. We see professors being pulled from universities to work on something when it's a really interesting situation.

也许这是个天真的问题，但刚才你谈到AI for math领域的参与者，有你、Harmonic，还有那些大实验室，对吧？我漏了谁吗？这真的算碎片化吗？

Maybe this is a naive question, but right now when you were talking about players in, let's say, AI for math, where you have you, Harmonic, and then the big labs, right? Am I missing someone? Is that actually fragmented really?

我想碎片化是整个AI领域的瓶颈。

I guess fragmentation is a bottleneck for the entire AI landscape.

好的，是的。

Okay, yeah.

我认为AI for math这个类别实际上不是一个泡沫，因为它没有碎片化。那些真正有才华的人确实喜欢联合起来。例如，我们团队能请到Keonno和Francois Charton，这太棒了。你有一个来自DeepMind的核心贡献者，他做了非常棒的基准测试，还有Francois，他从事AI for math的证明与发现。他们一起工作。然后你突然就有了一个兼具已验证能力和构建能力的参与者。这太棒了。而且我相信，正如你所说，Harmonic可能也有一些非常优秀的人才联合起来。我认为AI for math是一个好的类别，因为它没有碎片化。但即使从我们的角度来看，例如强化学习（RL）？我不认为那本身是一个类别，但RL人才目前对几乎所有人来说都很难吸引和留住。有很多公司成立三个月后就卖掉了。每个月你本可以解决一个技术问题，却花在了交易上，这一个月就浪费了。我这么说带着一些痛苦和煎熬，因为我经历过两次融资。

I think AI for math is a category that is actually not a bubble because it is not fragmented. People who are really amazing talents do like to join forces. For example, the fact that we got Keonno and Francois Charton on the team is fantastic. You have someone who's a core contributor from DeepMind for really great benchmarks, and Francois who's on the AI for math discovery at proving and discovery. They work together. Then you are suddenly a player with both proven capability and construction capability. That's fantastic. And I believe, as you said, Harmonic probably also has some really great talents joining forces. I think AI for math is a good category because of the absence of fragmentation. But even from our perspective, for example, RL, right? I don't think that's a category per se, but RL talents are currently quite hard to attract and retain for literally everyone. There are a lot of companies being started and sold 3 months later. Each month where you could have worked on a technical problem and you're instead working on deals is a month that is wasted. I say that with some pain and suffering because I've gone through two fundraisers.

是的。那么AI for math最大的瓶颈是什么？

Yeah. So what's the biggest bottleneck in AI for math?

对于Axiom在AI for math方面。

For Axiom for AI for math.

不是Axiom，而是整个社区。

Not Axiom, but just the community.

但就是AI for math的社区。

But the community of AI for math.

它走向何方？大家真正想突破的是什么？

Where is it going? What is the thing that everyone just really wants to break?

我预计随着Axiom和Harmonic确立类别领导地位，碎片化会开始出现。所以我认为这是一件事。但我也认为另一个瓶颈可能是短期与长期的压力。我认为我们做事节奏非常快。但这并不意味着总是以最快的节奏做事就是正确的。我们做事节奏快是因为我们在国际数学奥林匹克竞赛（IMO）当天成立，所以我们无论如何都无法参加那场比赛。下一场数学竞赛是普特南（Putnam），我们很兴奋，因为这是一场本科生考试。今年的IMO 2025在MOHS难度标尺上相对容易，而普特南可能很难。事实上，如果你看AI在平均得分和题目最大难度上的表现，普特南在两个维度上都更难。所以我们想尝试，而且只有4个月的间隔，但这并不意味着我总是设定4个月的目标。如果我仅仅设定4个月的目标来建立公司，我可能会建立一个非常短视的公司。所以我看到了更长周期的问题。例如，市场力量可能迫使其他参与者进入行程验证（trip verification）。核心验证（core verification）可能是圣杯。有可能如果你解决了核心验证，那么你也会自然解决行程验证，只需考虑分布偏移的epsilon修正。但我坚信瓶颈可能是压力。但我认为Axiom很幸运，我们足够早期，而且我们是一个由极高自主性的人组成的团队，所以我们的执行通常超出预期。但我认为整个AI for math领域可能的一个瓶颈是，试图证明商业价值会严重分散对核心能力提升的注意力。

I expect fragmentation to start to happen as Axiom and Harmonic establish category leadership. So I expect that's one thing. But I also think another bottleneck could be the pressure of short-term versus long-term. I think we are doing things in a very fast-paced manner. But that does not mean it is always correct to do things in the most fast-paced manner. We do things in a fast-paced manner because we were founded on the day of the International Math Olympiad, so we couldn't have competed in that anyway. The next Math Olympiad is Putnam, and we're quite excited because it's an undergraduate exam. This year's IMO 2025 was easy on the MOHS scale, and Putnam could be hard. In fact, it was harder than the IMO on the MOHS scale if you look at how many scores the AI has retained on average and on the max difficulty of the problem. Putnam is harder on both axes. So we want to try, and there's only a gap of 4 months, but it doesn't mean I'm always going to set 4-month goals. If I build a company only setting 4-month goals, I might build a really short-sighted company. So I see longer horizon problems. For example, market forces could force other players into trip verification. It is possible that core verification is a holy grail. It's possible that if you solve that, then you also naturally solve trip verification with some epsilon caveat of distribution shift. But I strongly believe that a bottleneck could be the pressure. But I think Axiom is fortunate that we are early enough, and we are a team of incredibly high agency people, so our execution generally surpasses expectation. But I think what could be a bottleneck for the entire AI for math field is that potentially trying to prove commercial value is going to distract significantly from core capability improvement.

是的。有道理。太好了。谢谢你开车过来看我们。

Yeah. That makes sense. Cool. Thank you for driving up and coming to see us.

非常感谢。是的。

Thank you so much. Yeah.

我知道交通很糟糕。

I know the traffic was horrible.

是的。谢谢。

Yeah. Thank you.

和你谈话真的很愉快，我们期待看到事情如何发展。

And it's been really a pleasure speaking with you and we look forward to seeing how things develop.

是的。非常感谢。

Yeah. Thank you so much.

谢谢。

Thank you.

太棒了。谢谢。是的。

Awesome. Thank you. Yeah.