Is human led mathematics over? Panel with Joelle Pineau, Timothy Gowers & Yann LeCun | Meta AI
发布时间 2022-11-03 13:41:10 来源
Hello everyone and welcome to this panel. It's a pleasure to be here with you today to talk about AI and mathematics.
大家好，欢迎来到这个专题讨论。今天能够和大家一起探讨AI和数学真是难以忘怀的荣幸。
I'll briefly introduce myself. I'm Joël Pinot. I'm a faculty member and the School of Computer Science at Miguel University. I'm also the managing director of meta-AI's fundamental AI research team. With me, I have two researchers who will join me in discussing this topic.
我来简要介绍一下自己。我是Joël Pinot，任教于Miguel大学计算机科学学院，同时也是meta-AI基础智能研究团队的总经理。此外，还有两名研究人员与我一同讨论这个话题。
Jan L'Accune is a French computer scientist, well known for his work in machine learning, deep learning. He's currently the vice president and chief AI scientist at meta, as well as the silver professor at the current Institute of Mathematical Sciences at New York University. Jan's the father of modern AI techniques in computer vision, in particularly known for convolutional neural networks. In 2018, he was awarded the Touring Award together with Yashua Benjou and Jeffrey Hinton for his work and their work I should say on deep learning. Welcome Jan. Pleus de bien.
简·拉库恩(Jan L'Accune)是一位著名的法国计算机科学家，主要研究机器学习和深度学习。他目前是Meta的副总裁和首席人工智能科学家，同时也是纽约大学现代数学科学研究所的银级教授。他是现代计算机视觉人工智能技术的创始人，尤其以卷积神经网络著名。2018年，他与杨劭和杰弗里·辛顿共同获得了图灵奖，以表彰他们在深度学习领域的工作。欢迎Jan。祝一切顺利。
With Diane, I have a Sir Timothy Gowers. Welcome to the panel Tim. You are a British mathematician as well as professor titular of the combinatorics chair at the College of France and the Director of Research at the University of Cambridge. You've contributed to important areas of combinatorics and functional analysis, including the theory of Bannach spaces, Ramsey theory, and as well making important contributions in analytics and combinatorial number theory. And in 1998, if I'm correct, you have received the field's medal for your work on combinatorics and functional analysis. So really distinguished panel today to discuss this topic of AI and mathematics. Really pleased to have both of you with us. Welcome. Thank you very much.
戴安娜：我邀请了蒂姆·高华斯爵士加入我们的小组讨论，欢迎蒂姆。您是一位英国数学家，在法国学院担任组合数学教授、在剑桥大学担任研究主任。您在组合数学和泛函分析等重要领域做出了贡献，包括班纳赫空间理论、拉姆齐理论以及在分析和组合数论方面做出了重要贡献。如果我没记错的话，1998年，您因在组合数学和泛函分析方面的工作荣获了菲尔兹奖。今天，我们非常荣幸能有如此杰出的专家加入我们，一起探讨人工智能和数学的主题。感谢你们的到来。
The panel is entitled whether human lead mathematics is over. That is quite a provocative topic. We'll start with a little bit of a warm up rather than dig right into that question. I take the statement to apply that going forward, AI should be leading mathematics rather than humans. But we may well have a little bit of ways to go before we get there.
这个讨论小组的主题是人类是否已经被淘汰，不能称为数学领袖了。这是非常挑衅性的话题。我们会从一个小小的热身话题开始，而不会直接回答这个问题。我理解这个声明的意思是，在未来，人工智能应该取代人类成为数学领袖。但是在那之前，我们还有很长的路要走。
And so let me start really just to get us grounded on this on this topic. In particular, I would love to hear from both of you. What does it mean to solve mathematics using AI? Jan, do you want to get us started?
所以让我开始吧，只是为了让我们在这个话题上有个基础。特别是，我很想听听你们俩的意见。用人工智能解决数学问题是什么意思？Jan，你想先谈谈吗？
I was going to say team should start because is the real mathematician here? I'm just kind of in person. I was going to say the Jan should start because he knows a lot more about AI than I do. But I mean, a simple answer to that would be just that we can create an AI that can, that is at least as good as a human mathematician or an expert human mathematician at solving mass problems.
我本来打算说该团队应该由谁开始，因为谁才是真正的数学家？我只是一个普通的人。我原本想说让Jan开始，因为他比我更了解人工智能。但是，简单的答案是我们可以创建一个人工智能，至少与人类数学家或专家一样擅长解决大量问题。
Of course, that raises additional issues like which problems should it solve and there are other things that mathematicians do other than solving problems like formulating problems, building theories, making definitions, making posing problems etc. But I would say that if a computer could become at least as good as a human mathematician or maybe if it could sort of pass a mathematician's Turing test and produce research output that we couldn't tell was not produced by a human mathematician, I would be very happy to count that as AI has sort of solved mathematics in some sense.
当然，这引发了其他问题，例如它应该解决哪些问题。数学家还会做其他事情，如制定问题、构建理论、定义、提出问题等。但我认为，如果计算机能够至少与人类数学家一样出色，或者如果它能够通过数学家的图灵测试并产生研究成果，我们无法分辨出这不是由人类数学家产生的，那么我很高兴将其视为在某种程度上解决了数学问题的人工智能。
You said something that I think was fascinating and we'll come back to it a little bit later, right? Whether you could look at the work of the AI and if it was indistinguishable from the human, then we may pass it Turing test of sort for AI and mathematics. But let me more emphasize the first part of what you shared which is sort of decomposing the ways in which mathematicians contribute, right? There's sort of the identification of the question which is one step of it. Then there's a formulae, we're really formulating the problem perhaps with a more formal language and putting in the assumptions that may give at least some boundaries to what you're trying to solve. Then there's a derivation of the proof and eventually all out if I can there's actually the verification of the work which is which is another step.
你说了一些我认为很棒的话，我们稍后会回到这个话题，对吧？你提到了如果能够看到AI的工作并且无法区分是否是人类的工作，那么我们就可以通过测试来评估AI和数学的能力了。但是，让我更加强调你分享的第一部分，也就是分解数学家的贡献方式。第一步是确定问题，然后我们用更加正式的语言得出公式，并加入一些假设来给问题设定一些边界。接着进行证明的推导，最后进行验证工作，这是另一步。
Jan, do you want to jump in and share some ideas in terms of these different levels, you know, where do you see AI being most effective right now? Right, I would actually put more levels into the process. There is certainly the, I mean, the thing that a lot of mathematicians do is forming sort of mental models of a particular problem or situation that they're interested in and sort of manipulating this mental model. And then there is perhaps coming up with appropriate concepts and definitions that are relevant for approaching the problem and that's an essential task, right? Constructing the right concepts to manipulate so definition forming which you know Tim mentioned.
简，你想不想加入讨论一下这些不同层次的想法，你知道，你现在认为人工智能在哪些方面最有效？是的，我实际上会将更多的层次加入到这个过程中。当然，许多数学家所做的事情是构建特定问题或情况的心理模型，并对其进行操作。然后可能会提出适当的概念和定义，这对于处理问题是至关重要的，对吧？构建正确的概念以进行操作，然后定义形成，正如Tim提到的那样。
Then there is intuition about, you know, potential theorems which are really properties of those mental models that may or may not be true, right? Her hypothesis then coming up with a sketch of a proof and then actually kind of writing down the proof and then, you know, doing it in a formal or semi-formal way, right? I mean, there are mathematicians who would be actually successful just coming up with sort of a somewhat informal sketch of a proof and then we're not other people who are much better at actually kind of feeling in the blanks right to the good example is the, you know, from as last theorem, right?
这里涉及到直觉，你知道可能定理，但实际上这些定理只是那些心理模型的特性，它们真实或不真实。她的假设是提出一个证明草稿，然后实际写下证明，最后以正式或半正式的方式进行。我的意思是，有些数学家可能只需要提出对证明的一些草稿，就能成功了，而有些人则更善于填补空白的部分，例如泼辣一役定理。
So I think, you know, currently, like, you know, the bottom layer, like, you know, formalizing, like doing the last step, I think it's things that where computers have already helped and can probably help some more. A lot of people are working on today, at least people who are interested in deep learning and stuff like that is kind of the step above coming up with sketch of a proof or strategies and kind of searching for proof. Perhaps also have some level of, you know, very kind of superficial intuition about what type of strategy for the proof will work. You know, not to predict whether a particular strategy is like it will work or something like that. And then, you know, of course, searching, you know, we know from results on games that, you know, searching through trees of, you know, multiple options is something that we can do really efficiently with computers, as long as we can direct that search.
我认为，目前，像正式化、最后一步这样的事情，计算机已经在帮忙了，而且可能还可以做得更好。至少对于那些对深度学习有兴趣的人来说，很多人正在致力于寻找证明的策略和勘误的阶段。或许还需要对什么类型的证明策略会有一些非常肤浅的直觉，但不能预测这个策略是否会奏效。当然，搜索也是必要的，我们从游戏结果得到的结论是，只要我们能够指引这个搜索，那么我们就可以使用计算机高效地搜索多种选择的树。
Higher levels coming up with definitions, forming mental models and things like that and and and like manipulating your the model in some sort of, you know, abstract, non formal, non formal way, I don't think we can do those computers today. And until we do this, I think we're not going to have computers that replace human mathematicians. But you will help that's for sure.
更高层次的数学工作包括定义、构建心理模型等等，还包括以一种抽象的、非正式的方式操作模型，我认为我们现在还无法使用计算机做到这些。在我们能够做到这些之前，我认为计算机无法替代人类数学家。但是你们（计算机）一定会帮助我们的。
Tim, do you have any follow up thoughts about which of these, you know, aspects of mathematics, AI is most able to help with at least currently.
蒂姆，你对于数学的哪些方面，人工智能目前最能发挥帮助的能力是否有进一步的想法？请尽量用通俗易懂的语言表达出来。
So if we're talking about AI and the sort of more deep learning sense as opposed to traditional AI, I say that because I'm actually working quite hard on a more traditional approach to automatic theorem proving. I think I hesitate to say to give a precise answer to that, I find it very hard to predict what AI's what the eventual capabilities are. I see a big spectrum from reaching a plateau rather soon and finding that we, you know, some pretty impressive things have happened now.
如果我们谈论AI，尤其是深度学习方面，而不是传统的AI，我这么说是因为我正在努力研究更传统的自动定理证明方法。我认为我很难给出精确的答案，因为我发现很难预测AI最终的能力。我看到一个大的范围，可能很快达到平台，发现我们已经取得了一些相当令人印象深刻的成果。
But maybe we'll find that in order to go further, we need to have a sort of training set that's 100 times bigger than what we've got now. And so therefore it's not feasible. Or maybe there will be some little tweaks to the system now and it'll become much more powerful in a short time. And I think.
也许我们会发现，为了走得更远，我们需要一个训练集，比我们现在拥有的大100倍。因此，这不可行。或者现在系统会有一些小调整，很快就会变得更加强大。我认为……
And let me let me allow you to open it up to other types of AI techniques, not just deep learning, right? I do, you know, you know, I mentioned searched and I do think some of the more classical AI techniques actually have a lot to to bring. Particularly in this context.
让我让我允许你开放到其他类型的人工智能技术，不仅仅是深度学习，对吧？我认为，你知道，我提到了搜索，我认为一些更经典的人工智能技术实际上有很多可以带来的东西。特别是在这种情况下。
Yes, so I think something that's very interesting is something that I plan to be spending quite a lot of time on over the next three years or so is thinking about a very abstract theoretical question, which is roughly speaking the following which that we know that if he doesn't equal NP as most people believe, then the general problem of finding a proof of an arbitrary statement of length that most N is an NP complete problem.
我觉得很有趣的一件事情，是我计划在未来三年左右的时间里，花很多时间思考一个非常抽象理论的问题。这个问题大概可以用以下方式来概括：如果我们相信 P 不等于 NP ，那么在长度为 N 的大多数任意语句的证明问题，就是一个 NP 难问题。
So it's not feasible. And sorry, we know it's an NP complete problem if P doesn't equal NP, then it's not feasible. But human mathematicians find extremely long and complicated proofs. The only explanation for that if you believe that P doesn't equal NP must be that we are looking within a very small portion of the sort of space of all possible proofs. We're looking at proofs have a very particular structure, very sort of modular and tied to the way humans think in various ways.
所以这是不可行的。很抱歉，如果P不等于NP，则这是一个NP完全问题，那么就不可行。但是，人类数学家会找到极其冗长和复杂的证明。如果你相信P不等于NP，唯一的解释就是我们只在所有可能证明的一个非常小的空间内寻找。我们只看到了结构非常特别、与人类思维方式密切相关的证明。
If we could understand that really well from a theoretical point of view, I feel that that would feed in to our understanding of what exactly the task is that AI is trying to accomplish. So that I think is and that I think applies both to traditional methods and to deep learning sorts of methods. I think this connects perhaps with some theoretical results in machine learning that's that they call the no free learns theorems that say that you can only learn with a non ridiculous number of training samples, a very, very small portion of the space of all possible functions.
如果我们能从理论角度充分理解这一点，我认为这会有助于我们理解AI试图完成的任务究竟是什么。因此，我认为这不仅适用于传统方法，也适用于深度学习等方法。我认为这可能与机器学习中的一些理论结果相关，它们称之为无免费学习定理，该定理表明你只能在非常非常小的功能可能性空间中学习，而需要非常非常多的训练样本。
So as you say, the type of proofs that humans can come up with is probably a very, very small subset. I mean, not probably is certainly a tiny subset of all possible proofs. And the question is what's what's special about those about those is there anything special about those first is it just because of our particular way that we are built and could we build.
正如你所说，人类能够想出的证明类型可能只是全部可能证明类型的非常非常小的一部分，这是肯定的。问题是，这些证明类型有什么特别之处？它们是否具有特殊性质，仅仅因为我们是这样构建的，那么我们是否能够构建出其他类型的证明呢？
AI systems that may have a different bias in terms of what they can do. Can I orient you to sort of ground the conversation for some of our listeners, you know, is there anything you have seen in recent systems that have been shared with, you know, with the community.
AI系统可能在它们可以做什么方面有不同的偏见。我能否帮助你为我们的听众提供一些基础知识，你知道，你是否看到了最近与社区分享的一些系统。
Anything that's impressive or that's worth noting or that you feel is actually a meaningful progress, you know, we've seen systems such as maneuver Everest a few others come out recently. Where do you think that we've seen genuine progress on this question of using AI for mathematics?
任何令人印象深刻、值得注意或者你觉得是真正有意义的进展，在使用AI解决数学问题方面，我们最近看到了一些像是“攀登珠峰”等系统的出现。你认为我们在这个问题上看到了真正的进展在哪里？
Well, I think I mean, there's been progress, you know, in in in recent years for various applications, particularly for games and that has translated and also in natural language processing. And the combination of those has translated into progress in sort of, you know, systems that are applied to mathematics.
嗯，我的意思是，在近年来，各种应用程序，特别是游戏，在技术上有了进步，这也转化为自然语言处理的进展。而这些技术的结合，也带来了在数学系统上的进展。
So in particular, is the idea that of course we can do three search right and we've, that's a classical AI technique we've been able to do three search for decades. More decades than team and I've been alive for.
因此，问题在于我们当然可以实现三搜索，这是一种经典的人工智能技术，我们已经能够进行三搜索几十年了。比我和我的团队活着的时间更长。
But but the problem has always been that, you know, you don't know what to prove like, you know, the branching factor is infinite essentially right there. So, the search space is gigantic and so how do you direct the search so that you arrive at a result that you have to size for example. And then there's a question of why do you have to size which is a different question.
但问题一直以来都是，你不知道要证明什么，就像你所知道的那样，分支因子本质上是无限的。因此，搜索空间非常庞大，如何指导搜索，使你能够得出例如大小的结果。然后还有一个问题，为什么你需要有一个大小，这是一个不同的问题。
So, I think the progress has been made, you know, following things like, you know, alpha zero and things like that is is research efficient research where the way the steps in the trees are taken is is basically a neural net making the choice. So what moves to make in the tree and then another neural net that evaluates the position if you want.
我认为已经取得了进展，比如AlphaZero等研究具有高效的研究方式，因为它利用神经网络来作出树形结构中的选择。一个神经网络用于选择树形结构中的移动，另一个神经网络则用于评估其位置。
Yes, the critics, we sometimes solve the critic that evaluates the, you know, where we are is it likely to lead to a proof of the ultimate results. And you know, in the past, you know, before kind of the last ten years or so. This was those those functions were kind of hardwired programmed and now we can learn that.
是的，有批评家，我们有时解决那些评估我们所处位置是否有可能导致最终结果证明的批评家。你知道，在过去，你知道，在最近的十年左右之前，这些函数通常是预先设计好的程序，现在我们可以通过学习来进行更改。
You know, you know, the statistics for example, yeah, right. And now we can learn that we can we can learn the the step using, you know, large language models that is trained on lots of proofs and we can also learn the the the critic. And so I think that's really sort of the conceptual progress that you know directed tree search in the space of possible proofs that I think is so that takes us to kind of the next level which gives a little bit of intuition about the sketch of proof.
你知道的，你知道的，比如说统计数据，是的。现在我们可以学习到利用大型语言模型，它们是在大量的证明上进行训练的，我们还可以学习到批评家。所以我认为这真的是在可能证明的领域中进行有向树搜索的概念性进展，这使我们进入了下一个级别，为证明的大纲提供了一些直觉。
I think in in mathematical systems, we're still missing all the top layers are always talking about earlier of like coming up with appropriate concepts and. We'll get to it with these questions.
我认为在数学系统中，我们仍然缺乏关于如何提出合适的概念等高层次的讨论。我们可以通过这些问题来探讨这些层次。
Yes. Tim has there been a particular result that you found inspiring. In terms of in terms of, you know, using AI techniques to improve our ability, particularly in terms of solving theorems.
是的，Tim，请问您是否发现过一些特别鼓舞人心的结果呢？特别是在利用人工智能技术提高我们解定理能力方面。
I have a slightly ambivalent attitude to all these things so. Not maybe in the way you expect so some mathematicians are ambivalent because they worry that at some point maybe probably put out of a job to sort of theme was which we started.
我对所有这些事情都持有稍微矛盾的态度。可能不是你所期望的那样，一些数学家的矛盾情绪是因为他们担心在某个时候可能会失业，因为我们开始讨论的主题。
That I'm not I'm relaxed about I'm old enough. It won't I was a very selfish attitude, but anyway, it won't affect me. So, but what I said when I see, for example, something like manoeuvre for the first time and it does quite a bit more than I was expecting it to be able to do.
我并不担心我已经足够年老了。尽管我的想法有些自私，但它不会对我产生影响。然而，当我第一次见到一些比我预想中更强大的操作时，我会说出我的看法。
Then part of me is impressed and part of me is a bit sort of nervous because I was been wanting to try and think about this thing from a more traditional perspective and. So, and worry. I start to worry that maybe I wasting my time with that, but on the other hand, I feel so the other reasons why ambivalence related to what you answered.
我有一部分心里感到印象深刻，但也有一部分感觉有点紧张，因为我一直想尝试并从传统的角度去思考这件事情。我开始担心，可能我的时间浪费在这上面了，但另一方面，我也感到困扰是因为你回答的原因。
Talking about having a critic that can be just learnt by a neural net. There's a part of me that really wants to understand what's going on when we find proofs and solve theorems and if we can just get a black box produced by a neural net that does the job, then I'm sort of worried that that.
谈到只能通过神经网络学习的评论。其实有一部分我很想理解，当我们发现证据和解决定理时发生了什么，如果我们只能获得一个由神经网络产生的黑匣子来完成这项工作，那么我有点担心这种情况。
Curiosity to understand really what it's doing how it works what what humans are doing when we come up with these ideas. But the sort of people will get less interested in that which I feel they should be interested in because they'll say well we don't need that anymore in order to create a program that can do it.
好奇心是想要真正理解事物的运作原理和人类在想出这些想法时所做的事情。然而，有些人会越来越不感兴趣于这些事情，因为他们会说我们不需要再去了解它们的运作原理才能创造出相应的程序。我认为他们应该对这些事情保持兴趣。
And I think that will be, I mean, maybe it'll be right that we won't need it, but I think it'll still be sad if we, if we, if we drop that theoretical problem. The thing is, you know, the functioning of your brain team when you're doing mathematics is a complete mystery to me.
我认为，也许我们不需要它会更好，但是如果我们放弃了这个理论问题，我觉得还是会感到悲伤的。问题是，当你做数学时，你的大脑团队如何运作对我来说是完完全全的谜。
So, you know, I, I take that point, but actually there's another, there's something else I've always felt that a large part of that mystery. I mean, I have that with other mathematicians, they look at their papers and I say where did that idea come from? It came out of absolutely nowhere.
你知道吗，我听懂了你的观点，但是我一直觉得数学中的许多奥秘其实还有另一种解释。我看其他数学家的论文，总会想，他们的想法从哪里来的？它们似乎就是从一个空白开始产生的。
But I know that I myself, my ideas don't come out of nowhere. So I have this very strong conviction that nobody's ideas come out of nowhere. There is always an explanation. It's just that there's a long tradition of how we write maths papers that obscures the discovery process.
但是我知道，我自己的想法并不是凭空出现的。因此，我坚信没有人的想法是凭空而来的，总有一种解释。只是有一个长久的传统，规定了我们如何写数学论文，这种传统掩盖了发现过程。
And it's something I've long wanted to do which is to bring that discovery process as much as possible out into the open. And I slightly worry that developments in deep learning, if they go fast enough, will just push it back in and say, well, we'll just replace a mysterious human mathematician who has a parent flashes of intuition that come from nowhere by a mysterious machine that does the same thing. And I will have lost the battle.
这是我长期以来想做的一件事，即尽可能公开发现过程。我有点担心，深度学习的发展如果足够快，将会把这个想法推回去，并说：我们可以用一个神秘的机器来取代一个神秘的人类数学家，后者会突发灵感。我会输掉这场战斗。
It's very interesting because there was exactly the same kind of reaction initially during the emergence of deep learning for computer vision. A lot of people who have spent their career trying to sort of discover the mechanisms of image formation and things like that. So deep learning as well now we just have a black box. We it's not going to teach us anything about how vision works. But it didn't change anything in the end. I mean, the people are using what works.
这是非常有趣的，因为在深度学习用于计算机视觉中的出现时，起初也有完全相同的反应。很多人花费了整个职业生涯试图去发现图像形成的机制等等。因此，现在深度学习也只是一个黑盒子，对于视觉工作的机制没有教给我们任何信息。但最终这并没有改变任何事情。我的意思是，人们正在使用有效的东西。
I want to go back to an idea you suggested Tim earlier and I think is very relevant in this case, right? Which is this question of before we, before we, you know, adopt the black box and sort of move to higher levels of abstraction. You know, do we have a sense of what's going on inside of the box, whether it's a human or a computer? Is the process of solving these problems, at least for the simple mathematical problems that we've been able to solve with AI? Does the process look the same?
我想再讲一下你之前提出的、我认为在这种情况下非常相关的想法，对吧？也就是我们在采用黑盒并转向更高层次的抽象之前，是否能知道盒子内部的情况，无论是人类还是计算机？对于我们已经能够用人工智能解决的简单数学问题，其解决过程是否相同？
So when we, you know, when we combine a one of these search algorithms with an evaluation function that may be able to, you know, from training learn how to evaluate different different search options. Do we find that in the end it comes up with a proof that is analogous to the path that the humans would have followed or is it different in qualitative ways? I think it's very important here to distinguish between the proof and the proof discovery process.
所以当我们将其中一个搜索算法与评估函数结合起来，这个评估函数能够通过训练学习如何评估不同的搜索选项。我们是否会发现最终的证明与人类所遵循的路径类似，或者在质量上有所不同呢？我认为在这里非常重要的是区分证明和证明发现过程。
And my impression is that the proof itself can certainly with some of these different, these things can look very similar to what a human would write down. Some of the proofs have been produced in natural language. Not all. So there was the, I think it was open AI solution of some international mass or the impiad problems where the proof just was we will feed this expression into lean and then lean just says completed. And there's a sort of guarantee that the thing is proved and no proof is necessary written down at all, though you can actually construct a proof out of that and that but that somehow looks very unhuman.
我的印象是证明本身确实可以与这些不同的东西相匹配，这些东西看起来很类似于人类所写的。其中一些证明是用自然语言撰写的，但不是全部。例如，有一个名为“Open AI”的国际数学竞赛中，该算法的解决方案将该表达式输入到“Lean”中，然后“Lean”就会显示“已完成”，并且有一种保证证明的方式，不需要写下任何证明，但实际上可以从那个证明中构造出一个证明，但那看起来非常不像人类。
But when it comes to the actual search process, I think there's an awful lot of searching that's going on behind the scenes and not displayed for the for the consumption afterwards that a human mathematician would not be doing. So very efficient, very efficient in its solving compared to human. Yes, it's all the output.
但是当涉及到实际的搜索过程时，我认为很多搜索是在幕后进行的，而人类数学家不会进行这样的搜索。因此，它与人类相比在解决问题时非常高效。是的，这是所有输出结果。
So when I talk about the cheering test before actually, I don't totally believe in that because I do actually think that the process that goes on is as important as well as the output is not just the output that matters to me, I think. But partly because I think if you have inefficient things that's going to be much harder to scale up when you have more complicated problems with that.
所以，当我在之前谈论欢呼测试时，我并不完全相信它，因为我实际上认为进行的过程就像产出一样重要，而且不只是产出对我很重要，我认为这一部分也很重要。但部分原因是我认为如果你有低效的事情，当你面对更复杂的问题时，它将更难扩展。
What are your thoughts, Jan, between the at least the relatively simple problems that we can solve with AI. Do you think both in terms of the search process and the final result? And let me add one more color to that question. It is even if the solution looks similar at the end, are there are there ways in which it's expressed that let me rephrase this.
简，你对我们可以用人工智能相对简单地解决的问题有什么想法？你认为这既涉及到搜索过程，也涉及到最终结果？让我再提出一个问题，即使解决方案在最后看起来很相似，是否还存在表达方式上的差异？让我来换个方式来表述。
In many ways, the reason it might look similar at the end is because we're training from other examples of proofs that humans have generated. And so do you think that's part of the reason that the proof looks so similar or you think there's something beyond that that's at the true property of the problem? I mean, certainly, I think there is a very strong bias towards reproducing the type of proofs that humans have come up with.
在很多方面，证明看起来相似的原因是因为我们是从人类所生成的其他证明示例进行训练的。你认为这是证明相似的部分原因，还是你认为有其他真正问题性质的东西存在？我想，确实有一种非常强烈的偏向于复制人类想出来的那种证明类型。
And there may be another set, you know, perhaps a very large set of other types of proofs that nobody is there to try because perhaps they require too much kind of working memory. For example, the humans are not particularly good at doing a good example of this is the graph coloring theorem, which is one of the first ones that required the help of a computer to kind of explore all the cases and figure out what the story was. It's something that's very difficult to do by hand.
你知道的，可能还有另一组非常庞大的其他类型的证明，没人去尝试，可能因为需要太多的工作记忆。例如，人类不擅长做一件事，即图着色定理，这是第一批需要计算机帮助探索所有情况并找出答案的定理之一，手动操作非常困难。
And I think there are probably a lot of very interesting results that are of that nature that require. You know, ridiculously large commutational exploration that you can do by hand, but but computers would have no no issue doing. Perhaps things that require so this is perhaps connected to something you, Joel, you and I are familiar with, but we are very often misled, for example, when we do, we try to do some reasoning, I'll get some intuition about high dimensional geometry. And you know, vectors in high dimension, for example, that we reason with, you know, three dimensional space and that's completely wrong.
我认为可能有很多非常有趣的结果需要进行非常大的计算探索，这是我们手动无法完成的，但计算机可以做到。也许涉及到需要一些高维几何感或直觉的事情，我们通常被误导，试图在高维空间中进行推理，例如高维向量，但我们用三维空间进行推理是完全错误的。可能与你，Joel，和我熟悉的一些事情有关。
Ready gives us kind of wrong intuitions. Would it be possible for a machine to get a better intuition than humans in sort of higher dimensional spaces? And you know, I think there are sort of probably important results there that we're kind of we're missing. But at the lower level, more short term, I mean, there's clearly in situations like, like go and chess,
准备让我们产生了某种错误的直觉。机器是否可能在某种高维空间中比人类具有更好的直觉力？我认为可能会有重要的结果被我们错过了。但在较低层面、更短期的情况下，比如围棋和国际象棋等情况，显然有...
right? Computers can come up with solutions that people had never thought about, right? For particular situations. And I imagine the same thing will happen with not automated proof, but sort of computer assisted mathematics.
计算机可以想出人们从未想到的解决方案，对于某些特定情况而言。我认为，在非自动化证明方面，但是在某种程度上辅助计算机进行数学运算时，同样的情况也会发生。
Yeah, I want to take time to go sort of at the higher level of abstraction, which is in the discovery process, in, you know, picking what are the right problems to solve at the right time and point given our body of knowledge. And let me link this to where we are on the AI side. You know, we've seen some tremendous progress in creativity recently.
是啊，我想花点时间在更高层次的抽象上，主要是在发现过程中，选择在我们所掌握的知识范围内，在正确的时间和地点解决正确的问题。让我把这与我们在人工智能方面的进展联系起来。你知道，我们最近在创造力方面取得了一些惊人的进展。
For many many years, people thought the domain of creativity, whether it's artistic expression through, you know, painting or music or other mediums, was really the domain of humans. And that really we wouldn't see much creativity coming out of AI. Recently, we've seen a bit of an explosion of work that shows, for example, that we can create completely new images, recently new video, new music, poetry, using AI. Looking at that and now transposing that to the spheres of mathematics, where I believe the, you know, the, the formulating the problem, choosing the question is the more creative aspect of the work.
许多年来，人们认为创意的领域，无论是通过绘画、音乐或其他媒介的艺术表现，都是人类的领域。他们认为我们不会看到来自人工智能的大量创造力。然而，最近我们看到了一些作品的大量增长，例如我们可以使用人工智能创造全新的图像、最近的视频、新的音乐和诗歌等。现在，我们把这些转移到了数学的领域，我相信，提出问题和选择问题是工作中更有创造力的方面。
What do you see as the potential for bringing in an eye at that level? Huge potential, but it's not going to happen anytime very soon. It's going to take years because what are the main and sole problems in my opinion in AI is, is getting machines to form mental models of the world, of the environment, of the data they are fed with. So that if they have some idea of how this environment, this world will change as they take an action.
你认为在这个层面引入视觉技术有什么潜力？
巨大的潜力，但很快不会发生。这需要很多年的时间，因为在我看来，人工智能的主要和唯一问题是让机器形成世界、环境和输入数据的心理模型。因此，如果它们能够对它们采取行动会如何改变这个环境、这个世界有一些想法。
And then the context of mathematics, you know, the, the, the formulas or the, the sort of things that you know are true, changes for, for every kind of transformation of that that you're doing any step in the proof that you're doing. So if you can have a model, sort of abstract metal model of what this process is, then you can plan a sequence of actions to arrive at a goal.
然后在数学的语境中，你知道，公式或其他你知道是真实的东西，针对每一种你所做的证明中的转化都会有所不同。因此，如果你能有一个抽象的金属模型来描述这个过程，那么你就可以规划一系列行动来达到目标。
And we do this as humans all the time. Most animals can do this as well decompose a complex task into sequences of kind of lower level, more immediate, kind of sequences of actions. We don't know how to do this with AI systems yet until we know how to do this. I don't think we'll have kind of full-fledged AI mathematicians.
我们作为人类经常这样做。大多数动物也能够将一个复杂的任务拆分成一系列更低层次、更直接的行动序列。然而，我们目前还不知道如何将这种能力应用于人工智能系统，因此我认为我们不可能拥有真正意义上的人工智能数学家。
And, and you know, what are the right techniques for this? We don't know yet. Let me just add a dimension and I'll let you jump in to them. I think Jan, you talk about, you know, sort of tip, you know, having a mental model of it and then then decomposing it being a really important part of the discovery process.
嗯，你知道吗，这需要什么正确的技巧吗？我们还不清楚。让我加一点内容，然后你就可以讨论它们了。我认为，Jan你提到，拥有一个心理模型，然后将其分解是发现过程中非常重要的一部分。
So maybe a little bit further and say a lot of the results we've seen on creativity are based on generative models, right? Essentially, feeding in enough data that the model can then generate new information that comes out of the distribution, but then sampling really quite widely across that distribution. So with this require building a generative model of mathematics to be able to truly inform that discovery process.
也许我们可以进一步说，我们在创造力领域看到的很多结果都是基于生成模型的，对吗？本质上，输入足够的数据，使模型能够生成从分布中出现的新信息，但在这个分布上广泛采样。因此，这就需要建立一个数学生成模型，以真正启发发现过程。
Let me leave it there and then bring you into that into that discussion. I was just going to respond to something that Jan didn't say explicitly, but I want, so I think there's a question that we don't know the answer to, although I have, I have my own view about what I think the answer is, but I can't justify it fully. And that's the question of whether which comes first, do first have a kind of AGI capacities that have the kind of creativity that you need and then you feed that into mathematics in order to find these intermediate steps in complicated proofs and that sort of thing.
让我把它放在那里，然后引导你进入讨论。我只是想回应一些简没有明确表达的东西，但我认为有一个问题我们不知道答案，尽管我自己对答案有自己的看法，但我无法完全证明它。那个问题是，哪个先出现，首先有一种AGI能力，具有所需的创造力，然后再将其输入到数学中以找到复杂证明的中间步骤等。
Or is the problem that the specific mathematical problem of creativity where you are looking for intermediate steps. An easier version of the more general problem of creativity that would need to be solved for AGI. So I personally think that the maths, the problem of finding proofs is not, is it's, my hunch is that it's strictly easier than full AGI is a step to on, on the way to AGI rather than something that has to wait for AGI.
问题是你正在寻找中间步骤的创造性数学问题，这可能是通向人工通用智能（AGI）必须解决的更一般的创造性问题的简化版本。因此，我个人认为，找到证明的问题不是一个必须等到AGI之后才能解决的难题，而是AGI的一步，也是通向AGI的一步。
And I think that for example, what we, what we think of as the very creative moments in proofs that some people come up with, it's not creativity in the sense of, you know, an artist having a dream and getting up and in a frenzy of creating some picture or something. Of course, there are lots of stories that suggest that it is like that, but actually, quite a lot of what passes for creativity and mathematics is sort of concatenation of fairly standard sort of steps like let's take this statement and abstract it as much as we can before it becomes false. And that's just one of many different techniques that we use, you know, a lot of what we do is asking questions. So we have a question that we're trying to answer, we can't answer it.
我认为，例如数学证明中某些人创造性时刻是并非艺术家做梦并狂热地创造一些画作之类的创造性。当然有许多故事表明它是这样的，但实际上，数学中的许多创造性都是标准步骤的串联，例如把一个陈述尽可能抽象化以避免出错。这只是我们使用的许多不同技术之一，我们很多工作是在提问，当我们有一个问题需要回答时，我们无法回答。
So we ask another question that's related and so on. And those questions don't come out of nowhere. And I think that's a, my view is that a small class of question transforming moves that we have at our disposal. And we just keep on using those and then eventually we find something that, that is both non trivial and something that we can answer and then we know we are making some progress. So I'm optimistic that that will be something that AI will be able to do. Not saying it's an easy thing, but I think it's not fundamentally mysterious.
我们会问一个相关的问题，然后再问下一个。这些问题不是无中生有的。我的看法是，在我们手头有一小类问题转化的方法，我们只需一直使用这些方法，最终我们会发现一些有意义且可以回答的问题，这样我们就知道我们在取得一些进展。因此，我对AI能够做到这一点持乐观态度。我并不是说这是一件容易的事情，但我认为这并不是一个基本上神秘的事情。
I wonder if, and you know, Yana, Yana, you're a little bit of a musician at your hours as a, as am I, you know, when I hear you speak to, oh, also wonderful. We can have a whole other panel on the link between music and mathematics. But I think the interesting point you bring to me is the process by which creativity, you know, is expressed in mathematics, maybe less of sort of a strike of genius than, you know, having a rich set of tools on which to build. And in many ways, I would argue that human creativity may have the same kind of scaffolding and may also not come out of sort of, you know, sort of genuine inspiration.
我想知道，你知道的，雅娜，雅娜，你在音乐方面有些小天份，像我一样，在你说话时听到你的声音真是太好了。我们可以就音乐和数学之间的联系开一个完整的小组讨论。但我认为你给我的有趣观点是，创造性在数学中的表达可能不是一时的天才灵感，而是有一套丰富的工具来构建。在许多方面，我认为人类创造力可能也有相同的支架，也可能并非真正的灵感所产生。
And it really rise out of that of that expertise. Yana, I don't know if you, if that resonates with you. And also if you wanted to comment on the, you know, do we achieve AGI first and then solve mathematics or do we? Well, I think on the, on the point of creativity, I think, you know, people who are original creators basically very often invent a new scaffolding of the type that you were talking about, right? A new set of tools and the use those tools to invent new things or produce new things in music and visual arts or probably in mathematics as well. I mean, also in natural science, right? A lot of science advances in science are due to progress in tools, you know, astronomy, telescopes and my co-scoops, my co-scoops and, you know, molecular biology and biology.
它确实源自于那样的专业知识。雅娜，我不知道你是否有同感。另外，如果你想评论一下，我们是先实现AGI然后解决数学问题，还是...嗯，我认为在创意方面，原创者往往发明一种新的脚手架类型，就像你所谈到的那样，一个新的工具集，并使用这些工具来发明新东西或在音乐和视觉艺术或数学中生产新事物。我意思是，在自然科学中也是这样的，对吧？许多科学进步都是由于工具的进步而推动的，比如天文学、望远镜和显微镜、分子生物学和生物学等。
So things like that, where the tools kind of create the progress. Now, on the question you were asking before, you know, there's been a lot of progress in, sort of, you know, computer creativity using generative models for mathematics. I think the last piece, which is the generation, is the easy part to some extent. So this is what, you know, people have either solved or are working on sort of turning some sort of abstract representation of a schedule of proof into something formal, right? That's something that is some level of achievements there, right? And, you know, the problem is, is at the high level, I sort of keep coming back to this to this question.
像这样的情况，工具可以创造进步。现在，在你之前问的问题上，使用生成模型进行数学计算的计算机创造性已经取得了很多进展。我认为最后一个部分——生成——在某种程度上是比较容易的。因此，人们已经解决或正在努力将一些抽象的定理证明排程转化为形式化的东西。在这个领域已经有一定的成就了。然而，问题在于高层次上，我总是回到这个问题。
Now, what's he trying to think about those recent image generation and video generation systems, for example, is that they actually produce images or videos at a very low resolution. They're kind of sort of, you know, for the abstract things. And then there is a different process that actually kind of samples that produces nice looking pictures. And so, you know, this is two levels. I think we need more than two levels, but, but we can do the lower level easier in a easier way than the simpler way than the top levels. Yeah, that is, that is just an interesting aspect of how human mathematicians work.
现在，他在思考最近的图像生成和视频生成系统，例如，它们实际上以非常低的分辨率产生图像或视频。它们更适合用于抽象的事物。然后有一个不同的过程，实际上对这种低分辨率的采样进行了处理，产生了漂亮的图片。所以，你知道，这是两个层次。我认为我们需要更多的层次, 但是，我们可以以比顶层更简单的方式来进行更低层次的处理。是的，这只是人类数学家工作的有趣方面。
We often sort of, if we're reasonably experienced in some area, we may sort of see that we can prove something long before, even though we know that it would take 10 pages and lots of boring calculations actually to write out the full proof. There's something that when you, when you haven't reached that level of experience, seems very sort of intimidating, but after a while you, you get used to it because you're sort of, you learn to think in bigger and bigger steps with, because you've had experience with certain types of problems.
如果我们在某个领域有一定的经验，通常会发现我们可以先证明某些东西，即使我们知道这需要写出长达10页、大量枯燥的计算才能完整地证明它。在你没有达到那种经验水平时，这似乎是非常吓人的，但是随着时间的推移，你会习惯这种感觉，因为你已经通过一些类型的问题积累了经验，你开始学会以更大的步骤思考。
And so, you know that the technicalities will work out and so. And so, quite what's going on in our brain when we think in these big steps, I think it's quite, it's quite difficult to fathom. That is something that with experience, you know, I think that that level of abstraction, it really, really increases.
因此，你知道技术细节会解决一切。当我们进行大的认知跨越时，我们的大脑到底在思考什么，我认为这是非常难以理解的。随着经验的增加，我认为这种抽象层次会大大提高。
That brings me to question we haven't touched on, but I think maybe interesting, which is what do you think is a role of AI towards the learning of mathematics? Do you see a role either sort of to train, you know, the maybe high school or Lisi level students or the more advanced students, the graduate level students, those who are making sort of their first steps into into research? Do you see that AI could play a role, for example, to bring in that scaffolding that permits faster access to higher levels of abstraction?
这就引出了一个我们没有涉及但我认为很有意思的问题，那就是你认为AI在数学学习中扮演的角色是什么？你是否认为AI可以在培训高中或理科水平的学生以及更高级别的研究生，那些正在开始研究的人中扮演一个角色呢？例如，你是否认为AI可以发挥作用，提供支持结构，以便更快地访问更高层次的抽象？
I think the potential in that direction is absolutely limitless. I mean, once you've got the AI that can find proofs, and again, it slightly depends. I think the more black boxy it is, the harder it's going to be to, because if it just sort of says, here's the proof, admiring yourself. It's between a good teacher and sort of a sort of a crutch.
我认为这个方向的潜力绝对是无限的。我的意思是，一旦你拥有了可以找到证明的 AI，这取决于一定程度。我认为它的黑盒子越多，它就越难，因为如果AI只是说，这是证明，那么你就会停下来自吹自擂。这就是好老师和拐杖之间的区别。
But people have been, I know already people have been working on using language models to produce not just proofs, but proofs together with accounts of the thought process. And tell me the steps you used, that sort of thing. So I think that will come as well. I mean, I think once that technology is there, I think we've definitely got the potential to turn that into remarkable educational tools and tools that can respond to mistakes that people make and ask them questions that will help them to clear up their misunderstandings and that sort of thing.
但我知道人们已经在使用语言模型来不仅产生证明，而且还包括思考过程的描述方面进行研究。比如告诉我你所用的步骤等。所以我觉得这也会实现。我的意思是，一旦这项技术出现，我们肯定有可能将其转化为出色的教育工具和工具，能够响应人们所犯下的错误，并提出一些问题以帮助他们澄清误解，等等。
I hope that we'll reach a stage where we can have a sort of golden age of mathematical teaching and I won't be sure to do a math teacher anymore because computers can do the job. Yeah. Yeah, I think that from that.
我希望我们能够达到一个数学教学的黄金时代，到那时，我可能不再需要成为一名数学教师，因为计算机可以胜任这份工作。是的，我认为这一天将会到来。
I think the arrival of computer mathematicians, perhaps will change the activity of mathematics, not just for professional mathematicians, but also for students. The same way the, you know, the pocket calculator has changed what students can do. And it used to be that you could be a mathematician and spend your career computing logarithm tables. And, you know, not anymore, right, because we have computers to do this now.
我认为计算机数学家的到来可能会改变数学活动，不仅仅是对专业数学家，还包括学生。就像口袋计算器改变了学生的所能做的一样。过去，你可以成为一名数学家并且一生计算对数表，但现在已不再需要了，因为我们有了计算机来完成这个工作。
And, and similarly, you know, we used to ice match a lot of time in school, you know, learning how to, you know, get logarithms from a table and then sort of interpret the thing between, you know, this was an exam in eighth grade or something like that. So those things have disappeared because we have pocket calculators. And so I imagine that the, the sort of role level steps of mathematical proofs will also disappear and that people will be able to concentrate on what's going to more interesting, perhaps, which is sort of the more conceptual aspects of mathematics, not the mechanics of, you know, here is how you solve linear equation, aquatic equation, but, but what does it mean really like what's the tuition behind it's right.
同样地，我们在学校经常做匹配冰，学习如何从表格中获取对数，然后解释它们之间的关系，这是八年级的一次考试。但是由于我们现在有口袋计算器，这些东西已经消失了。因此，我想数学证明的级别步骤也将消失，人们将能够集中精力于更有趣的东西，也许是数学的更概念性方面，而不是像解线性方程、求根公式这样的机械化操作，而是求解这些公式背后的含义。
For example, the tuition behind, you know, aquatic equations and, and, you know, curves that intersect the x axis, you know, is, is, is, is something that, you know, you might, you might still want to build, even if, you know, you don't need to learn by heart, the former, I mean, it's useful, perhaps to show how you derive it, but, but then you can always look it up. So, so I, you know, I think it's going to change the activity of what students learn eventually and it's going to also change the type of activities that mathematicians work on, but I agree with Tim, the potential is, you know, somewhat somewhat limitless, whether we'll be able to explore it.
举个例子，比如说，你要学习水文方程、与x轴相交的曲线等课程内容，尽管你可能不需要死记硬背这些，但学习这些对你也是有用处的。它可能有助于展示这些知识是如何得出的，但如果你忘了，也可以随时查阅。因此，我认为它将最终改变学生所学习的内容，并改变数学家所从事工作的类型，但我同意Tim的看法，它的潜力是无限的，我们需要不懈地探索。
And I will add, you know, I think all three of us have done a fair bit of teaching that the part that short term is especially appealing is the ability to do the marking and the correction automatically so that the verification of the work, you know, it's one thing to teach, but it's another thing to a hundred times over verify proof that students have done with various degrees of success. So, the more tracing thing would be personalized tutoring, right?
我想说的是，我觉得我们三个人都做了不少的教学，其中短期教学特别吸引人的地方就是能够自动完成标记和纠错，这样验证学生的作品就变得简单了。教授一门课很容易，但要验证学生的不同程度的作品一百遍就不是那么容易了。所以，更有针对性的辅导应该是更好的选择，对吧？
Yes, and we can certainly count on that. I hope pretty soon. We're really near the end of our time together and I want to broaden this up, you know, if we, we project, if we have a similar conversation in five years or even in 50 years, you know, pick a time horizon that, that, that inspires you. What do you think will be different? Where do you think will be really both in terms of acknowledging the success and what will be the remaining open problems would love to hear each of you on that.
是的，我们肯定可以指望这一点。我希望很快。我们的时间已经接近尾声，我希望打开一些更广泛的话题，如果我们在五年，甚至五十年后进行类似的对话，你知道的，选择一个时间范围，激励你的未来想象。你认为会有什么不同？在我们承认成功的同时，你认为还有什么未解决的问题，非常想听听你们每个人的看法。
Well, so the question is when will there be a new theorem that no human thought about that would be proved by a computer or by, you know, one of those automated proof systems and not clear. It may happen faster than we think or it may take it may be much more difficult than we think. And then there is the question that that team that you are asking joy, that. For which team had an answer, you know, we do we need to have sort of human level level intelligence systems before we get computer mathematicians and the answer is yes and no. Because we can still we can do a lot of useful things with computers without them having human level intelligence or super human intelligence.
那么，问题是，什么时候会有一个新的定理被计算机或自动证明系统证明，而没有任何人曾考虑过它，这不是很清楚。这可能比我们想象的要快，也可能比我们想象的困难得多。然后还有一个问题，那就是你问乔伊的那个团队。该团队有一个答案，就是我们是否需要拥有人类级别的智能系统才能得到计算机数学家，答案是肯定和否定的。因为我们可以在计算机没有人类级别智能或超人级智能的情况下完成许多有用的事情。
And then to get them to sort of do things that are at that human level or or better, we can engineer it. Okay, so this is what's happening for example in the autonomous driving domain, the systems that we have don't learn nearly as efficiently as humans or even animals. But we just engineer the hell out of it and eventually we'll have a system that's, you know, heavy engineer that kind of works well enough. It's very expensive. It takes a lot of time. But then there's going to be another step right set some years or decades in the future where we have much better learning systems that learn pretty much like humans and animals can form this kind of a distraction can build those models of the world or mental models that was talking about earlier.
然后，我们可以通过工程设计方法，使它们能够达到与人类水平或更好的表现。例如，在自动驾驶领域，我们所拥有的系统并不像人类或动物那样学习效率高。但我们会通过工程设计来改进它们，最终会有一个相对完美的、高效的系统。这需要很大的成本和时间投入。但在未来几年或几十年中，我们会迈入另一个阶段，拥有更好的学习系统，几乎可以像人类和动物那样进行这种分析，建立一个完整的世界或认知模型。
And then they may become better than humans at all the tests where are where humans are good. And and we'll have you know, serving cards from mathematicians automated virtual assistants and domestic robots and all the stuff that you know science fiction imagined for us. When when that happens, how long is that going to take? I have no idea, but we're working on it. Promising days and then the three of us will be playing in a band together while the air is popping the rest of the problems.
然后它们可能会在人类擅长的所有测试中比人类更出色。我们将拥有来自数学家自动化虚拟助手和家庭机器人的服务卡，以及所有科幻小说中想象的东西。当发生这种情况时，需要多长时间？我不知道，但我们正在努力实现。有希望的日子，那时我们三个将一起组乐队，而空气会弹出其余的问题。
Jim, what is your prediction for us? I feel reasonably confident that in 50 years time, the whole landscape of mathematics will have been completely transformed. But in a near term, it's for the reasons that Jan already mentioned, I find it a little bit less clear. I think the progress will be I think a very interesting milestone will be at what stage does an AI of whatever kind. Managed to solve the sort of problem that you get on some metal impiads where it doesn't fit into a sort of well known category of problems such as geometry problem where when you put in the right construction line. It becomes easy or something like that because those problems are amenable to just a brute force search or some inequalities, you know, you have some expression, you want to rearrange it so it looks like a sum of squares or something like that. That's something that you can search for.
吉姆，你对我们有何预测？我相当自信，在50年内，整个数学领域将会彻底转变。但是在短期内，就像珍已经提到的那样，我觉得不太清楚。我认为进展将会非常有趣。一个非常有趣的里程碑是，我们会看到一种人工智能解决各种金属合金问题的方式，这些问题并不适用于众所周知的问题分类，比如几何问题，当你增加正确的构造线时，问题会变得简单或类似的问题，因为这些问题可以通过暴力搜索或某些不等式来解决。
But there's another type of another style of problem where you have to have the right idea. There's some kind of out of the way, seeming idea, but it's not if you're if you're experienced mathematician in those sorts of problems, you kind of worry away at the problem, you dig and dig and dig and eventually you see the idea and this sort of key that unlocks the problem. Having an AI that can do that kind of problem solving, I think once we get to that, it's not clear that you can't just sort of then build on that and go much, much further and really solve interesting mass problems. We need one sort of genuinely interesting problem that doesn't fit into anything like a kind of brute forceable search class of problems. And then I think we'll be so when we get to that, I think progress will be extremely rapid after that probably.
但是还有另一种类型的问题，需要有正确的思路。这种问题有一种看似偏门的想法，但如果你是有经验的数学家，你会在问题上思考、挖掘，最终会看到解锁问题的关键思路。如果有一种可以解决这种问题的人工智能，我认为一旦实现了这一点，就可以在此基础上继续深入研究和解决更有趣的数学问题。我们需要一个确实有趣的问题，它不属于任何像粗暴的搜索类问题一样的问题类型。然后我认为，一旦我们达到了这个目标，进展将会非常快，可能会非常迅速。
Well, well, I do hope we have an opportunity for that discussion in a few years. It's been great to have both of you on the panel. Thank you so much, Timothy Gowers, Jan LeCoon. It's been a pleasure to talk about AI mathematics today. Thank you very much. Thank you, Gowers.
好的，我们希望在未来几年有机会进行这样的讨论。很高兴能有你们两位在讨论组中。非常感谢Timothy Gowers和Jan LeCoon，今天能够谈论人工智能数学真是太愉快了。非常感谢你们。谢谢，Gowers。