为什么Harmonic的Vlad Tenev和Tudor Achim认为AI即将改变数学——以及这为何重要

我上次查看时，有43%的概率下一个千禧年大奖难题将由AI解决，或者由人类在AI的显著辅助下完成。我认为我认为这个估计偏低了。我的意思是，我们可能很幸运，拉里·古斯可能正在研究黎曼猜想的道路上，那将非常了不起。但我认为，你知道，如果下一个难题是由人类解决的，那很可能必须是在不久的将来。而且可以肯定的是，再下一个难题很可能将由AI主导解决。

Last I checked, there's a 43% chance that the next Millennium Prize will be solved by AI or, like, human with significant AI assist. I I think I think that's an underestimate. I mean, we could be lucky, and Larry Guth might be on the on the path to the Riemann hypothesis, which would be amazing. But I I think that, you know, if if the next one is solved by a human, it would probably have to be in the very near future. And for sure, the next next one will probably be significantly solved by AI.

我们很高兴欢迎弗拉德和Tutor来到节目。我们在红杉资本认识弗拉德多年，但你们很多人可能不知道，除了是Robinhood的创始人和CEO之外，他还是一位极具天赋的数学家。弗拉德和Tutor联手创建了Harmonic，这是一个旨在推动人类知识前沿的AI研究实验室。具体来说，他们希望创建数学超级智能，其核心理念是：理解数学能让你更好地理解和推理更广阔的世界。我们很兴奋能与Tudor和弗拉德讨论Harmonic，讨论创建数学超级智能的要素，包括合成数据、强化学习和自我博弈，以及AI何时能赢得IMO或千禧年大奖，甚至解决黎曼猜想。

We're excited to welcome Vlad and Tutor to the show. We've had the pleasure of knowing Vlad for many years at Sequoia, but what many of you may not know about Vlad is that in addition to being founder and CEO of Robinhood, he's also an enormously talented mathematician. Vlad and Tutor have teamed up to create Harmonic, an AI research lab with the goal of pushing the frontiers of human knowledge. Specifically, they hope to create mathematical superintelligence with the thesis that understanding math allows you to better understand and reason about much of the broader world. We're excited to talk to Tudor and Vlad about Harmonic, about the ingredients that go into creating mathematical superintelligence including synthetic data, reinforcement learning and self play, and when AI will win the IMO or a Millennium Prize or even solve the Riemann hypothesis.

好的。弗拉德·Tutor，欢迎来到节目。

All right. Vlad Tutor, welcome to the show.

嗯，谢谢邀请我们。

Well, thanks for having us.

好的。所以你们有一个核心信念，认为数学即推理，并且你们可能持有一个非主流的观点：训练一个模型在数学上表现优异的最佳方式是直接教它数学，而不是让数学作为规模扩展的副产品自然涌现——这是许多其他基础模型公司正在做的。你能谈谈这个核心信念吗？为什么需要直接教模型数学？另外，也许可以解释一下‘数学即推理’意味着什么？

All right. So you guys, you have this core belief that math is reasoning, and you have what might be a contrarian belief that the best way to train a model to perform well in math is to directly teach it math versus allowing math to emerge as a property of scale, which is what a lot of the other foundation model companies are doing. Can you talk a bit about that core belief? Why do you need to teach the model directly math? And also maybe what does it mean that math is reasoning?

当我们创办公司时，我们，你知道，非常专注于数学，也许我们稍后会谈到这一点。但是，你看，如果你环顾所有科学和工程领域，嗯，几乎是所有领域，数学确实是它们的基础。数学本质上已经成为人们理解宇宙的方式。它是你从黑洞到原子建模现象的方式。它是你在工程中设计事物的方式。

When we started the company, we, you know, had a really big focus on math and maybe we can get to that later. But, you know, if you look around at all fields of science and engineering, well, almost all fields, math is really at their foundation. And math has essentially become the way that people understand the universe. It's the way you model phenomena from black holes to atoms. It's the way you design things in engineering.

而且，你知道，这有几个原因。首先，宇宙恰好可以用数学来解释。所以你可以写下，你知道，相当复杂的符号集来解释事物。但另一个非常重要的事情是，它是一种构建这些，你知道，共享的认知理论的方式，这些理论非常客观、清晰和透明。如果你我在讨论一些严谨的事情，我们可以写下一套演绎规则，我们可以就我们正在建模的任何事情的基本规则达成一致。

And, you know, there's a couple of reasons for that. First of all, it just happens to be the case that the universe is explainable by math. So you can write down, you know, fairly complex set of symbols that explain things. But the other really important thing is that it's a way to build these, you know, shared cognitive theories that are very objective and clear and transparent. And if you and I are discussing something that's, you know, rigorous, we can write down a set of deductive rules, we can agree on what, you know, the ground rules are of whatever we're modeling.

然后从那里，我们可以推导出结论。对于人类来说，你会发现当人们非常擅长数学时，他们往往在科学和工程的其他量化领域也很出色。所以我们的赌注是，如果你打造一个真正擅长数学的系统，你很可能会看到同样的现象——它可能不会立刻写出世界上最好的历史论文，但当你要求它做科学或工程方面的事情时，它就会表现得非常非常出色。这就是我们从数学开始的原因。

And then from there, we can derive, you know, conclusions. And so with humans, what you see is that when people become very good at math, they tend to be good at other quantitative areas in science and engineering. And so our bet is that, you know, if you make a system that's really good at math, you're probably going to see the same phenomenon where it's true, it might not immediately write the world's best history essays. But when you ask it to do something scientific or something in engineering, it's just gonna be really, really good at that. That's why we started with math.

那么'帮我做数学作业'和'写一篇历史论文'之间的界限在哪里？存在一些数学难以跨越的边界。你认为以数学为核心的这个模型，其可能性的外缘在哪里？那些边界在何处？

And where is that boundary between, you know, help me with my math homework and write a history essay. There is some boundary that it's hard for math to cross. What do you think the outer edges of what's possible with a model with sort of math at its core? Where are those outer edges?

我给你们一个非AI视角的解读。我学过数学，从小数学就很好。我记得数学课上总有七年级学生，老师一提出什么抽象概念——比如三角形的边角边定理——他们就举手。

I'll give you sort of the the non AI perspective. So I studied math. And, you know, I I was really good at math from when I was a little kid. And I remember there were there were always, the seventh graders in math class that would raise raise their hands whenever the teacher would come up with something. It was always, a abstract thing, like, you know, the side angle side of triangles.

总有个烦人的孩子会问：'我们什么时候才会用到这个？'老师通常会含糊其辞地说：'你可能不会很快用到，但它会让你在其他方面变得很厉害。'其他孩子总是对此表示怀疑，但我相信了。所以我一直坚持学习更高级的数学。

