3 ms·

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 bas

by 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.
  - ykonstant 3y ago
    >And tools like Lean4 aren't limited to constructive math afaik. In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use classical logic, especially the excluded middle.
  - staunton 3y ago
    > what excuse do mere mortal mathematicians have? As an ardent proponent of formalizing proofs, I still have to disagree with this framing. Mortal mathematicians don't need any excuse not to formalize their stuff. They rather need a reason to do it. One can give lots of reasons but mathematicians often don't know them or don't agree with them. An important point is, for example, to understand that most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math.
    - trevyn 3y ago
      >most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math. Is this because the proof author is generally confident that the proof is essentially correct?
      - staunton 3y ago
        Here's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
    - t_mann 3y ago
      Mathematicians might not like the insinuation, but the best reason to formalize mathematics is indeed to check its correctness: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... tl;dr: contradictory stuff even gets published in the likes of Annals of Mathematics, and even top journals are reluctant to retract published proofs that have later been shown to be false (which in itself shouldn't be possible). Like it or not, the reasons for formalizing mathematics abound, and they have a lot to do with the fact that humans are fallible, but mathematics shouldn't be. The incredibly tedious work of tracking down a proof's correctness to the last axiom is, while overwhelming for humans, exactly the kind of work that classical computers excel at.

by t_mann 3y ago

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.
- ykonstant 3y ago
  >And tools like Lean4 aren't limited to constructive math afaik. In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use classical logic, especially the excluded middle.
- staunton 3y ago
  > what excuse do mere mortal mathematicians have? As an ardent proponent of formalizing proofs, I still have to disagree with this framing. Mortal mathematicians don't need any excuse not to formalize their stuff. They rather need a reason to do it. One can give lots of reasons but mathematicians often don't know them or don't agree with them. An important point is, for example, to understand that most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math.
  - trevyn 3y ago
    >most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math. Is this because the proof author is generally confident that the proof is essentially correct?
    - staunton 3y ago
      Here's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Array.2EanyM.20is.20inconsistent/near/396178821 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
  - t_mann 3y ago
    Mathematicians might not like the insinuation, but the best reason to formalize mathematics is indeed to check its correctness: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... tl;dr: contradictory stuff even gets published in the likes of Annals of Mathematics, and even top journals are reluctant to retract published proofs that have later been shown to be false (which in itself shouldn't be possible). Like it or not, the reasons for formalizing mathematics abound, and they have a lot to do with the fact that humans are fallible, but mathematics shouldn't be. The incredibly tedious work of tracking down a proof's correctness to the last axiom is, while overwhelming for humans, exactly the kind of work that classical computers excel at.