5 ms·

Formalizing the proof of PFR in Lean4 using Blueprint: a short tour

99 points by georgehill 3y ago

laichzeit0 3y ago
I find his comment on Copilot to be enlightening. He says it’s not always right, but he still finds it useful. Kinda like that old saying in stats “all models are wrong, but some models are useful”. Language models are really helpful when you have enough experience to be able to judge when it fails, I do feel sorry for novices who don’t have enough experience yet to do that.
- t_mann 3y ago
  It arguably matters a lot less in this context - you don't need experience to see when Copilot has failed at Lean, the compiler will tell you anyway. But I'm not saying that understanding it yourself won't matter. In fact, I wouldn't be surprised if the gap between him and more mortal mathematicians actually widens with the availability of those tools.
lanstin 3y ago
Ok, I'll download lean4 and read the tutorials. Everything else I've tried that Prof. Tao has suggested has worked well. I didn't really realize that proof software had advanced so far. I tried to do a project in undergrad to put a lot of ZFC into Prolog but it was just too early to work.
- swagmoney1606 3y ago
  Lean4 has been a pleasure to learn so far! Starting with the natural numbers game was great for me: https://adam.math.hhu.de/ https://adam.math.hhu.de/
Epa095 3y ago
In the last comment below he writes > The project has now completed its primary goals; the entire dependency graph is now green.
haskellandchill 3y ago
I don't follow how the proof text is generated from lean? Or is it not, they are doing the verification in lean and the proof text is completely separate. Looking at the project more I see it's the latter. Turning lean tactics into readable proof text would be hard, as the lean phrase book he is keeping shows: https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0 https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6...
- empath-nirvana 3y ago
  There will probably be a time where most proofs are just done in Lean or some similar system and nobody bothers writing a "human readable" paper. Math will just become a kind of programming.
  - da39a3ee 3y ago
    No, I don't think that is so. For one, you still have to decide what is worthwhile to prove. The subject matter of mathematics is very different from that of programming.
  - jhanschoo 3y ago
    Informal proof will always be a thing like how project specifications are always thing. It helps to have a traditional proof to outline the major milestones of your formal proof before actually delving into the formal proof.
  - 082349872349872 3y ago
    I had been under the impression that mechanised proof assistants were much too low level for actual mathematicians (like asking programmers to explicitly allocate functional units and issue slots?) so it's interesting news that Prof. Tao finds mucking about with them worthwhile.
    - trealira 3y ago
      This isn't about Terry Tao specifically, but proof assistants can help you manage a proof when it's gotten too big or complex to manage in your head without making mistakes. There was this project to use Lean to prove a theorem of Peter Scholze's (Scholze is a well-respected professor and a famous mathemtician). Apparently, it was so big and complex that he could barely keep it in his head, so after writing the proof, he and Kevin Buzzard formalized it with Lean. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm... Then, 6 months later, he was interviewed, where he talks about using Lean for proving his theorem: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... And the experiment was finished in 2022. Announcement: https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/
InfoSecErik 3y ago
Lean has been a really exciting thing for me to watch (as an amateur observer), it's gonna go right up to the limits that Godel found.
t_mann 3y ago
I find it almost scary how casual Terry is about all this. Comparing this to my own humble attempts at graduate math, I feel like a caveman trying to rock a basic wheelbarrow who just gets a visit from a guy in a helicopter. And then that guy is stretching out his hand 'Here, try it out, it's fun, useful and not scary at all'. It was always clear to me that formalization was the future of math ever since I heard about the four-color theorem. What I did not anticipate, and what Terry seems to take in stride here, was that we'd get an AI that can almost do the job of writing the math as well around the same time as formalization starts to gain traction. The fact that I get to learn about it from the most friendly and humble generational genius is just the cherry on top.
- jhanschoo 3y ago
  My experience with copilot in lean is that it's just as useful as in programming. It guesses alright and works well for boilerplate, and structure and syntax, but you need to tune by hand whenever you need to do something significant or clever.
- rq1 3y ago
  Formalism and its “derivatives” died a long time ago already. Even Hilbert couldn’t do much about it. That being said, constructive math is still a great idea.
  - t_mann 3y ago
    Not sure what you mean by that - what I meant by formalization was to really deduce every statement in a proof from basic axioms and rules. So basically what Prof Tao did in this blog post (except that the hard rote labor has all been abstracted away and handed off to a machine). This kind of formalization is hardly dead I'd say, in fact it's just starting to gain traction in mainstream mathematics, as Prof Tao's recent work shows (if it's not too much work for a Fields medal winner to formalize their proofs, then what excuse do mere mortal mathematicians have?). So what did you mean? Edit: it's clear that the original four-color proof had nothing to do with this kind of formalization, it was just the debate that got me thinking about it. And tools like Lean4 aren't limited to constructive math afaik.