There'd be the annoying kid that was, like, when are we ever gonna use this? And, you know, the teacher would kinda mumble a little bit, and they'd be like, well, you know, math just like you're probably not gonna use it soon, but it'll make you really good at at other things. And, you know, the other kids were always skeptical of that. And I bought into it. And so I just kept taking more and more advanced math.

后来我去了斯坦福大学，主修数学，然后又去读数学博士。我的信念是：只要专注于数学，我就能变得非常擅长解决问题。商业问题和其他问题，相比我每周花十个小时绞尽脑汁解决的抽象代数习题集，会容易得多。我认为这个想法基本上是正确的。

You know, I went to Stanford and I majored in it. Then I went to grad school to do a math PhD. And my belief was that, okay, if I just focus on math, then I'm gonna get really good at problem solving. And, you know, business problems and other problems will be easy compared to, you know, solving these, like, really tough, like, abstract algebra problem sets that I was banging my head against the wall for ten hours every week trying to do. And I think it basically ended up being correct.

对吧？我几乎没关注其他东西。在斯坦福我只修过一门计算机科学入门课。五年后当我成为创业者时，我发现学编程很容易，理解合同也很轻松。

Right? It's like I I didn't really pay attention to anything else. I took maybe, like, one computer science class intro to to computer programming at Stanford. And, you know, five years later, when I became an entrepreneur, I found it really easy to to pick up code. I found it really easy to, like, pick up contracts.

当然我不是律师，但你能理解那些东西。我的意思是，逻辑基础相比抽象代数和分析来说相对简单。所以我认为至少对人类而言——我把自己视为数学能转化为其他高变现能力事物的例子。对AI来说，我的直觉表明这应该也是一样的。

And, you know, of course, I'm no lawyer, but you could understand that stuff. I mean, the logical underpinnings are relatively simple compared to abstract algebra and analysis. So I I think for for humans, at least, I I consider myself an example of, like, math transferring to other very monetizable things. And I think for AI, my intuition seems to suggest that it should be the same.

是的。你已经看到一些这方面的迹象了，你知道，目前这在业内已是公开的秘密，即用大量代码数据进行代码训练可以显著提升推理基准测试的表现。所以你可以想象，当你拥有包含更广泛通用推理类型的惊人数学数据集时，情况会是什么样子。

Yeah. And you already see a little bit of evidence of this, you know, at this point, it's an open secret in the industry that, you know, code training on a lot of code data leads to much better performance on reasoning benchmarks. So you can imagine what that'll look like when you have incredible math data sets that encompass a lot more general types of reasoning.

是的，是的，这很有共鸣。这个想法是，数学在某种程度上教会人类如何批判性思考、如何逻辑思考，而这种技能可以迁移到许多其他领域。有理由认为这在人工智能领域也会奏效。弗拉德，你随口提到你学过一点数学，对于不太熟悉你数学背景的人，我相信你曾短暂师从陶哲轩，他可能是当今世界上最伟大的在世数学家。

Yeah. Yeah, that resonates. The idea that, you know, math kind of, math teaches a human how to think critically, how to think logically, and that skill can be ported to a bunch of other domains. It stands to reason that that would work in AI also. Vlad, you casually mentioned that you studied a little bit of math and just for anybody who's not quite familiar with your background in math, I believe you studied briefly under Terry Tau, who is perhaps the world's greatest living mathematician.

是的。然后你跟我们提到的一件事是，你仍然会时不时和他聚一聚。比如你在洛杉矶时一起吃午饭之类的。所以我很好奇，你和陶哲轩一起吃午饭时，你们都聊些什么？你会给我一些股票建议吗？

Yeah. And then one of the things you mentioned to us was that you still catch up with him every now and then. Have lunch when you're in LA, that sort of thing. So I'm curious, when you have lunch with Terry Tau, what do you guys talk about? Do you give me any do you give me stock tips?

不。不。我不被允许那样做。是的。有，有，是的。

No. No. I'm not allowed to do that. Yeah. One one of the, yeah.

作为金融领域的上市公司CEO，一个不幸的事情是，我有很多股票内幕消息，但是

One of the unfortunate things of being a public company CEO in the financial space is I have lots of stock tips, but

我不能分享任何一条。我

I can't share any of them. I have

必须，比如，把它们憋在心里，我甚至自己都不能用。我基本上不能再交易了，这很不幸，因为我热爱交易。但是，是的。我，我，所以回到我是怎么去UCLA的，陶哲轩是UCLA的教授，我认为他真正令人惊叹的是其工作的广度。大多数数学家会，比如，非常深入地钻研一个相当狭窄的领域，而陶哲轩可以在几十个领域都达到非常深的造诣。

to, like, keep them in term and I can't even use them. I basically can't trade anymore, which which is unfortunate because I love trading. But yeah. I I so to backtrack how I got to UCLA, I so Terry Tau is a professor at UCLA, and I think what's really amazing about him is the breadth of the work. So most mathematicians get, like, very deep into a pretty narrow domain, and Terry can get very deep across, like, dozens of domains.

你知道，他在数论、组合数学、调和分析、应用数学领域都做出了贡献。我相信他现在是Lean社区的主要贡献者之一。他正在用Lean形式化自己的论文，还活跃在社区Zulip上，与学生互动。他还有一个非常受欢迎的博客。我认为他能做到这些，是因为他比99.999%的人都要聪明，可能还不止。

You know, he's made contributions to number theory, combinatorics, harmonic analysis, applied math. He's one of the leading Lean contributors at this point, I'm sure. He's like formalizing his papers in Lean and actually hopping on the community Zulip and like, engaging with students. And then he has a very popular blog. And I I think the way that he's been able to do this is he he's just smarter than 99.999% of people, probably even more than that.

所以从很小的时候起，就很明显他处于另一个层次。我在本科时跟随这位教授Larry Guth完成了数学荣誉论文，他也很了不起。我是说，他最近出了一个突破性成果，我想是关于数论或黎曼猜想相关的内容。但没错，这个非AI数学领域的成果确实相当了不起。他还建议我考虑UCLA。

So from a very early age, it was very clear that that he was, like, on an on another plane. And I studied I did my math honors thesis in undergrad under this professor, Larry Guth, who's also really amazing. I mean, the he actually had a recent result that came out that was a groundbreaking result in, I wanna say, number theory or some something about the Riemann hypothesis. But, yeah, this this result in non a a AI math really was was quite something. And, you know, he he kinda suggested I I look at UCLA.

我当时对他的领域非常感兴趣，最终有幸去那里师从陶哲轩教授。但需要说明的是，我是个辍学生。虽然是在研究生之后，但我仍坚持自称辍学生。所以我只在UCLA读了一年。陶哲轩教了我第一年的研究生层次分析导论，这非常棒。

