Transcription
Certainly, throughout my career, I've always felt that there's something missing in the way we do mathematics, you know. So, we work on a math problem and we uh we want to try to find the cool idea that's going to unlock a solution to a problem. But before you get to that point, there's a lot of drudgery. You know, there's a lot of literature review. There's a technique that you see in another paper you want to apply to your your problem, but all the all the inputs are a little bit different. So you need to hand-tweak um all the arguments and you do these computations which are useful. They give you intuition. Um but uh often it's just a slog and it's like, I have to just keep computing and computing. Um and I've tried in the past to make, you know, like little calculators to do some some small calculations faster, but it was um the technology was not there yet.
Um but about two years ago, here at IPAM actually, we ran a um uh a conference on machine-assisted proof, which I was one of the organizers for. Um and we got exposed to all the different things people were trying with SAT solvers and computer-assisted software packages, um large language models. ChatGPT had just come out and um um and Lean. And it was just an exciting universe and suddenly you could see that things were possible um and it was just beginning to happen in um in the field. Like Peter Scholze had just finished an 18-month project formalizing one of his big theorems, >> the liquid tensor >> the liquid liquid tensor experiment, which was a a big effort, one theorem, 18 months. But this was already considered a great breakthrough because, like, the formalization projects of the 20th century, they took decades to uh to complete. So those are already the speed-up um in part because we already learned how to to use all these tools from software engineering like GitHub and just much more intelligent structuring of these projects. I I got very interested both in AI and in in formalization um >> because of this conference. >> Yes. Yes. Um and so um I got convinced that this was the future of mathematics and I started giving interviews about this. Um but uh at some point, you need, you can't just talk the talk, you actually have to walk the walk. So I I actually learned Lean, which, you know, took me a month. But actually, it was it was a lot of fun, actually. It it reminded me actually of um um writing my textbooks on undergraduate teaching undergraduate analysis, like really from the foundations, getting everything completely rigorous. And it was it was it was like playing a computer game. I think Kevin Buzzard described Lean as as as the world's best computer game or something like that. >> Just perfectly addictive. >> Very addictive for a certain type of person. Yes. Um and now, in the last year, the the uh the large language models have caught up and and they can now auto-formalize um individual steps and and and really start to take away a lot of the drudgery of of formalization and really to the point where you can do it in real time. And and this opens up so so many possibilities.
>> Um so, you know, my first encounter with Kevin was actually when he taught this uh course at the MSRI on automorphic forms in 2017. Um, and I talked to him a couple years later and he said he wasn't paying attention to that at all because that was the summer that he was teaching himself Lean after Tom Hales had urged everyone at the first big proof conference that like Lean was going to be the future. Um, you know, one experience that I had when I was learning how to formally prove things for the first time was that I like slowly realized that um, I had actually never learned to really think all that clearly about mathematical arguments. And there's this kind of like endemic or maybe like cultural like messiness that sometimes comes with like proofs in higher math. And I'm curious um, like how your perception of your own mathematical cognition changed as you got deeper and deeper into like anticipating how to formalize proofs.
>> It has changed a little bit the way I approach writing papers. Uh I I I can see the invisible assumptions now that that you just customarily make. Um and um you think a little bit harder about what is the cleanest way to define things because in Lean, when you define a concept um and you want to use it, you have to first set up a lot of trivial lemmas, uh what's called API, around each each each concept. And these are the things which in a paper say, you know, "Clearly this concept is monotone," "you know, it's closed under something," but you should actually prove it. And you find that if you don't define things quite the right way, it takes twice as long or five times as long to do it, to formalize it, these these trivial statements, than than they ought to. Um, so it has given me a perspective of how to to clean up um my own writing. Um, and sometimes I get a little bit annoyed at my co-authors who don't uh who haven't seen this perspective and they're still sort of writing the old informal style. Um, Heather McBth has written um about um how formalization and automation has enabled a new style of writing proofs where so proofs are normally kind of linear. You know, you get from A to B and and and and you you you you try to have a chain of equalities or something. Um but with automation, you can just say, "Here are 10 relevant facts for um to get from A to B," and you can use a standard tool to find the right combination of these 10 facts to to finish the job. And that combination is is often something boring and not super interesting. You you know that some sort of linear algebra or something will get your conclusion from these these facts. And it's a different style of of writing proofs that actually is, in some ways, easier to read. Um, I mean, harder to check by humans, but but you see more clearly the inputs and outputs of a proof, which is something which traditional writing often conceals. I think in the case of Peter Scholze, he he essentially said that the process of getting feedback was actually making him think more clearly about this uh the actual details of this kind of key lemma, which he regarded as kind of being very productive as an activity.
>> Yeah. Um and you have this great uh I think framework that being uh rigorous or being pre-rigorous, rigorous, and then post-rigorous, and maybe how does that kind of framework fit into this uh kind of conversation?
>> Right, yeah. So um I I wrote this this rather uh viral article about how this this three stages in which you learn mathematics. So one is this pre-rigorous stage where you don't really know what a proof is, but you have some vague intuition about what works, what doesn't work. This is the type of understanding of math you have at the primary school level, often. Um, so sometimes your intuition is good, uh, sometimes it's bad, but you you don't have a way of of of telling which is which. Um and then you have the rigorous stage where you you're forced to do things exactly correctly, by the book. Um, but at this stage, you often lose your intuition because you you're you're focusing on getting all the um the steps exactly correct. Um and but it's helps you um remove all your bad intuition because you can see precise counterexamples where the argument fails. Um and you keep all your good intuition, the ones that are still consistent with your um with your with your rigor. Um and then there's this post-rigorous phase where you can switch back and forth, like you can you can argue um informally, but now um safely because you you've got rid of all your bad intuition. But then um and you know that if you need to, you can you can convert it back into um something rigorous. Conversely, you can read an argument which is rigorous and convert it back into intuitive language. So Lean has definitely cleaned up some bad um or or inefficient ways of thinking in my intuition. Um so like one very common inefficiency is is when you um state a theorem in a textbook, you often put in way too many hypotheses. You're a bit too conservative. You want to make sure that your proof is is correct. So you you add all these extra hypotheses that this is not empty, that this is continuous, or whatever, this is positive. Um and >> You want to stress-test those assumptions. >> Yeah. Uh but actually, there's also the automatic linters. You know, when when when you when you formalize something in Lean, at the end of the proof, they will say, "Oh, by the way, you never use these hypotheses." Oh, actually, yeah, this is true. I never actually needed positivity. Um and there are times in the literature where this has been a real advance, where people mentally had a mental block that a certain tool they thought was only applicable in, say, the positive case, but the proof just worked without positivity, but no one noticed this. Um but formalization lets you automatically sort of find the natural um uh shape of every single tool. Um and that that's already very useful.
>> Yeah, I think that's a really great way of putting it. Um, something that we spent a lot of time thinking about is like the interplay between insights that are derived from thinking really deeply about software engineering and computer science and how that affects the way that people think about mathematical cognition and mathematical research. Um, and like to the point that you were making earlier about um how formalization cleans up um this like understanding of what the assumptions are, what the outputs are of every theorem, right? Like that's just like good software engineering practice, right? Like Dijkstra had this whole thing about how people should be reasoning more about preconditions and postconditions. Um and similarly, this like practice of propagating around every possible assumption is like this clear anti-pattern from software engineering. Um, one thing that I really wanted to ask you actually is like, you know, what was like the aha moment for you when it came to um, like staying excited about formalization, right? Like obviously there was like, you know, this initial activation energy, you have to learn all of this like very esoteric stuff about this like niche academic programming language. Um, but like what was the moment where like as you realized that there was this process of like turning mathematics into software, but it was also something that could accelerate like your understanding, right? The process of performing mathematical discovery? For me, this was um like when I was formalizing the independence of the continuum hypothesis, there came this moment where I was lost. All of the source material was wrong and I realized I could just like turn on and off like certain critical assumptions and very quickly gain a far deeper understanding than like anything that was possible in the textbook. And I'm curious what like that sort of analog was for you.
>> Okay. So, I had two moments which really made an impression on me. Um one was when I was formalizing u this theorem I had proven with some quarters called the PFR conjecture um and um so this >> polynomial frame rule conjecture comics and had an exponent in it, 12. So we we we we we prove a conclusion, "There exists a constant such that something is true," and a constant turn be 12 because that's what happened when you when we uh um put together all the little constants in the rest of the proof. Um so we wrote out a blueprint in three, in like three weeks, I think we formalized this this con this proof of um uh C equals 12. It took 20 people. It was a it was a big effort, all by hand, with this before AI. Then someone in the archive put a little preprint saying that if you took the source material, the source paper, this, and you you made these five changes, you could lower the 12 to 11. Um and people said, "Oh, should we formalize this too?" And, you know, it took us three weeks to formalize C equals 12. So, oh my god, another three weeks to formalize C equals 11. But you basically, it wasn't quite this, but, you know, you just change it 12 to 11 in the final statement of the Lean, and then like five lines become red. They're no longer being justified. But you look at them, you you look at this this u this new preprint and say, "Oh, I know how to fix these five these five lines so that they compile." But by doing so, you know, 10 other lines become red. Um and then you go back and you do that, and within a day, we had actually updated the whole proof to do C equals 11. Um so while formalization is tedious, so even without AI, it was it was tedious for getting the first proof of a result. When once you want to modify a proof, it's much much better than the old the old way of doing it. So that was one uh one thing. Another um experience I had when formalizing um a proof from the Earth Later project called the Equation of Theories project was that someone was um formalizing a proof that um that someone else had written, and they got stuck at this one step um and they said, "I don't know how to do this step." And I was able to look at that line. I I didn't see, I didn't understand the whole proof, but I could understand that one line and I understood enough of the context to say, "Oh, you just need to copy um you need to modify this line to sort of match the um to be able to use this this tool." And I I could give a very atomic diagnosis of how to fix a proof just by inspecting three lines of like 10,000 lines of code. Um and like this is something that Lean, particularly has, like formally verified software is very very modular in a way that that other software isn't. Um and you can have really atomic discussions um about just fixing very specific lines in code without needing to know what is going on elsewhere. Um and that's something which in regular math, like I can only do that with a collaborator who's a complete expert and we've and we kind of have been talking for so long that we understand each other's um way of thinking at a really granular level. Um normally when you talk to someone who which you haven't kind of synced up >> You like complete each other's sentences. >> Yeah. Yeah. So you can get in that zone, and that's great, but um there's only a few collaborators for which I can do that. Often there's a lot of translating and you have to make all these definitions and and there's some misunderstandings. But with Lean, all this goes away because you have to, it's have a precise type description of what the problem is and how to fix it. It has atomized mathematics in a way that other ways of doing it haven't.
One of the things, just you know, thinking about how uh using mathematics in this way, I mean, one, you had the internet, and I think you were also, you know, one of the pioneers with the kind of concept of uh Polymath projects. Maybe you can maybe talk a little bit about instinct for kind of collaboration and how that's kind of evolved, you know, over maybe 20 years, 20 years or so, and now what kind of very modular type of interaction, um, sometimes anonymously, how how mathematics could kind of look in in in the future. Um, and um, sorry, just to add to that, um, you said something very interesting in your Notices of the AMS paper from a couple years ago about how you see the roles of mathematicians evolving. And I'd be curious to hear because it is very related, like how you felt your own role evolve as you sort of orchestrated these kinds of formalization projects, and how the experience that you've accrued from like running the Polymath projects um has intersected.
>> So, um, I have always felt that there's more math that I want to do than I can do on my own. So, I've always found collaborations extremely productive. Um, I've learned a lot from my co-authors. Um, and I have just learned a lot from just random interactions on the internet. Um, like um, I started a blog because I posted some question on my web page at one point, not not expecting anyone to answer, but like within, I posted a math question on my web page and enough people were reading my page at that point that within three days, I got a a complete reference to like where where this question came from. Nowadays, I use it's a very simple ChatGPT query to answer this question, but but this was revolutionary for me. Um and then Tim G proposed these Polymath projects um to try to crowdsource um um math, but uh which I enjoyed a lot. I it resonated with me that there's a lot of connections, that the more people you have, the more chance you have of making chance connections that that no one person, no matter how expert, would find on their own. But it was always bottlenecked these Polymath projects, you know, when there were 10, 20 people contributing, someone had to check all the answers and make sure that it was all coherent and summarized. And so it was me or Tim Gow or or someone else. It was extremely exhausting. >> It'd be like a star graph, like you have the central node. >> Right. So this while promising, this paradigm did not scale. Um, but it did enable these very broad projects where where people contributed lots of connections from chances of mathematics. We had no idea the people who ran the project had no idea were connected, but they were relevant. Um, but we just didn't have the organizational infrastructure of verification and and, you know, we were also running things on a blog rather and and a wiki rather than a GitHub, which is what we we would do nowadays. Um, so, um, yeah, one of the other things that these um these tools enable, formalization and AI, is is really enabling seamless collaboration between people of very different skill sets. In particular, in a formalization project, not everyone needs to know Lean, not everyone needs to know the math, not everyone needs to know GitHub. You just need sort of overlapping sets of people who know um each each individual piece. Um and then this allows also for divisional labor in a in a math project. You know, so in a traditional math project, you have maybe one or two co-authors, but even when you collaborate, everyone has to do everything, right? Everyone has to understand the the math, everyone has to understand how to write the LaTeX, how to check it. You know, like every single component of everyone does everything. You know, in in true division of labor, mass production, specialization, you know, you have people who manage, manage the project, people who do quality assurance. So I mean, so software has has already figured this out. Software engineering used to also be one lone hacker does everything. Um and that doesn't scale. You know, if you want, if you want enterprise-level software, you need uh people who specialize in in in in different things. And so I do see um more and more mass-produced mathematics at scale with that specialization. I think there will still be traditional sort of handcrafted mathematics which will be very valued. Um, but we will have this this very complimentary way of of of doing that.
And so does that mean that like you foresee the roles of most professional mathematicians evolving to that of being architects of these kinds of industrialized systems?
>> I think that the definition of a of a mathematician will broaden. Um so that there will be people who are good at at at running big projects and they'll be project managers and they will know enough math and enough Lean to um understand sort of at a high level what's going on, but they they may not be able to to sort of spot-fix individual problems. Um but they can they can coordinate big projects and that will be an important skill. Uh there'll be people who are just very good at formalizing or very good at using these new AI tools, but maybe not domain experts in in in in a field. And so and so people can join a project and leave a project and and it will become much more fluid, or you can have a more traditional project where it's a small team of people where everyone gets involved in everything. And that I think is still a very important way of doing mathematics. Um, but the important thing is that we have options. Um, so right now, a lot of people who like mathematics are shut out from doing math research because it's just too intimidating. If you want to work on a cutting-edge research project, you have to learn PhD-level math. You have to um, you know, you have to know how to to use LaTeX and you have to to know how to not make any mistakes in in in in your writing. Um, and um, you know, it's it's it's it's too intimidating. There's too much of a barrier of entry for many math-adjacent people to get involved. Um, and those who do, they often dismiss as tracks because they has so many gaps in the skill set.
>> But there is a great demand I would say in society of like citizen mathematicians like citizen science.
>> Yeah. No, we're seeing this, you know. So I'm involved a lot in this um website called this this problem um website and it's a it's become this community of of dozens of people of various levels of mathematical education contributing little things. We we figured out how to modularize different aspects of a problem. So, you know, maybe you can't solve this problem, but you can you can dig up some references, or you can make a connection to an integer sequence, or you can comment on someone else's proof, or do some numeric. Yeah, we have there's a there's a blatant pull of people who want to to do research-level math um which these tools can hopefully enable. So, so we've spoken so far about, you know, your experience with working at the bleeding edge of formalization and we've spoken so far about like your experience with coordinating large-scale efforts to sort of accelerate mathematical research um and things at the intersection of these two. Um, I think this would be like a really good time for us to jump into um like this project that you're really excited about pushing for formalizing bounds for analytic number theory. Like perhaps we could get started with like a brief explanation that could make sense for like say a lay audience for like why this problem is important and how it's sort of like a reflection of the issues that we've talked about so far.
>> Yeah. So um so just as one framing um I tend to view um automation in general as a complimentary um tool for human thought. Um, so the most obvious way to use computers to do math is you take the hardest math problems that humans want to do, the Riemann Hypothesis or whatever, and say, "Try to get the computers to do those instead." Um, and they will have some success doing the problems that humans want to do. But I think they will have much more success, at least in the near term, um doing things that are completely orthogonal to what humans like doing. Um, in particular, things that involve lots and lots of tedious number crunching and sifting through lots and lots of permutations and and and things which which uh humans do not enjoy. Um, but AI and and um will have no problem um um working with. So in analytic number theory, which is one of my fields, there was definitely um there was one one sector which has a lot of that tedious um computational work which until now only humans can do.
>> Yeah. And I would estimate it's at least for me, it takes about 70, at least 70% of my time, you know, thinking through an analytic number theory problem. There's a lot of this kind of drudgery.
>> Yeah. So I think I think we've got a lot of really neat ideas and tools um um that that can convert one type of of statement about numbers or or exponential sums or other things that or the Riemann zeta function, things that that numbers care about, into other statements that we care about. But there's all these inputs and outputs um in these tools and you have to chain them together. Um, and you can find these tools in papers, but but each paper's got the different notation, and sometimes the hypotheses they have are not quite the ones that that you have. So, you have to unpack the uh the proof and sort of build your own version. And so, there's there's a lot of of reinventing the wheel and and just adjusting parameters and you make mistakes. Um, we have little cheats to make it a little bit um less painful. So, one of which is um we say we're not going to care about constants. So instead of having a constant 27 here and a constant 38 here, I'm just going to call this C and also call this C. Um and we're just going to say the um this is a constant, this constant. We're not we're not going to work out these constants. Um and that um reduces the computation. Um it also guards against errors. You know, if you made an arithmetic error in your constant, but you still got C, nothing really bad happens. Um but the price you pay for that is that many of our results in gamma 3 are not explicit. You might prove that every odd number bigger which is large enough is the sum of three primes or whatever. Um, but how large is large? It's larger than C. What's C? Well, I didn't work it out. I was I was too lazy. Um, so there's only a small segment of um what's called um explicit analytic number theory where all the constants are exactly worked out and it's much more tedious to do um and so fewer people do it and the papers are not pleasant to read, to be honest. Uh I mean, not because of the author's fault, it's just the subject matter itself is not um it's just lots and lots of explicit computations, not, you know, it's not >> By its nature. >> Yeah. >> Yeah. It's not compelling reading. Um, it's it's it's not literature. But this I think is a prime target for automation. That if if we can um set up some pipeline where we can take these explicit um papers where the ideas, the inputs are fairly well understood, it's it's just trying to match together lots and lots of slightly incompatible tools um and getting all the parameters to match up. Um, I think uh it is well within range of current um methods to formalize these in a way which is can be done at scale and then we can maybe use some AIs to to to um or machine learning or something to to figure out the optimal ways to chain these these together and and then this creates all kinds of of new ways to to look at the field. Um, so um we um like if if for example, someone proves some new um bounds on this zeta function, we would like to drop it into this pile of 100 formalized theorems and just automate like an Excel spreadsheet. You you change one cell and all the other cells just just just update. We could have a living, dynamic um state-of-the-art of the entire field. Uh rather than have these worked-out papers with hard-coded exponents where every time the uh um result literature changes, you have you have to actually rewrite um an existing paper to to figure out what the what the newest bounds are, you know, and we do this once every 10 years or something for any given result. But it could be done in minutes um if if we had the right tooling.
>> So you're saying it's a software problem, right? Like this is probably how people thought about assembly back in the early days of programming. It was this tedious thing. There are these subroutines. It's kind of like hidden in the code. It's not really literature. Um, but like once you can reason about it at a higher level?
>> Right. And and there are ways and and um, you know, modern software, in principle, is all interoperable. You know, you you don't, you can use, you can call other routines and and there's some standardized format to to for for software tools to talk to each other, and you can create massive complex ecosystems, unfortunately, with lots of bugs, uh, because of this. Um, but you see, but with Lean, you know, you can you can hope that it's a bug-free uh way to make lots and lots of of of of research results interoperable. Um, yeah, you know, so this is something that you just, you just we just don't have right now.
And would you say or maybe kind of trying to speculate, how what percentage of, would you say, work in number theory and maybe other fields are kind of constituted of these maybe kind of drudgerous activities that if the balance is shifted, could lead to, you know, a different kind of workflow?
>> Oh, sorry, can I add a question to that? Surely there have been like non-formal verification-based or like non-computational examples of simply better mathematical technologies being invented which throughout like the history of the field have allowed mathematicians to avoid previous forms of drudgery and like think about new things. Um, and I'd be curious to hear about like what instances of that were really relevant for analytic number theory, right? Like as the way that people thought about the field evolved. Um, and then how maybe like the use of these kinds of like formalization technologies like Lean and auto-formalization um like could be viewed as an instance of that.
>> Well, um, number theory was a pioneering um adoption of experimental mathematics. So the prime number theorem, the jewel of gamma theory, was first conjectured by Gauss, who very painfully computed the first 100,000 primes or 1 million primes and predicted a pattern.
>> Still on small training data.
>> Yes. Yes. So, so Gauss had the ability to to to generalize from very small data sets. Huge Gauss. Okay. Um, because that's why you named your tool after after. But um, yeah, so so with computation, we were able to explore and there have been examples. Yeah. The Birch and Swinnerton-Dyer conjecture was also um found by by numerical exploration. Um, and more recent enumerations, I guess, by machine learning.
>> I guess even Turing was like computing zeros.
>> Yeah. Yeah. Yeah. Um, yeah. >> The zeta function. >> Yeah. The uh the the GUE hypothesis, I think, was also very much supported by numerical data. Um, so there is precedent for using computers to enable a new type of way of doing mathematics, not just of thinking by pure thought, but but data-driven um, so uh, yeah, this this type of formalization, this is not quite the same as data-driven mathematics, but but definitely computer-assisted. I have already forgotten your original question. So what what what percentage like, you know, outside of um, maybe a small corner um of the maybe machine learning community or maybe some curious people who have ventured inside, for for the average mathematician maybe working in number theory or maybe another field, what percentage of the kind of day-to-day work is kind of bottlenecked by this kind of drudgery?
>> Well, uh, it's hard to give a precise percentage, but um, I think it's indirect. So because of this drudgery, we often um consciously change the way we do our mathematics to to reduce the amount of drudgery that we do. And so we sort of consciously avoid, you know, the moment that a computation looks messy. So we'll turn and do this instead. And so if you look at raw percentages, um, just by what the the results, the work that people do, um, it looks like we have um um we have very little drudgery well, we have relatively little drudgery in our papers. But it's because we are avoiding all these potholes that are that are in in on our roads um metaphorically. Um, I think when when these tools are perfected, uh, we will change the way we do math. We'll just plow through. Yeah. If if there's a drudgery, big computation, we'll just hit it with all our technology and say, "You, you know, by Gauss or whatever, you can get from here to here." Okay. And now we just keep going. So we can blast through all these obstacles that um we just avoid um almost subconsciously. Um, now um, so I think the percentage is looks low, but um, it if you actually look at what we >> The missed opportunities. >> Is yes, as a percentage of opportunities, I think is huge.
>> Yeah. >> So earlier you were talking about how like one major bottleneck is just like finding good collaborators and like, you know, communicating and like sharing that state of mind with them in terms of like how people work on um like, you know, bounds and explicit analytic number theory today. How much, you know, like what percentage of time would you say is bottlenecked by just like trying to communicate results or like to perform this kind of distributed computation among human experts of how to propagate these bounds? And by what factor do you think mathematical research in that field could be accelerated like if this vision of yours were to come to fruition?
>> I think so, first of all, it's a trust issue, right? So with these computations, if you make one wrong computation, one wrong step somewhere, the whole computation is is bad. So you have to know who who's the reliable authors and who are not. And this is implicit information. We don't publish shame lists of of bad authors or whatever. So, a lot of it right now, you have to know the community um and you have to know who to ask. Like if if there's a result which is not quite in the literature, but you know, you can ask an expert. Yeah, I can do that. That's true. You just need to modify this. Um, so there's a bottleneck in that is that you you need to be in the network of of of you need to know all the right people and then you can work in this field. I think once you have this uh this trust guarantee, you can open the field up much more and you can you can use results that you from people that you've never met. Um, but all the proofs are guaranteed by Lean. Um, and so, yeah, that that will unblock um a lot of um a lot of work.
Yeah, I mean, I know, so so you mentioned this idea of kind of trust, I guess building on I guess past papers, you know, a researcher will maybe work in an area and then slowly over time that trust will accumulate. Um, one of the kind of motivating stories that really got me interested in uh, formalization and kind of foundations is the story of Voevodsky, who had built up this reputation, this trust of proving really remarkable results. But in the late '90s, he essentially uh wrote this paper which, I guess it was a decade after which he ended up realizing there was a a a critical error. And he essentially kind of viewed that everyone was just trusting him because he had a track record, but that is not necessarily the guarantee of truth.
>> Yeah. Yeah. Know, there there's a limit to how deep we can do, we can push mathematics currently because of this increasing web of trust. In analysis, it's less of a problem because somehow, uh, we don't, uh, we build things more from the ground up. We're closer to first principles than in other areas, but it is a limiting factor in mathematics.
That's another great u and just as kind of a maybe a follow-up question to that, as more and more so we're going to start here with maybe some of these classical papers of Ryser and Chilton, for example, other papers from the the literature from the back in the 1960s and onwards. How would you say many errors might be existing in the literature that people don't know about? So that's one question. And then also, how many of these errors will be, you know, just minor fixes and be the kind of corpus of mathematics as a field would be robust to these kinds of errors?
>> I don't know. I will be interested to find out uh what the error rate actually is. Uh maybe we're pleasantly surprised and maybe we're unpleasantly surprised. Ask me in six months.
>> Okay.
>> Yeah. I mean, we'll find out. We'll find out. Um, well, Terry, this was such a treat. Yeah. I wish we could have spent more time, but really, really excited to be working with you on this.
>> Okay. Well, hopefully six months, we'll have another conversation.
>> Yes. Okay.
>> Yeah, we will.