Focusing heavily on large language models and mathematical theorem provers on the backend of a system that centralized mathematical content (and ideally automatically converts it into formalized math) might be one of the biggest steps humans will have thus taken, and his shirt, is why I love the mathematical community more than any other community. Mathematicians are the most humble. Not big headed like tech people or cocky like physicists, yet consistently the backbone to all major human revolutions.
You might enjoy "The future of mathematics" on the microsoft research channel. It's the same speaker on the topic of mathematical automation, but it's around an hour long.
The main problem with the combined approach is that LLMs work by (most cleverly) interpolating between their input data. That is the sole way they produce "novel" content, therefore they cannot be used to solve open problems or, more in general, new theorems that are not too similar to the ones they know about. I'm no expert in AI, but for the little I know about proofs and machine learning, I would imagine some ad-hoc solution to the problem; maybe something that, looking at a bunch of Lean or Coq proofs, realizes specifically when it's best to apply the various proof techniques (say, induction, contraposition etc). This might be one way for them to understand which heuristics a human would apply in which context, but still, even in this case, it would have no way to invent new heuristics. No superhuman power. So, I guess something that is able to invent new heuristics is needed(?). One thing that's for sure is that the same approach used for solving finite games (hybrid approaches with graph searches) cannot be applied to maths because of the infinite nature of the game, so.... idk, I'll leave that to the experts...
Naive question here, but even if a computer program can defeat any human at a game, does that really mean the program has "solved" the game? Wouldn't a solution consist of a deteriministic algorithm which is provably correct that a human could actually follow (even if slowly) to play optimally 100% of the time? I suppose when I think of an AI approach to a problem, I think of there being some underlying statistical character, but maybe I'm wrong about that. Or maybe I need to expand my definition of a "solution"?
You are right. In game theory terms, "solved" implies an understanding of perfect play. AlphaZero and friends are superhuman, but they are not perfect.
He has very wrong notion of mathematics , He says relation between Automorphic Forms and Discrete Objects is Langlands Program but that is not Langlands Program is relation between Number Theoretic objects and Galois Representations further to Motives or Geometric Objects . For learning more about Langlands Program see the videos of Robert Langlands Abel Prize lectures.
For some reason I remember Kevin Buzzard's summer school "Automorphic Forms and the Langlands Program" at MSRI in 2017 covering the relation of number theoretic objects such as Galois representations not just with geometric things like Shimura varieties (motives) but with automorphic representations as well. The analytic ("automorphic") side of the theory was sort of the main area in which Langlands was an expert. Buzzard giving a watered-down version of Langlands here to the viewers of this TED talk probably doesn't represent any error in his "notion of mathematics." Although I'm sure that any videos of lectures given by Langlands are worth watching anyway.
Focusing heavily on large language models and mathematical theorem provers on the backend of a system that centralized mathematical content (and ideally automatically converts it into formalized math) might be one of the biggest steps humans will have thus taken, and his shirt, is why I love the mathematical community more than any other community. Mathematicians are the most humble. Not big headed like tech people or cocky like physicists, yet consistently the backbone to all major human revolutions.
I wish his presentation would be longer. It was to short for such an exciting topic.
You might enjoy "The future of mathematics" on the microsoft research channel. It's the same speaker on the topic of mathematical automation, but it's around an hour long.
The main problem with the combined approach is that LLMs work by (most cleverly) interpolating between their input data. That is the sole way they produce "novel" content, therefore they cannot be used to solve open problems or, more in general, new theorems that are not too similar to the ones they know about.
I'm no expert in AI, but for the little I know about proofs and machine learning, I would imagine some ad-hoc solution to the problem; maybe something that, looking at a bunch of Lean or Coq proofs, realizes specifically when it's best to apply the various proof techniques (say, induction, contraposition etc). This might be one way for them to understand which heuristics a human would apply in which context, but still, even in this case, it would have no way to invent new heuristics. No superhuman power.
So, I guess something that is able to invent new heuristics is needed(?). One thing that's for sure is that the same approach used for solving finite games (hybrid approaches with graph searches) cannot be applied to maths because of the infinite nature of the game, so.... idk, I'll leave that to the experts...
Naive question here, but even if a computer program can defeat any human at a game, does that really mean the program has "solved" the game? Wouldn't a solution consist of a deteriministic algorithm which is provably correct that a human could actually follow (even if slowly) to play optimally 100% of the time? I suppose when I think of an AI approach to a problem, I think of there being some underlying statistical character, but maybe I'm wrong about that. Or maybe I need to expand my definition of a "solution"?
You are right. In game theory terms, "solved" implies an understanding of perfect play. AlphaZero and friends are superhuman, but they are not perfect.
He has very wrong notion of mathematics , He says relation between Automorphic Forms and Discrete Objects is Langlands Program but that is not Langlands Program is relation between Number Theoretic objects and Galois Representations further to Motives or Geometric Objects . For learning more about Langlands Program see the videos of Robert Langlands Abel Prize lectures.
For some reason I remember Kevin Buzzard's summer school "Automorphic Forms and the Langlands Program" at MSRI in 2017 covering the relation of number theoretic objects such as Galois representations not just with geometric things like Shimura varieties (motives) but with automorphic representations as well. The analytic ("automorphic") side of the theory was sort of the main area in which Langlands was an expert. Buzzard giving a watered-down version of Langlands here to the viewers of this TED talk probably doesn't represent any error in his "notion of mathematics." Although I'm sure that any videos of lectures given by Langlands are worth watching anyway.