I was, like, really interested in in in his field, I ended up I ended up going there and being fortunate to study under professor Tau. But I should be clear, I am a dropout. And it's amazing that I can claim that after grad school, but I I will claim dropout status. So I only did one year of of of UCLA. So it was intro to graduate level analysis Terry Tau taught my my first year, which was pretty amazing.

我记得有一次和陶教授一起阅读，他给了我一本书并签了名。我想他签名是为了确保我读完后会还给他。但他没想到，签名反而保证了他永远拿不回那本书了。每次见到他我都会提起这件事，就像在说：嘿。

And the one thing I remember was I was doing some reading with with professor Tau, and he gave me this book and he signed it. And I think he signed it because he wanted to make sure I would give it back to him when I was done reading it. And little did he know that by signing it, he guaranteed he would never get that book back. And I I bring it up every time I see him. I'm like, hey.

那本书你别想拿回去了。它就在我的书架上，和其他签名首版书放在一起。

You're not getting that book back. It's on my shelf next to all my other autograph first editions.

数学界对AI数学怎么看？大家意见分歧吗？还是认为这是通往应许之地的道路，是我们解决黎曼猜想等所有问题的方法？

What does the math community think of AI math? Are people split? Or do people think it's, you know, the path to the promised land and the way that we're gonna solve Riemann and everything else?

我认为是分裂的。看起来确实存在分歧。年轻数学家似乎非常支持AI、支持验证和Lean这类工具。而年长一些的人则更为怀疑。这并不令人意外。

I think it's split. I I think it seems to be split. And there's sort of like the younger mathematicians, I think, are very, like, pro AI and and pro verification and and tools like Lean. And I think the the older folks are a little bit more skeptical. So not surprising.

我认为你在几乎所有领域都能看到这一点。是的。我的猜测是这会不断演变。我的思维模型类似于国际象棋，一开始可能会有一个漫长的时期，人类加上AI辅助，这将带来很多非常好的结果。但随着时间的推移，我认为AI会变得越来越好。

I think you see that in pretty much Yeah. Every field. I think that my my guess would be that this will evolve. My mental model is something like chess where, you know, at first, there will be perhaps a lengthy period of, you know, humans plus AI assist, and and that will lead to a lot of really good results. But over time, I think the AI will get better and better.

而且，你看现在的国际象棋，有点像，如果有人类辅助AI，AI可能会感到厌烦。它们可能只想删除所有人类输入，因为这只会让结果更糟。所以我不确定我们是否会达到那个阶段。我认为人类在某个时候仍然需要指导算法。但我觉得数学家的定义将发生根本性的改变。

And, you know, you look at chess right now, and it's sort of like, you know, if if there's a human assisting the AI, the AI would be, like, annoyed of it. They would just wanna just delete all of the input because it would only make the results worse. So I'm not sure if we're gonna get to that point. I think humans will, at some point I mean, they they'll need to guide the algorithms. But I I think the the kind of definition of what a mathematician will do will will fundamentally change.

我和我在MIT的一位数学家朋友聊天时问他，当我们刚开始接触这个时，你怎么看？这是一位年轻的教授，对这个领域非常兴奋。我问他，你是否担心自己所在的领域将发生根本性变化？他说，数学领域一直在变化。回溯到十九世纪，数学家们就像是皇家宫廷里的成员，他们是 glorified calculators（ glorified 的计算器）。

I I was talking to one of my friends who's a mathematician at MIT, and I asked him, you know, when we when we were kinda first starting this, what do you think? And this is a young professor, like, very excited about about the field. I was like, are are you worried that you're kind of in a in a field that is gonna fundamentally change? He's like, the the field of math has always changed. Back in the eighteen hundreds, mathematicians used to be kind of like in the royal court, and they would be glorified calculators.

他们曾经手工解二次方程。当然，他们担心当计算机和计算器出现时，这份工作将不复存在。但数学家们可以定义数学是什么。所以我确信在某个时候，数学家的角色将是提示和指导这些AI解决问题。我认为是的。

They would solve quadratic equations by hand. And, of course, the they were worried that, you know, when computers and calculators came out, the the job would no longer exist. But mathematicians get to define what math is. So I'm sure at some point, it'll be prompting and kind of guiding these AIs to solve problems. And I think yeah.

我认为这将非常巨大。所以即使AI解决了黎曼猜想，人类也总会参与其中，因为最初提出黎曼猜想的是人类。

I I think that's gonna be very huge. So even if an AI solves the Riemann hypothesis, a human will always be in the loop because the humans kind of pose the Riemann hypothesis to begin with.

是的。接着这个话题说，我认为未来会有大量计算资源专门用于数学。问题将是一个非常人性化的问题，即人类通过什么程序来决定如何引导所有这些推理火力。我认为这将成为数学家的工作，他们必须选择我们研究什么？如何解释结果？

Yeah. Just to hop on that, think there's like like in the future, you're gonna have a lot of compute resources dedicated to math. And the question will be like a very human one, which is like by which procedure do humans decide where to like direct all that, like reasoning firepower. And I think that's going to be like the job of mathematicians, have to choose what do we work on? How do we interpret the results?

如何解释未能找到答案的情况？诸如此类的事情。

How do we interpret failures to find answers? That kind of thing.

你认为AI数学系统能解决黎曼猜想吗？或者你认为天花板在哪里？

Do you think an AI an AI math system can solve Riemann? Or where is the ceiling do you think?

我认为它应该能够解决这个问题，或者证明它是不可判定的。那也会是个有趣的结果。是的。我觉得如果我们思考一下，像陶哲轩这样伟大的数学家能做什么，他们能够综合大量论文和前沿成果，并以其他顶尖人类数学家无法做到的方式从中学习，找到这些事物之间的联系，并利用它们创建更新更复杂的理论。我的意思是，这基本上就是系统工程的工作方式，而这正是计算机和AI模型擅长的——综合大量信息、发现模式、递归式自我改进。

I think that it should be able to solve it or or, you know, prove that it's undecidable. That would also be an interesting result. Yeah. I I think the if if we think about, like, what a great mathematician, like a Terry Tau, for instance, is capable of doing, you know, they're they're able to, like, synthesize lots of papers, lots of frontier results, and learn from them in a way that the other top human mathematicians can't and kind of find connections between these things and sort of use them to create new and more complex theories. I mean, that that's exactly kinda how the system where engineering works, and that's that's what computers are great at and AI models are great at, synthesizing large amounts of information, finding patterns, recursively self improving.

我记得现在在Metaculus上，有43%的概率下一个千禧年大奖难题将由AI或得到AI重要辅助的人类解决。我认为这个估计偏低了。我的意思是，我们可能很幸运，拉里·古斯可能已经在解决黎曼猜想的道路上了，那将非常了不起。但我认为，如果下一个问题是由人类解决的，那很可能必须是在不久的将来。而且可以肯定的是，再下一个问题很可能会主要由AI解决。

