YouSaid · the spoken record

Terence Tao

lines on the record: 252
first: 2025-06-15
most recent: 2025-06-15
sittings or episodes: 1
sources: podcast

Every line below is reproduced as it was said and linked to the record it came from. Nothing here is summarised or generated. Directory · Search · Corrections

“So I gave a bit of kin in print, but by 2026, which is now next year, there will be. Math collaborations with AI. So not fuels not a winning, but actual research level.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Already, like, I can imagine if it was at a wedding paper having some AI systems in writing it, like the old complete alone. I use it, it speeds up my own writing. You can have a theorem, you have a proof, and the proof has three cases. And I write down the proof of the first case, and the order complete just suggests that now here's half a proof of second case could work. And he was exactly correct. That was great. Save me like five 10 minutes of typing.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“One facet of this type that happened in the past was the adoptions Late. They take this typesetting language that all master students use now. So in the past, people used all kinds of word processes and typewriters and whatever. But at some point, LaTeX became easier to use than all other competitors. And people switched within a few years. It was just a dramatic phase shift.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Considerified papers are getting longer and longer in mathematics and he's harder and harder to get good refereeing for the really long ones unless they're really important. It is actually an issue which the formalization is coming in at just the right time for this to be.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“I believe so. So, in formalization, I mentioned before that it takes 10 times longer to formalize a proof than to write it by hand. With these modern AI tools and also just better tooling the lean developers are doing a great job adding more and more features and making it user-friendly. It's going from 9 to 8 to 7. Okay, no big deal. One day it will drop a little one. And that's the phase shift because suddenly it makes sense when you write a paper to write it in lean first or through a conversation with AI who is generating lean on the fly with you. And it becomes natural for journals to accept, maybe they'll offer expedite refereeing if a paper has already been formalized in lean, they'll just ask the referee to comment on the significance of the results and how it connects to literature and not worry so much about the correctness.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Using this tool, and it finds this lovely argument using a completely different tool, which eventually goes into Louis to say, no, no, no, try using this. And I might start using this, and they'll go back to the tool that I don't want you to do before. And you have to keep railroading it onto the path you want. And I could eventually force it to give the proof I wanted. But it was like herding cats. And the amount of personal effort I had to take to not just sort of prompt it, but also check its output because a lot of what it looks like is going to work. I know there's a problem on line 17. And basically arguing with it, it was more exhausting than doing it unassisted. But that's the current state of the art.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“That's funny. Yeah, he wrote in his article, a hypothetical conversation between a methodical assistant of the future and himself. He's trying to solve a problem and they would have a conversation. Sometimes the human would propose an idea and the AI would evaluate it. And sometimes the AI would propose an idea. And sometimes a competition was required and A would just go and say, okay, I've checked the 100 cases needed here or the first, you set the true for all and I've checked it for n up to 100 and it looks good so far or hang on there's a problem at n equals 46 and so just a freeform conversation where you don't know in advance where things are going to go but just based on on i think ideas are good proposals on both sides calculations get proposed on both sides i've had conversations with ai where i say okay let's we're going to collaborate to solve this math problem and it's a problem that i already know the solution to so i try to prompt it okay so here's the problem i suggest”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“I think all of the above. A lot of it is we don't know how to use these tools because it's a paradigm that's... We have not had in the past assistants that are competent enough to understand complex instructions that can work at massive scale, but are also unreliable. It's an interesting and subtle ways whilst providing sufficiently good output. It's an interesting combination. You have graduate students you work with who kind of like this, but not at scale. And we had previous software tours that can work at scale, but very narrow. So we have to figure out how to use, I mean, so Tim Kao is actually, you mentioned, he actually foresaw like in 2000, he was envisioning what mathematics would look like in actually two and a half decades.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Very rarely do transport a simpler problem. So if they can pick up a sense of smell, then they could maybe start competing with human-level mathematicians.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“That this position is good for white, it's good for black. They can't enunciate white, but just having that sense of smell lets them strategize. So if AIs gain that ability to sort of a sense of viability of certain proof strategies, I'm going to try to break up this problem into two small subtasks and say, oh, this looks good. The two tasks look like they're simpler tasks than your main task. And they still got a good chance of being true. So this is good to try. Or no, you made the problem worse because each of the two sub-problems is actually harder than your original problem, which is actually what normally happens if you try a random thing to try. Normally, it's very easy to transform a problem into an even harder problem.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, so yeah, so the sense of smell, this is one thing that humans have. And it's a metaphorical mathematical smell that. It's not clear how to get the AIs to duplicate that. Eventually, I mean, so the way Alpha Zero and so forth make progress on Go and Chess and so forth is in some sense they have developed a sense of smell for Go and chess positions.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Makes really basic mistakes, but the AI generate proofs they can look superficially flawless. And that's partly because that's what the reinforcement learning has actually trained them to do, to produce text that looks like what is correct, which for many applications is good enough. So the errors often really subtle. And then when you spot them, they're really stupid. No human would have actually made that mistake.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Problem to make the AI attack 100 adjacent problems. The things that humans do still, so where the AI really struggles right now is knowing when it's made a wrong turn. That it can say, oh, I'm going to solve this problem. I'm going to split up this problem into these two cases. I'm going to try this technique. And sometimes if you're lucky and it's a simple problem, it's the right technique and you solve the problem. And sometimes it will get proposed an approach which is just complete nonsense. But it looks like a proof. So this is one annoying thing about LLM generated mathematics. We've had human generative effects that are very low quality. Some emissions for people who don't have the formal training and so forth. But if a human proof is bad, you can tell it's bad pretty quickly.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Even a lot of underquestion mathematics, even before AI, like Wolf from Alpha, for example, is not a language model. It can solve a lot of undergraduate level math tasks. So on the computational side, verifying routine things like having a problem and say, here's a problem in partial equations. Could you solve it using any of the 20 standard techniques? And yes, I've tried all 20, and here are the 100 different permutations, and this is my results. And that type of thing, I think, will work very well. type of scaling to once you solve one”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“It's a good question. I think the nature of what mathematicians do over time has changed a lot. So a thousand years ago, mathematicians had to compute the date of Easter and really complicated calculations, but it's all automated centuries. We don't need that anymore. They used to navigate to do spherical navigation, spherical trigonometry to navigate how to get from the old world to the new very complicated calculations again, being automated.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“And if you're trying to do billions of reinforcement learning runs, you can't hire enough humans to grade those. It's already hard enough for the last time Quick Wars to do reinforcement learning on just the regular text that people get. But now if you hire people not just give thumbs up, thumbs down, but actually check the output mathematically. That's too expensive.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“It won't happen this IMO. The performance is not good enough in the time period. But there are smaller competitions. There are competitions where the answer is a number rather than a long-form proof. And AI is actually a lot better at problems where there's a specific numerical answer because it's easy to reinforce learning on it. You got the right answer, you got the wrong answer. It's a very clear signal. A long form proof either has to be formal and then the lean can give it thumbs up, thumbs down, or it's informal. But then you need a human to create it.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“But also they're giving us those full marks for the solution, which I guess is formally verified. So I guess that's fair. There are efforts. There will be a proposal at some point to actually have an AI Math Olympia where at the same time as the human contestants get the actual Olympiad problems, AIs will also be given the same problems with the same time period and the outputs will have to be graded by the same judges, which means that it will have to be written in natural language rather than formal language.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“The equivalent of. I mean, equivalent of a silver. I mean, so first of all, they took way more time than was allotted. And they had this assistance where the humans started helped by formalizing.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, yeah, no, it's a great work that shows what's possible. The approach doesn't scale currently. Three days of Google's server is server time to solve one high school math from there. This is not a scalable prospect, especially with the exponential increase as the complexity increases.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“We talked earlier about things that are amazing over time become kind of normalized. Now somehow it's, of course, geometry is a solvable problem.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Oh, yeah, it's extremely hot, actually. Natural language, it's very fault tolerant. You can make a few minor grammatical errors and a speaker in the second language can get some idea of what you're saying. But formal language, if you get one little thing wrong, the whole thing is nonsense. Even formal to formal is very hard. There are different incompatible proofs and languages. There's lean, but also Koch and Isabel and so forth. Even converting from a formal language to formal language is an unsolved, basically unsolved problem.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, the difficulty increases exponentially with the number of steps involved in the proof. It's a combinatorial explosion. So the thing of large language models is that they make mistakes. And so if a proof has got 20 steps and R24 has a 10% failure rate at each step of going in the wrong direction, it's just extremely unlikely to actually reach the end.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So we're trying something different this time around where we have everyone's an author, but we will have an appendix of this matrix and we'll see how that works.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Called DHJ Polymath in the spirit of Bobaki is a pseudonym for a famous group of mathematicians in the 20th century. But so the paper was authored under pseudonym. So none of us got the author credit. This actually turned out to be not so great for a couple of reasons. So one is that if you actually wanted to be considered for 10 years or whatever, you could not use this paper in as you're submitted on your publications because you didn't have the formal author credit. But the other thing that we've recognized much later is that when people referred to these projects, they naturally refer to the most famous person who was involved in the project. Oh, so this was Tim Gower's prior project. This was Tim Stauer's prior project and not mention the other 19 or whatever people that were involved.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“And just give a rough idea. Oh, so you did some coding and you provided some compute, but you didn't do any of the pen and paper verification or whatever. And I think that that works out traditionally. Mathematicians just order alphabetically by surname. So we don't have this tradition as in the sciences of lead author and second author and so forth, which we're proud of. We make all the authors equal status, but it doesn't quite scale to this size. So a decade ago, I was involved in these things called polymath projects. It was a crowdsourcing mathematics, but without the lean component. So it was limited by you needed a human moderator to actually check that all the contributions coming in were actually valid. And this was a huge bottleneck, actually. But still, we had projects that were 10 authors or so. But we had decided at the time not to try to decide who did what, but to have a single pseudonym. So we created this fictional character.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, yeah, I know. I mean, it's rational. So, what we've done for this project is self-report. So there are actually standard categories from the sciences of what types of contributions people give. So there's this concept and validation and resources and coding and so forth. So there's a standard list of 12 or so categories. And we just ask each contributor to this big matrix of all the authors in all the categories just to tick the boxes where they think they contributed.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, I think it's interesting to study. I mean, I think you can do studies of whether these are better predictors. There's this problem called Good Harps Law. If a statistic is actually used to incentivize performance, it becomes gamed and then it is no longer a useful measure.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“The beauty of these lean projects is that automatically you get all this data. So everything's been uploaded for this GitHub and GitHub tracks who contributed what. So you could generate statistics at any later point in time. You could say, oh, this person contributed this many lines of code or whatever. These are very crude metrics. I would definitely not want this to become like part of your tenure review or something. But I think already in enterprise computing, right? People do use some of these metrics as part of the assessment of performance of an employee. Again, this is the direction which is a bit scary for academics to go down. We don't like metrics so much.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, so it would not have been feasible. I mean, the state of the art in the literature was like 15 equations and sort of how they applied it. That's sort of at the limit of what a humanly pen and paper can do. So you need to scale that up. So you need to crowdsource, but you also need to trust. I mean, no one person can check 22 million of these proofs. You need to be computerized. And so it only became possible with Lean. We were hoping to use a lot of AI as well. So the project is almost complete. So of these 22 million, all but two have been settled. Well, actually, and of those two, we have a pen and paper proof The two, and we're formalizing it. In fact, this morning I was working on finishing it. So we're almost done on this.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Or so that are really quite hard, but a lot are easy. And the project was just to work out, to determine the entire graph, like which ones imply which other ones.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So, given any operation, it obey some laws and not others. And so we generated about 4,000 of these possible laws of algebra that certain operations can satisfy. And our question is, which laws imply which other ones? So for example, does commutativity imply sociality? And the answer is no, because it turns out you can describe an operation which obeys the commutative law, but doesn't obey the assertion of law. So by producing an example, you can show that commitment does not imply associativity. But some other laws do imply other laws by substitution and so forth. And you can write down some algebraic proof. So we look at all the pairs between these 4,000 laws and there's up to 22 million of these pairs. And for each pair, we ask, does this law imply this law? If so, give a give a proof. If not, give a counterexample. So 22 million problems, each one of which you could give to an undergraduate algebra student. And they had a decent chance of solving the problem. Although there are a few, at least 22 million, they're like a”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“By non-professional programmers, by mathematicians, and the clunky and slow. And so because of that, it's hard to really mass-produce experimental results. But I think with Lean, I mean, I'm already starting some projects where we are not just experimenting with data, but experimenting with proofs. So I have this project called the equational theories project. Basically, we generated about 22 million little problems in abstract algebra, measured back up and tell you what the project is. Okay, so abstract algebra studies operations like multiplication and addition and their abstract properties. So multiplication, for example, is commutative, x times y is always y times x is for numbers, and it's also associative. x times y times z is the same as x times y times z. So these operations obey some laws that don't obey others. For example, x times x is not always equal to x. So that law is not always true.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So, I told you before about the split between theoretical and experimental mathematics. And right now, most mathematics is theoretical and when you tiny bit is experimental. I think the platform that Lean and other software tools, so GitHub and things like that, allow, they will allow experimental mathematics to scale up to a much greater degree than we can do now. So right now, if you want to do any mathematical exploration of some mathematical pattern or something, you need some code to write out the pattern. And I mean, sometimes there are some computer algebra packages that can help, but often it's just one mathematician coding lots and lots of Python or whatever. And because coding is such an error prone activity, it's not practical to allow other people to collaborate with you on writing modules for your code. Because if one of the modules has a bug in it, the whole thing is unreliable. So you get these bespoke spaghetti code that written.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So it's like a modern supply chain. If you want to create an iPhone or some other complicated object, no one person can build up a single object, but you can have specialist who just, if they're given some widgets from some other company, they can. Combine them together to form a slightly pickle widget.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So it makes everything compatible. And trustable. Yeah, so currently only a few mathematical projects can be cut up in this way. At the current state of the art, most of the lean activity is on formalizing booths that have already been proven by humans. Math paper basically is a boop, a bluefin in a sense. It is taking a difficult statement, like big theorem and breaking it up into 100 little lemmas. But often not all written with enough detail that each one can be sort of directly formalized. A blueprint is like a really pedantically written version of a paper where every step is explained as much detail as possible. And trying to make each step kind of self-contained, or depending on only a very specific number of previous statements have been proven, so that each node of this blueprint graph that gets generated can be tackled independently of the others. And you don't even need to know how the whole thing works.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, yeah. I want to cheat more, he wants to cheat less. But eventually, we found a property which, A, he could prove, and B, I could use, and then we could prove out here. So there are all kinds of dynamics. Every collaboration has some story. No two are the same.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“If I student rentless properties of some set relating to primes, there's a certain technical condition which if I could have it, if Ben could supply me this fact, I could complete the theorem. But what I asked was a really difficult question in number theory, which he said, there's no way we can prove this. So he said, can you prove your part of the theorem using a weaker hypothesis that I have a chance to prove it? And he proposed something which he could prove, but it was too weak for me. I can't use this. So there was this conversation going back and forth.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Might work. And then hopefully that breaks up the problem into smaller sub problems, which you don't know how to do, but then you focus on the sub ones. And sometimes different collaborators are better at working on certain things. So one of my theorems I'm known for is a theorem Ben Green, which is now called the Green Tau theorem. It's a statement that the primes contain athletic progressions of anything. So it was a modification of this theorem already. And the way we collaborated was that Ben had already proven a similar result for progressions of then three. He showed that just like the primes contain lots and lots of progressions of length three and even subsets of the primes, certain subsets do. But his techniques only worked for the field questions. They didn't work for longer progressions. But I had these techniques coming from agotic theory, which is something that I had been playing with and I knew better than Ben at the time. And so if I could just”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“There's always a brainstorming process first. Yeah, so math research projects by their nature, when you start, you don't really know how to do the problem. It's not like an engineering project where somehow the theory has been established for decades and its implementation is the main difficulty. You have to figure out even what is the right path. So this is what I said about cheating first. It's like, to go back to the bridge building analogy, first assume you have an infinite budget and unlimited amounts of workforce and so forth. Now can you build this bridge? Okay. Now have infinite budget but only finite workforce. Now can you do that and so forth. So I mean of course no engineer can actually do this. Like I said, they have fixed requirements. Yes, there's this sort of jam sessions always at the beginning where you try all kinds of crazy things and you make all these assumptions that are unrealistic but you plan to fix later and you try to see if there's even some skeleton of an approach.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Paper when you want to collaborate with another mathematician, either you do it at a blackboard where you can really interact. But if you're doing it sort of by email or something, basically you have to segment it. I'm going to finish section three. You do section four, but you can't really sort of work on the same. Dozens of people across the world, most of whom I don't have never met in person. And I may not know actually even whether how reliable they are in the Prusse infrastructure. But Lean gives me a certificate of trust. So I can do trustless mathematics.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yeah, so the poose are longer, but each individual piece is easier to read. So if you take a math paper and you jump to page 27 and you look at paragraph 6 and you have a line of text of math, I often can't read it immediately because it assumes various definitions, which I have to go back and maybe 10 pages earlier this was defined. And the proof is scattered all over the place. And you basically are forced to read fairly sequentially. It's not like, say, a novel where in Ethereum you could open a novel halfway through and start reading. There's a lot of context. But when I prove in Lean, if you put your cursor on a line of code, every single object there, you can hover over it and it will say what it is, where it came from, where stuff is justified. You can trace things back much easier than sort of flipping through a math paper. So one thing that Lean really enables is actually collaborating on proofs at a really atomic scale that you really couldn't do in the past. So traditionally penetrating.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Work for each one, you make a change, and now there's Pipel things that don't work, but the process converges much more smoothly than with pen and paper.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“And like 20 people to formalize this original proof. I said, oh, but now let's update the photo 11. And what you can do with Lean is that you just, in your headline theorem, you change your 12 to 11, you run the compiler. And of the thousands of lines of code you have, 90% of them still work. And there's a couple that are lined in red. Now I can't justify these steps, but it immediately isolates which steps you need to change. But you can skip over everything which works just fine. And if you program things correctly with good programming practices, most of your lines will not be read. And there'll just be a few places where you, I mean, if you don't hard code your constants, but you sort of use smart tactics and so forth, you can localize the things you need to change to a very small period of time. So like within a day or two, we had updated our proof. Because this is very quick process. You make a change. There are 10 things now that don't.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Right. Yeah. If that was the only aspect of it, okay. But there are some cases where it was actually more pleasant to do things formally. So there's a theorem I formalized and there was a certain constant 12 that came out in the final statement. And so this 12 had to be carried all through the proof and everything had to be checked, all these other numbers that had to be consistent with this final number 12. And then so we wrote a paper through this theorem with this number 12. And then a few weeks later, someone said, oh, we can actually improve this 12 to an 11 by reworking some of these steps. And when this happens with pen and paper, every time you change a parameter, you have to check line by line that every single line of your proof still works. And there can be subtle things that you didn't quite realize. Some properties are not a matrol that you didn't even realize that you were taking advantage of. So a proof can break down at a subtle place. So we had formalized the proof with this constant 12. And then when this new paper came out, we said, oh, so that took like three weeks to formalize.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Yes, yeah. So right now I estimate that the effort, time and effort taken to formalize a proof is about 10 times the amount taken to write it out. It's doable, but it's annoying.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“Into my IDE and it scans my text and it sees what I need says I might even type now I need to use the fundamental calculus okay and then it might suggest okay try this and like maybe 25% of the time it works exactly and then another It doesn't quite work, but it's close enough that I can say, oh, if I just change it here and here, it will work. And then like half the time, it gives me complete rubbish. But people are beginning to use AIs a little bit on top, mostly on the level of basically fancy autocomplete. That you can type half of one line of a proof and it will tell you.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So it's designed for reliability. So modern AIs are not used in, it's a disjoint technology. People are beginning to use AIs on top of lean. So when a mathematician tries to program a proof in lean, often there's a step, okay, now I want to use the funding on calculus to do the next step. So the lean developers have built this massive project called Methylib, a collection of tens of thousands of useful facts about methyl objects. And somewhere in there is the fundamental theme of calculus, but you need to find it. So a lot of the bottleneck now is actually lemma search. There's a tool that you know is in there somewhere and you need to find it. And so there are various search engines specialized for methylb that you can do. But there's now these large language models that you can say, I need the fundamental calculus at this point. And it was like, okay, for example, when I code, I have GitHub co-pilot installed as a plugin.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“It's using much more traditional good old fashioned AI. You can represent all these things as trees, and there's always algorithm to match one tree to another tree.”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source
“So Lean has a lot of automation in it to try to be less annoying. So, for example, every mathematical object has to come with a type. If I talk about X, is X a real number or a natural number or a function or something. If you write things informally, it's often in context. Clearly X is equal to let X be the sum of Y and Z and Y and Z are the real numbers, so X should also be a real number. So Lean can do a lot of that, but every so often it says, wait a minute, can you tell me more about what this object is, what type of object it is? You have to think more at a philosophical level, not just sort of computations that you're doing, but sort of what each object actually is in some sense”
2025-06-15 · Lex Fridman Podcast · #472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI · IDENTIFIED FROM THE TRANSCRIPT · source