4 ms·

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 jus

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/
- Someone 3y ago
  From what I understand, it’s more like requiring each programmer to write implementations of arrays, dictionaries, date/time handling code, float parsing and printing, etc. Once the language designers had figured out the hardware was now capable enough to make libraries useful, it only took one programmer to do that tedious work. After that all other programmers could reuse that work. This will be similar: once a large body of definitions and proofs has been built, mathematicians will be able to reuse higher-level constructs to build proofs for their theorems. It likely also will be similar in that there will be multiple approaches to this with one (or a few; it could be that one system works best/will have the largest set of definitions for one branch of mathematics, while another ‘wins’ in another) ending up victorious.
  - t_mann 3y ago
    Exactly. There are multiple ongoing projects to formalize existing math, there seems to be some convergence on Lean4 at the moment, but the best analogy is probably programming languages, where there's a constant battle between the old guards with huge staying power and newer entrants with just too many good ideas to ignore. Except that here a lot of the attractiveness of a language will come from how much math has been formalized in that language, which gives a huge advantage to the early leaders. So there might be a bit more emphasis on 'superset-languages' like Kotlin or TypeScript here, that can make use of the libraries from existing languages.
    - staunton 3y ago
      I think porting automation will eventually solve this problem. It's really easy to write "amazingly good test-suites" for this stuff. So a computer will do the porting and you essentially "only need to read mehod signatures" to make sure the port is correct. (In which case it is completely correct with all edge cases included). This is still some work but much more manageable than e.g. porting JS to Python...
lanstin 3y ago
I'm taking a masters in mathematics, and for me the steps are at least three-fold: understanding what you are trying to prove, which is mostly thinking about it and maybe reading or talking to people; picking up pen and paper and proceeding with a sketch of the essential points; typing the proof into LaTeX for a human readable homework :) I suspect lean will change the thoughts a bit but not eliminate step one. Maybe step three becomes interactive with lean4 etc. and ends in a PR with green build, but the work does not seem likely to end there. Put it this way: Terrence Tao is unbelievably better at maths than I am; Terrence Tao with lean4 is also unbelievably better at maths than I am with lean4. As far as the value embedded in all already proven mathematics, having it in mathlib is going to make it easy to use, but extending it in the way Prof. Tao can is still pretty hard. As a side note, I've extended my experimenting with GPT4 from writing Go and emacs lisp to asking it questions about my classes and it does sound smart but will happily give fractional results for an application of Burnside's Lemma, and say things like: "An example of a simple group without an element of order 2 is any non-abelian simple group of odd order. By the Feit-Thompson theorem, every finite group of odd order is solvable, which means that non-abelian simple groups of odd order do not exist. However, this theorem does not rule out the existence of infinite simple groups of odd order." Now this answer is correct in describing how (Feit-Thompson theorem) to show that there are no simple groups of odd order, but "infinite simple groups of odd order" is pretty non-sensical. If the order is infinite, it is not odd. One hopes future iterations will develop understanding in a way that this text lacks.
- t_mann 3y ago
  You don't really need understanding if you ask (or train, or fine-tune) the AI to produce a formalized answer, and then write a loop that feeds back the compiler output until it's correct. That doesn't guarantee that it's the answer that you want, but it's guaranteed to be correct, so it is something. You can also use this approach to produce more training examples, if you have time you can manually check and annotate whether the result is what was originally asked for, and then hope that the training improves the accuracy of the initial answer (avoiding the loaded term 'understanding' here). This might substantially reduce the amount of work that needs to be done manually after the first step. If I was doing a Math degree right now, that's exactly the kind of stuff I'd want to do for my thesis, kind of jealous tbh.

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/
Someone 3y ago
From what I understand, it’s more like requiring each programmer to write implementations of arrays, dictionaries, date/time handling code, float parsing and printing, etc. Once the language designers had figured out the hardware was now capable enough to make libraries useful, it only took one programmer to do that tedious work. After that all other programmers could reuse that work. This will be similar: once a large body of definitions and proofs has been built, mathematicians will be able to reuse higher-level constructs to build proofs for their theorems. It likely also will be similar in that there will be multiple approaches to this with one (or a few; it could be that one system works best/will have the largest set of definitions for one branch of mathematics, while another ‘wins’ in another) ending up victorious.
- t_mann 3y ago
  Exactly. There are multiple ongoing projects to formalize existing math, there seems to be some convergence on Lean4 at the moment, but the best analogy is probably programming languages, where there's a constant battle between the old guards with huge staying power and newer entrants with just too many good ideas to ignore. Except that here a lot of the attractiveness of a language will come from how much math has been formalized in that language, which gives a huge advantage to the early leaders. So there might be a bit more emphasis on 'superset-languages' like Kotlin or TypeScript here, that can make use of the libraries from existing languages.
  - staunton 3y ago
    I think porting automation will eventually solve this problem. It's really easy to write "amazingly good test-suites" for this stuff. So a computer will do the porting and you essentially "only need to read mehod signatures" to make sure the port is correct. (In which case it is completely correct with all edge cases included). This is still some work but much more manageable than e.g. porting JS to Python...

lanstin 3y ago

I'm taking a masters in mathematics, and for me the steps are at least three-fold: understanding what you are trying to prove, which is mostly thinking about it and maybe reading or talking to people; picking up pen and paper and proceeding with a sketch of the essential points; typing the proof into LaTeX for a human readable homework :) I suspect lean will change the thoughts a bit but not eliminate step one. Maybe step three becomes interactive with lean4 etc. and ends in a PR with green build, but the work does not seem likely to end there. Put it this way: Terrence Tao is unbelievably better at maths than I am; Terrence Tao with lean4 is also unbelievably better at maths than I am with lean4. As far as the value embedded in all already proven mathematics, having it in mathlib is going to make it easy to use, but extending it in the way Prof. Tao can is still pretty hard. As a side note, I've extended my experimenting with GPT4 from writing Go and emacs lisp to asking it questions about my classes and it does sound smart but will happily give fractional results for an application of Burnside's Lemma, and say things like: "An example of a simple group without an element of order 2 is any non-abelian simple group of odd order. By the Feit-Thompson theorem, every finite group of odd order is solvable, which means that non-abelian simple groups of odd order do not exist. However, this theorem does not rule out the existence of infinite simple groups of odd order." Now this answer is correct in describing how (Feit-Thompson theorem) to show that there are no simple groups of odd order, but "infinite simple groups of odd order" is pretty non-sensical. If the order is infinite, it is not odd. One hopes future iterations will develop understanding in a way that this text lacks.

t_mann 3y ago
You don't really need understanding if you ask (or train, or fine-tune) the AI to produce a formalized answer, and then write a loop that feeds back the compiler output until it's correct. That doesn't guarantee that it's the answer that you want, but it's guaranteed to be correct, so it is something. You can also use this approach to produce more training examples, if you have time you can manually check and annotate whether the result is what was originally asked for, and then hope that the training improves the accuracy of the initial answer (avoiding the loaded term 'understanding' here). This might substantially reduce the amount of work that needs to be done manually after the first step. If I was doing a Math degree right now, that's exactly the kind of stuff I'd want to do for my thesis, kind of jealous tbh.