I think now on Metaculous, last I checked, there's a 43% chance that the next Millennium Prize will be solved by AI or, like, human with significant AI assist. And I I think I think that's an underestimate. I mean, we could be lucky and Larry Guth might be on the on the path to the Riemann hypothesis, which would be amazing. But I I think that, you know, if if the next one is solved by a human, it would probably have to be in the very near future. And for sure, the the next next one will will probably be significantly solved by AI.

你提到的一点我想深入探讨，就是递归自我改进这个概念。因为在AI领域，如果画一个从纯人类到纯AI的谱系，那么人机协同就是中间的谱系，从大量人类参与少量AI辅助，到大量AI参与少量人类辅助。Harmonic有趣的一点，至少据我理解，是因为有了Lean，你可以用代码封装数学。由于形式化验证，你可以客观判断对错，这意味着你有一个明确的奖励函数，可以通过自我对弈配合强化学习实现极快的迭代周期。这意味着你的模型进步速度可能非常快，因为在这种递归自我改进中没有人类参与循环。目标函数明确定义，可以通过自我对弈让模型变得越来越好，这是我们在许多AI领域看不到的。

One of the things that you said I want to hit on, which is this idea of recursive self improvement, because it seems like in the world of AI, there are if you were to draw a spectrum of human only to AI only, and then human in the loop is sort of the spectrum in the middle from lots of human, a little bit of AI to lots of AI, a little bit of human. One of the things that is interesting about Harmonic, at least the way I understand it is because of lean, you can encapsulate math in code. Because of formal verification, you can objectively determine whether things are right or wrong, which means that you have an objective reward function that you can use with self play to have very fast cycle times with reinforcement learning, which means that the progress of your model has a chance to be extremely fast because there are no humans in the loop with that recursive self improvement. Like objective function is clearly defined. You can do self play to just make the model better and better and better and better and better, which is not something that we see in a lot of domains of AI.

在大多数AI领域，改进的迭代周期要混乱得多。你能简单介绍一下这个系统吗？比如你的模型输入是什么？什么决定了它变好的速度？因为这看起来像是一个能够相当快速自我提升的系统。

Most domains of AI, it's a lot messier to get the cycle time on improvement. Can you just talk through the system a bit, a little bit of what I described, like what feeds into your model? What governs the rate at which it can get better? Because it seems like something that will be able to get better at a pretty quick rate.

好的，很乐意讨论这个。在深入之前我想先说明一点，我认为最有趣的是，递归自我改进在其他领域也能发挥作用。比如在AlphaGo这样的棋盘游戏中。是的。

Yeah. Happy to cover that. One point before going to that is just that I think the most interesting part about this is that, you know, there are other areas where recursive self improvement can work. For example, again, in those board games like AlphaGo. Yep.

但我觉得很多人没有意识到的是，在这些完全观察的零和游戏中，通过自我对弈确实能实现递归改进，但你会达到一个最优策略。是的。所以到那时，无论你有什么系统，都无法做得更好了。数学最令人兴奋的地方就在于没有上限。

But I think what people don't realize well, what a lot of people don't realize is that in these, let's say, you know, perfectly observed zero sum games, you improve recursively just by playing against yourself, but you hit an optimal strategy. Yes. So at that point, you know, it doesn't matter what system you have. It won't do better. The most exciting part about math is that there is no upper bound.

所以你们只是不断投入算力，它就会持续变强，没有尽头。当我们讨论AI是否能解决黎曼假设或获得千禧年大奖时，这些其实都是非常人类化的里程碑。我认为真正的问题是：它会有停止进步的一天吗？因为很明显它终将达到那些目标。

So you're just gonna keep putting compute in and it's gonna keep getting better and there's no end to it. And so when we talk about, do we think AI can solve a Riemann hypothesis or get a Millennium Prize? Like, those are very human milestones. And I think the real question is like, will it ever stop? I mean, because it clearly will get there.

我认为我们最终会解决比黎曼假设困难得多的问题——那些我们甚至尚未构想出的难题，因为书写如此复杂的问题几乎超出了人类的能力范畴。不过说到这个，你们

And I think we're gonna end up solving problems that are much, much harder than three one hypothesis, which we haven't even conceived of yet because it's almost like beyond us to write down such a hard problem. But coming Have you

有没有看过那个AI用二十秒通关《我的世界》的视频？

guys ever seen that Minecraft video of, like, the AI beating Minecraft in twenty seconds?

没看过。听起来太

No. No. That sounds I

我觉得这个类比很贴切。就像你了解《我的世界》的人类玩法，而AI用二十秒通关的方式完全超出理解范围。是的，你甚至无法完全理解视频里发生了什么。

think that's a good analogy. It's like, you know what Minecraft is, how a human would play it, and then the AI beating it in twenty seconds is just, like, incomprehensible. Yeah. Like, you can't even kinda grok what's going on in the video feed.

没错。但如果我们讨论谐波系统的工作原理，可以将其视为一群试图解决问题的智能体集合。确实，通过使用Lean定理证明器，我们能验证答案正确性，从而获得多种训练信号来改进系统。但需要明确的是，Lean仅用于验证——它本身不会告诉你是否接近答案或是否变得更聪明。

Yeah. But I I think if we just talk about, you know, how harmonic works, you can just think of it as there's a collection of agents that are essentially trying to solve problems. And it's true, because we use lean, we're able to check whether our answers are correct, and thereby derive a variety of training signals that we use to improve the system. But just to be clear, you know, the use of lean just lets you verify things. Lean doesn't itself tell you whether you're getting closer to the answer or whether you're getting smarter or not.

它只判断正确与否。因此要实现快速进步，仍存在大量待解决的科学挑战。

It's just telling you whether it's correct or not. So there's a lot of open scientific challenges to making it get better quickly.

你能简单说一下Lean是什么吗？以防有人不熟悉。

And can you just say word about what Lean is just in case people aren't familiar?

当然可以。Lean是另一种编程语言，由Leo DeMora创建的一款非常优秀的语言，可以说是最好的编程语言。未来我们可能都在用Lean编程，或者AI会直接用Lean编写代码。

Yeah. Totally. Lean is a just another programming language, a really great one created by Leo DeMora. The best programming language. We might all be writing Lean or the AIs might just be writing Lean in the future.

其核心思想是将数学陈述编码在语言的类型系统中。简单来说，Lean中的函数输入类型对应数学定理的前提条件，输出类型对应结论。如果你编写的函数程序能够编译通过，就意味着你可以从输入类型推导出输出类型，这相当于从前提条件推导出结论。这就是使用Lean进行数学证明的基本原理。