99 points by georgehill 3y ago

I find his comment on Copilot to be enlightening. He says it’s not always right, but he still finds it useful. Kinda like that old saying in stats “all models are wrong, but some models are useful”. Language models are really helpful when you have enough experience to be able to judge when it fails, I do feel sorry for novices who don’t have enough experience yet to do that.

t_mann 3y ago
It arguably matters a lot less in this context - you don't need experience to see when Copilot has failed at Lean, the compiler will tell you anyway. But I'm not saying that understanding it yourself won't matter. In fact, I wouldn't be surprised if the gap between him and more mortal mathematicians actually widens with the availability of those tools.

lanstin 3y ago

Ok, I'll download lean4 and read the tutorials. Everything else I've tried that Prof. Tao has suggested has worked well. I didn't really realize that proof software had advanced so far. I tried to do a project in undergrad to put a lot of ZFC into Prolog but it was just too early to work.

swagmoney1606 3y ago
Lean4 has been a pleasure to learn so far! Starting with the natural numbers game was great for me: https://adam.math.hhu.de/ https://adam.math.hhu.de/

Epa095 3y ago

In the last comment below he writes > The project has now completed its primary goals; the entire dependency graph is now green.

haskellandchill 3y ago

I don't follow how the proof text is generated from lean? Or is it not, they are doing the verification in lean and the proof text is completely separate. Looking at the project more I see it's the latter. Turning lean tactics into readable proof text would be hard, as the lean phrase book he is keeping shows: https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0 https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6...

empath-nirvana 3y ago
There will probably be a time where most proofs are just done in Lean or some similar system and nobody bothers writing a "human readable" paper. Math will just become a kind of programming.
- da39a3ee 3y ago
  No, I don't think that is so. For one, you still have to decide what is worthwhile to prove. The subject matter of mathematics is very different from that of programming.
- jhanschoo 3y ago
  Informal proof will always be a thing like how project specifications are always thing. It helps to have a traditional proof to outline the major milestones of your formal proof before actually delving into the formal proof.
- 082349872349872 3y ago
  I had been under the impression that mechanised proof assistants were much too low level for actual mathematicians (like asking programmers to explicitly allocate functional units and issue slots?) so it's interesting news that Prof. Tao finds mucking about with them worthwhile.
  - trealira 3y ago
    This isn't about Terry Tao specifically, but proof assistants can help you manage a proof when it's gotten too big or complex to manage in your head without making mistakes. There was this project to use Lean to prove a theorem of Peter Scholze's (Scholze is a well-respected professor and a famous mathemtician). Apparently, it was so big and complex that he could barely keep it in his head, so after writing the proof, he and Kevin Buzzard formalized it with Lean. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm... Then, 6 months later, he was interviewed, where he talks about using Lean for proving his theorem: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... And the experiment was finished in 2022. Announcement: https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/

InfoSecErik 3y ago

Lean has been a really exciting thing for me to watch (as an amateur observer), it's gonna go right up to the limits that Godel found.

t_mann 3y ago

I find it almost scary how casual Terry is about all this. Comparing this to my own humble attempts at graduate math, I feel like a caveman trying to rock a basic wheelbarrow who just gets a visit from a guy in a helicopter. And then that guy is stretching out his hand 'Here, try it out, it's fun, useful and not scary at all'. It was always clear to me that formalization was the future of math ever since I heard about the four-color theorem. What I did not anticipate, and what Terry seems to take in stride here, was that we'd get an AI that can almost do the job of writing the math as well around the same time as formalization starts to gain traction. The fact that I get to learn about it from the most friendly and humble generational genius is just the cherry on top.

jhanschoo 3y ago
My experience with copilot in lean is that it's just as useful as in programming. It guesses alright and works well for boilerplate, and structure and syntax, but you need to tune by hand whenever you need to do something significant or clever.
rq1 3y ago
Formalism and its “derivatives” died a long time ago already. Even Hilbert couldn’t do much about it. That being said, constructive math is still a great idea.
- t_mann 3y ago
  Not sure what you mean by that - what I meant by formalization was to really deduce every statement in a proof from basic axioms and rules. So basically what Prof Tao did in this blog post (except that the hard rote labor has all been abstracted away and handed off to a machine). This kind of formalization is hardly dead I'd say, in fact it's just starting to gain traction in mainstream mathematics, as Prof Tao's recent work shows (if it's not too much work for a Fields medal winner to formalize their proofs, then what excuse do mere mortal mathematicians have?). So what did you mean? Edit: it's clear that the original four-color proof had nothing to do with this kind of formalization, it was just the debate that got me thinking about it. And tools like Lean4 aren't limited to constructive math afaik.