But the idea is that the mathematical statements are encoded in the type system of the language. So just very simply, you know, you have functions in Lean and the input types correspond to the assumptions of the mathematical theorem and the output type is the conclusion. And the point of lean is that if you write a program that implements that function and it compiles, that means you can derive the output type from the input type, which in turn implies that you can conclude the conclusion from the assumptions. So that's really the the fundament that's that's how you use lean for math.

我觉得Lean特别有趣的一点是，它的创造者Leo DeMora现在在亚马逊AWS工作，他并不是数学家。他开发这个工具原本是为了软件验证。他相信未来软件都需要经过验证，而现有的工具如Coq和Isabelle这些已有几十年历史的软件验证工具并不好用，说实话几乎无法使用，开发者的体验很差。所以他希望创建一个更好的软件验证工具，期待更好的工具能吸引更多人使用，从而产生更好的软件，这本身就是一个非常崇高的目标。但他当时没有意识到的是，软件验证本质上就是证明软件具有某些特性。

And I I think one thing that's super interesting about lean is if you look at Leo DeMora, the creator who's at Amazon AWS now, he's not a mathematician, and he wrote this as a software verification tool. So he he has, you know, the belief that, you know, in the future, software will be verified and the existing tools, things like Cock and Isabelle, which are kind of multi decade old software verification tools are just not good, you know, and and they're frankly unusable. The experience for developers is poor. And so he wanted to create a better software verification tool and in the hopes of if you build something better, more people will use it and will have better software, which is a super noble goal in in its own right. But then what he didn't realize was software verification, All it is is just proving that software has certain properties.

而这个工具在数学界变得非常流行。成千上万的数学家和数学学生共同构建了一个名为MathLib的有机库，你可以把它想象成最大的开源数学教科书。它在GitHub上，增长速度相当快。我觉得Lean在数学领域的使用程度在某种程度上已经超出了所有人的预期，可能现在已经超过了在验证软件方面的使用。

And this thing became very popular in the math community. And you had, like, thousands of mathematicians and math students building up an organic library called MathLib, which you can think of as kind of like the largest math textbook, open source. It's on GitHub, and it's just like growing at a at a pretty fast clip. And and, like, the usage of lean for math, I think, to some degree has surpassed anyone's expectations. It might be more than the usage for verified software at this point.

随着时间推移和AI的发展，这种情况可能会发生变化。

And that might change as time goes forward and and with AI.

我们经常问的一个问题是：为什么是现在？因为强化学习已经存在很长时间了，数学存在的时间更久。但数学似乎真的到了一个转折点。你们选择在这个时间点创办Harmonic。

One of the questions we always ask is why now? Because reinforcement learning has existed for a long time. Math has existed for even longer. And it seems like math has really hit an inflection point. You guys have chosen to start harmonic at this point in time.

为什么是现在？

Why now?

哦，我的意思是，现在有两个非常好的理由让我们感到兴奋。首先，你知道，一个是AI系统以一种有趣的方式变得更好了。实际上，我在2015和2016年就曾与一位密友讨论过强化学习在定理证明中的应用。当时的一个问题是，甚至没有一个很好的AI系统概念能够在无限动作空间中预测某些东西。比如在围棋中，你可以在某个位置落子，对吧，然后看到是黑子还是白子。

Oh, I mean, there there's two really good reasons why now that we're excited about. So first, you know, one one is just that the AI systems have gotten better in an interesting way. So I I was actually talking with with a friend, a close friend about, you know, RL for theorem proving back in 2015 and 2016. And one issue back then was that there wasn't even a great notion of an AI system that could predict something in an infinite action space. So in Go, you know, you can place a piece somewhere, right, and see either a black or white piece.

但在数学中，你真的可以做任何事情。比如，你可以生成任何下一步。所以当时我们没有很好的系统来做这件事。自回归语言模型现在已经变得相当不错了。这是使其成为可能的一个因素。

But in math, can really do anything. Like, you can just generate any, like, next step. And so we didn't have great systems to do that. So auto aggressive language models have gotten pretty good. That's one thing that makes it possible.

我在这里谈论的是大约十年的时间尺度，但这确实很重要。另一件有点疯狂的事情是，Lean已经变得非常强大了。如果你在二十年前告诉一位数学家，该领域的很大一部分人会为形式化方法和数学感到兴奋，他们可能会觉得你疯了，因为那时候形式化方法真的只局限于形式逻辑或某些类型的图论。如果你们听说过四色定理，那是形式化数学的一个重大成功。但改变的是，Lean如此灵活，如此令人兴奋，以至于人们贡献了这个叫做Mathlib的东西。

I'm talking on the timescale of like a decade here, but that's really important. And the other thing that's kind of crazy is that lean has gotten really good. So if you had told a mathematician twenty years ago that a large fraction of the field would be excited about formal methods and math, they might have thought you were crazy because back then formal methods were really isolated to formal logic or certain types of graph theory. Like if you guys have heard the four color theorem, that was one big success for formal math. But what's changed is that lean is so flexible, and so exciting for people that they've contributed this thing called math libs.

现在有了大量的知识体系，你可以在此基础上进行证明。所以，AI开始甚至可能适合这个问题，加上Lean运行得非常好，这两者的结合。而且Lean 4直到2023年9月才正式发布。所以这两件事同时发生，真的使其成为攻克这个问题的合适时机。

And now there's a lot of body of knowledge that you can build on to prove things. And so the combination of AI starting to like, even be a possible fit for this problem, plus lean working really well. And lean four was only released officially in September 2023. So those two things happening together really made it the right time to attack this.

你能谈谈数据，特别是合成数据，以及是什么在驱动你们正在构建的模型吗？

Can you say a word about data and specifically synthetic data and what it is that fuels the model that you guys are building?

是的。所以合成数据是模型的燃料。有一个惊人的资源叫做Mathlib。它是一个开源仓库。所以那里有很多人工编写的Lean代码。

Yeah. So synthetic data is the fuel for the model. There's a, there's an amazing resource called Mathlib. It's that open source repository. So that's a lot of human written lean.

而且它的编写方式非常通用和紧凑。所以它们实际上是在证明高级定理，对吧？这并不一定最适合解决问题。因此，几乎唯一能用于此的数据就是你自己生成的合成数据，因为原始数据不太适用。所以与AI的大多数领域相比，这有点像是数据贫乏的领域。

And it's written in a way that's very general and compact. So they're really proving advanced theorems, right? It's not necessarily the best fit for problem solving. And so as a result, almost the only data you can use for this is synthetic data generate yourself because that original data is not very applicable. So it's kind of a data poor regime compared to most areas of AI.

所以我描述的那个过程，即智能体本身试图解决问题从而生成训练信号，这是获取数据的主要方式。另一个问题是，你必须逐步提升智能水平。所以你并不是一开始就要证明黎曼猜想，而是先证明非常简单的东西，然后在整个过程中递归地自我增强。

And so that process that I described where the agents themselves are trying to solve problems and thereby generate training signals, that's the primary way in which you can get data. And the other issue is that, you know, you have to progress through levels of intelligence. So you're not necessarily proving the Riemann hypothesis upfront. You're proving really simple things, but then you kind of amplify yourself recursively throughout the process.

事实证明，互联网上的数学数据远不如猫咪视频多。

Turns out there's not as much math data on the internet as cat videos.

不幸的是，确实没有。很不幸，没有。

Unfortunately, no. Unfortunately, no.

嗯，是的，不过这很有趣，因为你知道，基础模型公司——那些通用基础模型公司——正面临数据墙的问题。目前他们已经耗尽了互联网上可用的数据。如果你能生成训练所需的大部分数据，那这就是以数学为核心相对于指望数学作为规模涌现属性的另一个优势。

Well, yeah, it's interesting though, because, you know, there's the data wall that the foundation model, you know, the general purpose foundation model companies are running into. And it's, at this point they've exhausted, you know, what's available on the internet. And if you can generate most of the data that's required to train, that's kind of another advantage of having math at the core versus hoping for math as an emergent property of scale.

是的。而且我认为数据墙以两种方式显现出来。一种就像你说的，我们已经用完了互联网数据。

Yeah. And I think the data wall kind of manifests itself in two ways. One is just, like you said, we're out of Internet data.

没错。

Yeah.

另一个是实际存在的互联网数据质量。你可以将其视为这些模型智能水平的上限，因为如果你用猫视频、所有优质的维基百科内容以及互联网内容进行训练，如何获得比这更智能的东西是一个开放性问题。因此，在我们看来，确实需要进入某种自我强化、自我对弈的机制，才能达到在多项任务上超越人类数学家和研究人员能力的水平。是的。

The other is the actual Internet data quality that's out there. You can think of that as providing kind of a ceiling to how smart these models can get because if you train on the cat videos and all the nice Wikipedia content and, you know, the the Internet content. It's an open problem how to get something that's significantly smarter than that. And so you do need to get into some kind of self reinforcing, self play regime, in our opinion, to get to a point where you can surpass the the ability of human mathematicians and researchers at multiple tasks. Yeah.

所以我认为在很多方面，这条路径不可避免地会采取AlphaGo到AlphaZero的方法，我们学习如何让这些模型创造绝大部分数据，并让数据复杂度随着模型持续迭代而增加。数学的伟大之处在于存在一条简单的实现路径——你可以通过解决数学问题所需的Lean代码行数来基本衡量问题的复杂度和难度，从而实际观察系统的复杂性。许多问题都是通过分解成更小的模块并逐个解决来实现的。

And so I think in many ways, like the the path, it's it's inevitable that it takes kind of the alpha go to alpha zero approach, and we learn how to make these models create the the vast majority of their data and have the the data actually increase in complexity as these models continue to to iterate. I think the the great thing about math is there's a simple path to doing this. You can you can basically measure the complexity of a math problem and and how difficult it is by how many lines of lean it takes to solve. So you can actually look at the complexity of a system. And a lot of a lot of, like, problems are solved by breaking it down into smaller chunks and actually solving those chunks.

如果你思考这个机制，更小的模块会更容易处理，因为解决它们所需的代码行数比大问题要少。所以如果你在这方面做得很好，并且擅长解决这些模块，就可以训练模型做得更好。随着你持续推动这个齿轮运转，模型会逐渐变得更擅长解决越来越困难复杂的问题。这在数学领域特别有效，因为它镜像了我们用纸笔解决数学问题的方式。是的。

And if if you kind of think about how that works, the smaller chunks are then more manageable because there are sort of, like, fewer lines to to solve than than the big one. So if you get really good at that, and then you get good at solving the chunks, then you can kind of like train your model to do better. And as as you kind of like keep turning the the gears on that, the model gets better at solving incrementally harder and harder and more complex problems. I think that works very well at math because it mirrors how we solve math, like, on on pen and paper. Yeah.

我们已经能够从简单公理开始，逐步构建起庞大的复杂结构。也许黎曼假设需要数百页才能证明，不会更多。费马大定理我记得有200页，非常非常复杂。所以，我确实认为最终会达到能够解决这些问题的水平。数学在某种程度上就像是原始的合成数据。

And we've been able to start with, like, simple axioms and build up, like, just giant complex structures. Maybe the Riemann hypothesis would be hundreds of pages, not more, to solve. Fermat's last theorem was, I think, 200 pages, very, very complex. So, yeah, I I do think eventually you'll get to a level where you'll you'll be able to solve these things. And the math is to some extent like the original synthetic data.

是的。是什么决定了你的模型改进的速度？

Yeah. What what determines the rate at which your model can get better?

改进的速度？我认为最高层面的因素是能源。投入的能源越多，就能并行进行更多尝试，这意味着数据生成速度更快。我的意思是，虽然没有速率限制步骤...抱歉，其实存在多个速率限制步骤，但并没有关于改进速度有多快的基本约束。

The rate at which you can get better? Well, I think the highest level one is energy. So the more energy you can put into it, the more attempts can happen in parallel, which means you generate data faster. So if I mean, there there's no rate limiting step. I mean, sorry, there's a bunch of rate limiting steps, but there's no, like, fundamental constraint on how far how fast it gets better.

所以这实际上只取决于你能投入多少计算资源

So it's really just about how much compute you

投入其中。我认为，这个领域仍然存在许多未解决的问题，对吧？比如，我们很大程度上受益于过去已证明的核心定理。想想数学竞赛的背景，有些定理是每个学生都会学习并使用的，比如AM-GM不等式这类东西。

put in. I think it's also I mean, there there's still a lot of unsolved problems in this field. Right? Like, we benefit a lot from core theorems that have been proved in the past. If you think about competition math context, there's theorems that every student would just learn and use, AMGM inequality, things of that nature.

因此在某种程度上，MathLib是不完整的。例如，几何方面的内容非常少，而且它非常理论和抽象。所以一个限制因素就是MathLib中有什么内容。当然，在某个时候，模型必须解决创建新理论和新结构的问题，扩展到其他领域，并且非常擅长形式化人类尚未形式化的东西。我认为这将是一个重大突破，而且肯定会在未来几年内发生。

And and so to some degree, like, MathLib is incomplete. There's very little content about geometry, for instance, and it it's, like, very theoretical and abstract. And and so a limiting step is, like, what's in MathLib. And, of course, at some point, the models have to solve the problem of, like, creating new theories and new structures and kind of, like, expanding to other domains and getting really, really good at formalizing things that haven't been formalized by humans. I think that'll be a big unlock, and that'll certainly happen within the next several several years.

你将能够说，嘿，就像这种情况。它可以简单到像一支棒球队，他们互相投球，你知道，系统将能够自动形式化这一点，并实时将其转化为Lean代码。我认为我们还没有达到那种可靠的程度。但当它变得可靠时，我认为那将是一个非常大的突破。

You'll be able to say, hey. Here's just like this situation. It could be as simple as, like, a baseball team, and they're, like, throwing balls back and forth to each other, and, you know, you systems would be able to kind of, like, auto formalize that and turn that into lean code on the fly. And I I don't think we're we're quite there yet to the point where that's reliable. But when it does get reliable, I think I think that'll be a really big unlock.

如果一切顺利，你认为Harmonic会变成什么？

If everything goes right, what do you what do you think Harmonic becomes?

嗯，我们的使命宣言是探索人类知识的前沿。所以对我们来说，我们产出的东西正确且对人类有用非常重要。因此，我认为在最好的情况下，我们能够构建一个工具，让许多数学家用来解决所有千禧年大奖难题，并远远超越这些。我认为那将是对人类的巨大贡献。该软件还有其他商业应用领域。

Well, our mission statement is to explore the frontiers of human knowledge. So it's very important to us that, you know, the things we produce are correct and useful to humans. So I think in the best case, you know, we're able to build a tool that a lot of mathematicians use to close all the Millennium Prize problems and to go far beyond that. I think that'd be a great, you know, service to humanity. There's also other areas of commercial application for the software.

所以，你知道，软件工程的梦想是能够直接验证代码的正确性。要做到这一点，你需要一个非常好的代码工作原理模型，能够理解库如何工作、它们承诺什么等等。因此，你可以想象一个未来，安全关键软件被证明是正确的，通用软件也被证明是正确的。软件工程的完成方式也可以改变。所以，如果你能创建一个非常擅长数学推理和验证其推理的系统，这将有很多应用。

So, you know, the dream for software engineering is to be able to just check that code is correct. To do that, you need to have a very good model of how code works, to be able to understand how the libraries work, what they promise, that kind of thing. And so you can imagine a future where safety critical software is proven correct, and general software is proven correct. And the way software engineering done is done can change as well. So this is like a lot of applications if you can make a system that's very good at math reasoning and very good at checking its reasoning.

是的，真的，我们认为有很多应用。

Yeah, really, we think there's a lot of applications.

是的。我认为，数学和软件是两个相当明显的领域。软件工程作为一个学科正在快速变化。我相信你们也看到了各种关于人们用Cursor和Claude 3.5做疯狂事情的报道。我认为未来的软件工程将不再那么关注代码成品的审查与协作，而会更侧重于对规格说明的协作。

Yeah. And I think the I mean, math and software are two fairly obvious ones. I think software engineering as a discipline is changing really quickly. I'm sure you guys are seeing all the reports of people doing crazy things with Cursor and, you know, Claude 3.5. I think in the future, software engineering will be less about, like, reviewing and collaborating on code as an artifact and will be more about collaborating on specs.

我们想要代码实现什么功能？我们能否在这方面更加严谨？我认为这就是验证将变得更加重要的地方。因为随着软件成本趋近于零，经过验证的软件成本也会趋近于零。突然之间，这件曾经非常不切实际且昂贵、需要专业人类来完成的事情，将会因为AI而急剧加速。

What do we want the code to do? Can we be more rigorous about that? And I think that's where verification will will become a a bigger thing. Because as the cost of software goes to zero, the cost of verified software will also go to zero. And suddenly, this thing that was like very impractical and expensive because you need specialist humans to do it will will just accelerate dramatically with AI.

所以我认为，展望五到十年后，如果我们沿着当前的能力曲线继续发展，绝大多数编写的软件都将经过验证且可证明正确。我认为这是一个非常令人兴奋的未来。在更理论化的方面，不仅仅是数学，物理学本质上也是数学。理论物理是数学前沿得以实现的主要途径之一。就我个人而言，如果能加速一些前沿的基础物理研究，真正理解宇宙为何如此存在、物理定律为何存在，并帮助设计实验来验证这些理论，那将会非常了不起。

So I think you look out five, ten years from now, the vast majority I mean, if we progress along the capability curve as we have been, the vast majority of software written will be verified and provably correct. And I think that's a really exciting future. I also think on the more theoretical side, it's not just math, but physics is essentially math. Theoretical physics is one of the main ways the frontier of math gets implemented. I think it would be amazing to me personally to accelerate some of the fundamental physics research at the frontier and really just develop an understanding for why the universe is the way it is, why the laws of physics exist, and also help figure out experiments to test those.

所以，如果我们能为这项努力做出贡献，我会感到非常自豪。

So I I I would be very proud if we contributed to that effort.

那么你认为你们主要会贡献于数学及数学相邻领域（如物理和软件工程）吗？还是说任何涉及推理的领域都在Harmonic的范围内？

And do you think you'll mostly be contributing to math and math adjacent areas like physics and software engineering? Or do you think anything that involves reasoning is in spec for Harmonic?

是的。我的意思是，我们尝试专注于某些领域，毕竟长期来看我们仍然是一家小公司。如果你相信数学就是推理——我们确实这么认为——那么，如果我们在数学和计算机科学（这是一个非常自然的类比领域）上变得非常非常厉害，那么是的，我认为任何领域都在这些模型的范围内。甚至历史论文也是如此。

Yeah. I mean, I think we try to be focused on the things that we're still a small company over the long term. I think if if you believe math is reasoning that and and we do, then, yeah, if if we get really, really good at math and computer science is a very natural analog, then, yeah, I mean, anything is in scope for for those models. Even the history essay, I think.

我们拭目以待。

We'll see.

蒂瑟其实不怎么碰历史论文。

Tither doesn't really touch history essays.

是啊。我真的很喜欢写历史论文，尽管我父母总说，你知道的，人文学科、语言艺术那些东西就别管了。但我觉得我的数学能力也让我写出了很棒的历史论文。所以希望亚里士多德也不会有什么不同。

Yeah. I I really enjoyed writing history essays even though my parents were like, you know, humanities, language arts, just ignore all that stuff. But, you know, I think my my math skills led me to write great history essays too. So hopefully, Aristotle will be no different.

总有一天会的。

One day.

亚里士多德写过一些很棒的历史评论。

Aristotle wrote some great historical commentary.

你真是个博学多才的人。

You are truly a polymath.

是啊。我是说，如果你读过《诗学》，就会发现...

Yeah. I mean, poetics is if you've read poetics, it's

我们要不要来个快速问答环节收尾？

Should we wrap it up with some rapid fire?

我们开始吧。闪电问答。

Let's do it. Lightning round.

好的。你会在哪一年赢得国际数学奥林匹克竞赛？

Okay. What in what year will you win the IMO?

导师，你觉得呢？很快。

What do you think, tutor? Soon.

好吧。2025年？

Alright. 2025?

很快。也许是2024年。

Soon. Maybe 2024.

好的。我们会为你报名2024年的比赛。那么，千禧年大奖呢？

Alright. We'll sign you up for 2024. Alright. How about the Millennium Prize?

哦，这个有点难。我猜是2029年吧。

Oh, that's a tough one. I would guess 2029.

2029年？

2029?

是的。好的。

Yeah. K.

我听说的是2028年。

I heard 2028.

是那样吗？他们说的是... 是的。我猜那会是一个完全由AI独立解决或AI与人类合作的千禧年大奖。

Is that is that what they're yeah. I guess it's a fully AI unassisted Millennium Prize or AI human hybrid.

那么，对于合作方式你怎么看？

Well, what do you how about what do you think for hybrid?

合作的话，我觉得2028年是有可能的。

Hybrid, I could see 2028.

我们说的是容易的千禧年大奖还是难的？

Are we talking an easy Millennium Prize or hard?

是像纳维·斯托克斯那样的吗？

Is it like Navey Stokes.

千禧年纳维

Millennium Navey

斯托克斯可能是2026年。黎曼假设，我给你20个。好吧，20个

Stokes might be 2026. Riemann hypothesis, I'll give you 20 Alright. 20

好的。就这样。很好。

Alright. There we go. Good.

考虑到我们今天甚至无法用大语言模型完成一个节奏性的小任务，这已经相当惊人了。你认为我们何时能拥有更广泛定义的人类或超人类水平的推理能力？

Given we can't even do a rhythmic tic today with LLMs, that's pretty amazing. When do you think we'll have human or superhuman level reasoning more broadly defined?

我认为在某种程度上，如果你将其定义为能够推理和解决数学问题，超越任何人类，比如能跟陶哲轩一较高下的水平。我想我们还需要几年时间，但我认为在接下来的一年内，模型可能会达到大约99.99百分位数的水平。

I think to some degree, if if you define it as something that can reason and solve math problems in excess of any human, like something that Terry Tau would, you know, would would give Terry Tau a run for for his money. I think we're a couple of years away, but I think the models within the next year will get to probably, like, ninety nine point nine ninth percentile.

陶哲轩会同意这个观点吗？

Would Terry agree with that?

我想是的。对。我不确定。你得问他本人，但我觉得他会同意这个观点。

I think so. Yeah. I don't know. You'd have to ask him, but I I think he would agree with that.

我们最喜欢的问题之一是：在AI领域你最钦佩谁？我们会稍作调整来问你们：在AI或数学领域，你们最钦佩谁？

One of our favorite questions is who in the world of AI do you admire most? And we'll modify it slightly for you guys. Who in the world of AI or math do you admire most?

我喜欢冯·诺依曼。我们刚才还在讨论他的传记。我觉得他真正吸引我的地方在于，他起初是数学家，但曾受到劝阻。我记得他父亲是匈牙利商人，试图劝他放弃数学，因为觉得这行不太赚钱。所以他请了一位杰出的数学家朋友去劝退他。

I like Von Neumann. We were just talking before about Von Neumann's biography. I think I think what I find really interesting about him was he started as a mathematician and he was discouraged. I think his father who was like a Hungarian businessman was trying to discourage him from doing math because it wasn't very, like, monetizable. And so he got his friend who was a a great mathematician to try to talk him out of it.

但那位朋友回来说：我做不到，这家伙太优秀了。如果他不发挥数学天赋，简直是对社会的损失。后来，他开创了计算机科学，冯·诺依曼架构成了所有现代计算机的蓝图。他还参与了曼哈顿计划，虽然有点争议，但非常务实且影响深远。

But the friend came back and he's like, I can't do it. This guy's too good. It would be just a disservice to society if he didn't use his talents for for math. And then, you know, he pioneered computer science, and the Von Neumann machine was like the blueprint for all modern computers. He contributed to the Manhattan Project, which, you know, is a little controversial, but very, very practical and impactful.

而且，他还创作了可能是博弈论的经典文献。所以，是的，我觉得这真的很了不起。另外，他也是东欧人。当然，有人争论匈牙利是否属于东欧。

And, you know, created probably the canonical text in game theory as well. So, yeah, I I think I think it's pretty amazing. Also, fellow Eastern European. Well, some people debate whether Hungary is in Eastern Europe.

是的。这是个有趣的问题。我觉得我几乎钦佩所有科学家和数学家。但如果你听说过数学家莱布尼茨，在创办这家公司过程中让我震惊的是：莱布尼茨曾与牛顿竞争创立微积分。虽然牛顿的表述流传更广，但莱布尼茨其实也独立达到了相同高度。

Yeah. It's it's an interesting question. I think, like, I definitely admire, like, almost all scientists and mathematicians. But I think that, like, you know, if you've heard of the mathematician Leibniz, what was kind of shocking to learn during the course of working on this company is that, you know, so Leibniz was competing with Newton to create calculus. And, you know, Newton's formulation went out, but Leibniz was basically there.

但人们不知道的是，莱布尼茨还有很多其他工作，其中一项具有惊人的预见性。要知道那可是17世纪末。他提出了称为'通用字符'的概念，本质上就是一种演绎语言，通过自动化程序用这种语言进行推理，并建立知识百科全书供推导使用。最让我惊叹的是，这位数百年前的思想家 essentially 预言了2024年正在发生的事。似乎只需要AI稍作进步，加上能运行类似Lean的计算机，这个愿景就能实现。

But one thing people don't know is that Leibniz also had a lot of other work and one piece of work that is just incredibly prescient. Keep in mind, this is the late sixteen hundreds. He created this thing called an idea called the universal characteristic, which is essentially the notion of having a deductive language, automated procedure to deduce things using that language and a body an encyclopedia of work in that language that you can build on to derive things. And so the amazing thing to me is that this thinker hundreds of years ago essentially predicted what will be happening in 2024. And it seems that the only thing that was required was having like AI get a little better and having like computers that can do something like lean.

对吧？我觉得这太不可思议了，一个人能在完全不知道未来会发生什么的情况下做出这样的预测，却能理解那是一个如此根本性的问题，以至于一百年后我们仍然会致力于此。太棒了。

Right? And I think it's just incredible to have a human being predict that with no concept whatsoever of what's gonna come later, but to understand that that's like such a fundamental thing that we're gonna end up working on that one hundred years later. Awesome.

谢谢大家。

Thank you, guys.

谢谢

Thanks

邀请我们。感谢邀请我们。

for having us. Thanks for having us.