7 ms·

The Dawn of Formalized Mathematics

127 points by matt_d 5y ago

outlace 5y ago
Highly recommend Lean theorem prover for programmers who want to self-learn some mathematics
- fogof 5y ago
  I want to second this. I started working on a project in Lean only last December. Since then, I've made several contributions to the mathlib github repo - the first time I've contributed to open source despite wanting to get into it for a few years. The Zulip forum https://leanprover.zulipchat.com/# https://leanprover.zulipchat.com/# is very welcoming and responsive to questions. If you're interested in mathematics and you want to contribute to the growing hivemind working on this kind of thing, I highly encourage you to learn Lean and join this community.
- zozbot234 5y ago
  I'm not sure if I would recommend that, given that Lean has less support for constructive math than some existing systems, and constructive math can be very convenient for proving stuff about programs/computations.
  - penisverse 5y ago
    At least it's easy to use, i can't for the life of me install and set up agda for example.
    - creata 5y ago
      This is way off topic, but that's funny, because it's the other way around for me: I can install Agda with a `pacman -S agda`, but I'd need to go through the AUR for Lean.
    - IngoBlechschmid 5y ago
      For this reason, I decided to make Agda playable in the browser here: https://agdapad.quasicoherent.io/ https://agdapad.quasicoherent.io/ Enjoy! :-)
  - outlace 5y ago
    Thats not true… in Lean you can restrict yourself to constructive math if you want to for some reason. Just that most actual mathematicians don’t.
  - creata 5y ago
    > constructive math can be very convenient for proving stuff about programs/computations. How? I can see how proving properties of programs is a place where constructivism won't get in the way, but do you have an example of where it can be more convenient?
    - logicchains 5y ago
      The Howard-Curry correspondence only applies if you stick to constructive maths. This means all your proofs are also programs (and computable) for free. E.g. if trying to prove "blah(x) = blaz(x)" for a fixed x, where blah and blaz are both computable predicates, then the proof can be solved easily just by evaluating blah(x) and blaz(x). This can't be done if blah or blaz isn't computable.
      - creata 5y ago
        Sure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate them, or they're not, in which case neither could evaluate them?
        logicchains 5y ago
        Yep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof assistant prevents accidentally doing this, and encourages using constructive definitions where possible. It also encourages using computable mathematical formulations (e.g. computable reals vs classical reals).
      - ProfHewitt 5y ago
        The Howard-Curry correspondence does not help proving properties of concurrent systems. Instead, need to use Actor Event induction: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003
    - ProfHewitt 5y ago
  - mbrodersen 5y ago
    Real mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.
    - zozbot234 5y ago
      The mathematicians who study topos theory, the 'internal logic' of whatever category etc. are definitely "real" mathematicians, and they have to care about constructive settings because these come up very naturally in that field. Constructivism is not an isolated niche anymore, it interacts with "real" math too.
- mbrodersen 5y ago
  Agree! I am learning a lot just reading through the mathlib definitions and playing around with proving simple compilers correct.
pohl 5y ago
This was worth it just to see the slide referencing "Liquid Tensor Experiment", a on pun on Liquid Tension Expermient: https://www.youtube.com/watch?v=aSU0xBGfkfg https://www.youtube.com/watch?v=aSU0xBGfkfg
dwrensha 5y ago
I really like this quote, from 39:50 in the talk: > This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.
- bookofsand 5y ago
  Change itself is speeding up. We are going to zoom through the hive era and jump straight into AI era, where 99%, if not more, of the heavy lifting will be done by the machines. The centaur era is rather close ahead. Beyond that, the hope is there will be some room left for humans, but I won't take a long term bet.
  - bawolff 5y ago
    People have been waxing poetic about the singularity for a long time now. I'm not holding my breath.
    - habibur 5y ago
      Neither am I. Had been hearing of downfall of software development since the dawn. Remember 4GL? 4th Generation languages were supposed to end programmer dependency. It will be managers writing what they want in mostly plain English and computer will do the rest. That was the vision of SQL too. Managers were supposed to write "select sum(amount) from sales where month=2021-05" Didn't happen. Developers still prefer function calls, ORMs and API calls over English-like sentences. And 4GL has died off like UML. But things are better now. Getting easier. You don't need to write assembly. And can develop a web page using wordpress without any coding. But that created a separate class of developers and didn't make seasoned developers out of job. Even though it's been like 20 years since. Underneath it all there will be people that develop and maintain these AI techs. And as usage rise so will demand for people that can maintain and develop those AI.
foxes 5y ago
I think it is the future. Writing a mathematical proof is writing a computer program. I think it is common to see lots of lets say hacky, untyped work, like some janky bash script, that takes you on some adventure, that you have to spend extra work exploring. Imagine instead reading some declarative program. Everything formalised, use of higher order functions/constructs when appropriate that encapsulate important generalisable ideas (eg in the programming example using "map" when you want to loop over some list). Hacky stuff is fine for exploration and experimentation. But something for publication should be clear. You could use engineering principles, optimising your proofs for readability and efficiency, version control. Seems like it is the future. Disclaimer I have written many "hacky" proofs.
- bmitc 5y ago
  I am of the opinion that mathematics is very much a human endeavor. Writing a proof is to convince other mathematicians that it’s true. While formalized mathematics is one such technique, I don’t believe it will replace how mathematics is generally done. Writing a program is something different entirely. One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.
  - foxes 5y ago
    A verified proof is a very convincing argument. I am not against including a human focused discussion of a proof, stepping through it in human terms. A verified proof is more like the final step or output. I agree this is not how maths is done, there is a huge exploration stage. People do not just crank out a proof even though sometimes it is written in a way to make you believe that. You can spend days, weeks, months exploring. But at some point you should try to formalise that into something coherent. Amendment: this seems to be a very controversial discussion with wildly swinging upvotes/downvotes. I hope people would elaborate on their viewpoints.
    - bmitc 5y ago
elcapitan 5y ago
How does Lean compare to Coq? And which one would be preferable for non-mathematicians trying to learn more about math? Which one would be better if you come from a software background and want to do formal verification for parts of your programs?
- srl 5y ago
  This is only a partial answer, but my understanding is that Lean is really not meant for software verification work. That's very much Coq's alley. I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.
  - mbrodersen 5y ago
    Not true. Lean and Coq are very similar. However it is true that Coq has more of a history when it comes to verifying software (CompCert is written in Coq for example). And Lean is the state of the art when it comes to mathematics (mathlib).
- logicchains 5y ago
  There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.
  - elcapitan 5y ago
    Thanks, that's very helpful!
    - logicchains 5y ago
      You're welcome!
artagnon 5y ago
Sorry to be the buzzkill here, but I'll say what needs to be said. Computers are decades away from being able to formalize any serious mathematical results, and "formalized mathematics" is a fancy term for "formal methods in computer science". I've worked for a good numbers of years in the US software industry as a compiler engineer, and am a Mathematics masters student now. I've played with proof assistants extensively, and in particular I'm currently working on a paper to formalize semi-cubical sets in Coq. Working with Coq has been most painful, and it requires spoon-feeding for verifying even the simplest results. Worst of all, it's riddled with bugs, and I'm constantly astounded at how stupid it is. That said, Lean is a much newer proof assistant, and while it offers some nice conveniences, it will take at least a decade before its power is comparable to Coq. Mathematics is a solitary activity for good reason. Much of the work happens on pen-and-paper, and it takes months of toil to prove a result. No serious mathematician is going to go through the pain of encoding her proof in a proof assistant, and spoon-feeding it to verify every little result. What's the news? That several computer scientists in the area are doing the work of formalizing simple mathematical results in Lean. Don't mistake Lean for some ground-breaking new technology; sure, it has a thriving community, and offers many conveniences, but the level of abstraction it offers isn't even close to the level of abstraction that my subject offers (I study stable ∞-categories). Sure, if you want to do the thankless work of formalizing well-known results from group theory, ring theory, or vector spaces in Lean, be my guest. But don't be under the illusion that it's going to change the way mathematics is fundamentally done. The work is comparable to type-setting a document, except that it's a LOT more painful.
- mathgenius 5y ago
  This is just not accurate. "I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research." Peter Scholze [1]. [1] 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-...
- ukj 5y ago
  It's called "learning a new language". You know what you want to express - you don't know how to express it in a way that your interlocutor will understand. Whether your interlocutor is a computer speaking Lean, or a human speaking your non-native tongue. All the benefits are on the other side of the learning curve.
touisteur 5y ago
I'm wondering about the 'searchability' or canonicalization of such a theorem library. How do you make sure there's no duplicate work? How do you index the thing? Can you match and input / output proposition and look through the whole database and have it find all related theorems? I'm thinking 'automatic lemma matching' for software verification. e.g. In a SPARK proof you might need to use a lemma [0]. If you formal math education is lacking or maybe your theorem library is not encyclopedic, you might want suggestions from 'the hive'... [0] https://blog.adacore.com/gnatprove-tips-and-tricks-using-the-lemma-library https://blog.adacore.com/gnatprove-tips-and-tricks-using-the...
- alimw 5y ago
  There is a tactic (in Lean) called library_search. I'm not sure it's as smart as you'd like? But it is useful. https://leanprover-community.github.io/mathlib_docs/tactics.html#library_search https://leanprover-community.github.io/mathlib_docs/tactics....
  - touisteur 5y ago
    Thanks now I need to install and test this Lean thing.

127 points by matt_d 5y ago

outlace 5y ago

Highly recommend Lean theorem prover for programmers who want to self-learn some mathematics

fogof 5y ago
I want to second this. I started working on a project in Lean only last December. Since then, I've made several contributions to the mathlib github repo - the first time I've contributed to open source despite wanting to get into it for a few years. The Zulip forum https://leanprover.zulipchat.com/# https://leanprover.zulipchat.com/# is very welcoming and responsive to questions. If you're interested in mathematics and you want to contribute to the growing hivemind working on this kind of thing, I highly encourage you to learn Lean and join this community.
zozbot234 5y ago
I'm not sure if I would recommend that, given that Lean has less support for constructive math than some existing systems, and constructive math can be very convenient for proving stuff about programs/computations.
- penisverse 5y ago
  At least it's easy to use, i can't for the life of me install and set up agda for example.
  - creata 5y ago
    This is way off topic, but that's funny, because it's the other way around for me: I can install Agda with a `pacman -S agda`, but I'd need to go through the AUR for Lean.
  - IngoBlechschmid 5y ago
    For this reason, I decided to make Agda playable in the browser here: https://agdapad.quasicoherent.io/ https://agdapad.quasicoherent.io/ Enjoy! :-)
- outlace 5y ago
  Thats not true… in Lean you can restrict yourself to constructive math if you want to for some reason. Just that most actual mathematicians don’t.
- creata 5y ago
  > constructive math can be very convenient for proving stuff about programs/computations. How? I can see how proving properties of programs is a place where constructivism won't get in the way, but do you have an example of where it can be more convenient?
  - logicchains 5y ago
    The Howard-Curry correspondence only applies if you stick to constructive maths. This means all your proofs are also programs (and computable) for free. E.g. if trying to prove "blah(x) = blaz(x)" for a fixed x, where blah and blaz are both computable predicates, then the proof can be solved easily just by evaluating blah(x) and blaz(x). This can't be done if blah or blaz isn't computable.
    - creata 5y ago
      Sure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate them, or they're not, in which case neither could evaluate them?
      - logicchains 5y ago
        Yep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof assistant prevents accidentally doing this, and encourages using constructive definitions where possible. It also encourages using computable mathematical formulations (e.g. computable reals vs classical reals).
    - ProfHewitt 5y ago
      The Howard-Curry correspondence does not help proving properties of concurrent systems. Instead, need to use Actor Event induction: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003
  - ProfHewitt 5y ago
- mbrodersen 5y ago
  Real mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.
  - zozbot234 5y ago
    The mathematicians who study topos theory, the 'internal logic' of whatever category etc. are definitely "real" mathematicians, and they have to care about constructive settings because these come up very naturally in that field. Constructivism is not an isolated niche anymore, it interacts with "real" math too.
mbrodersen 5y ago
Agree! I am learning a lot just reading through the mathlib definitions and playing around with proving simple compilers correct.

pohl 5y ago

This was worth it just to see the slide referencing "Liquid Tensor Experiment", a on pun on Liquid Tension Expermient: https://www.youtube.com/watch?v=aSU0xBGfkfg https://www.youtube.com/watch?v=aSU0xBGfkfg

dwrensha 5y ago

I really like this quote, from 39:50 in the talk: > This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.

bookofsand 5y ago
Change itself is speeding up. We are going to zoom through the hive era and jump straight into AI era, where 99%, if not more, of the heavy lifting will be done by the machines. The centaur era is rather close ahead. Beyond that, the hope is there will be some room left for humans, but I won't take a long term bet.
- bawolff 5y ago
  People have been waxing poetic about the singularity for a long time now. I'm not holding my breath.
  - habibur 5y ago
    Neither am I. Had been hearing of downfall of software development since the dawn. Remember 4GL? 4th Generation languages were supposed to end programmer dependency. It will be managers writing what they want in mostly plain English and computer will do the rest. That was the vision of SQL too. Managers were supposed to write "select sum(amount) from sales where month=2021-05" Didn't happen. Developers still prefer function calls, ORMs and API calls over English-like sentences. And 4GL has died off like UML. But things are better now. Getting easier. You don't need to write assembly. And can develop a web page using wordpress without any coding. But that created a separate class of developers and didn't make seasoned developers out of job. Even though it's been like 20 years since. Underneath it all there will be people that develop and maintain these AI techs. And as usage rise so will demand for people that can maintain and develop those AI.

foxes 5y ago

I think it is the future. Writing a mathematical proof is writing a computer program. I think it is common to see lots of lets say hacky, untyped work, like some janky bash script, that takes you on some adventure, that you have to spend extra work exploring. Imagine instead reading some declarative program. Everything formalised, use of higher order functions/constructs when appropriate that encapsulate important generalisable ideas (eg in the programming example using "map" when you want to loop over some list). Hacky stuff is fine for exploration and experimentation. But something for publication should be clear. You could use engineering principles, optimising your proofs for readability and efficiency, version control. Seems like it is the future. Disclaimer I have written many "hacky" proofs.

bmitc 5y ago
I am of the opinion that mathematics is very much a human endeavor. Writing a proof is to convince other mathematicians that it’s true. While formalized mathematics is one such technique, I don’t believe it will replace how mathematics is generally done. Writing a program is something different entirely. One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.
- foxes 5y ago
  A verified proof is a very convincing argument. I am not against including a human focused discussion of a proof, stepping through it in human terms. A verified proof is more like the final step or output. I agree this is not how maths is done, there is a huge exploration stage. People do not just crank out a proof even though sometimes it is written in a way to make you believe that. You can spend days, weeks, months exploring. But at some point you should try to formalise that into something coherent. Amendment: this seems to be a very controversial discussion with wildly swinging upvotes/downvotes. I hope people would elaborate on their viewpoints.
  - bmitc 5y ago

elcapitan 5y ago

How does Lean compare to Coq? And which one would be preferable for non-mathematicians trying to learn more about math? Which one would be better if you come from a software background and want to do formal verification for parts of your programs?

srl 5y ago
This is only a partial answer, but my understanding is that Lean is really not meant for software verification work. That's very much Coq's alley. I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.
- mbrodersen 5y ago
  Not true. Lean and Coq are very similar. However it is true that Coq has more of a history when it comes to verifying software (CompCert is written in Coq for example). And Lean is the state of the art when it comes to mathematics (mathlib).
logicchains 5y ago
There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.
- elcapitan 5y ago
  Thanks, that's very helpful!
  - logicchains 5y ago
    You're welcome!

artagnon 5y ago

Sorry to be the buzzkill here, but I'll say what needs to be said. Computers are decades away from being able to formalize any serious mathematical results, and "formalized mathematics" is a fancy term for "formal methods in computer science". I've worked for a good numbers of years in the US software industry as a compiler engineer, and am a Mathematics masters student now. I've played with proof assistants extensively, and in particular I'm currently working on a paper to formalize semi-cubical sets in Coq. Working with Coq has been most painful, and it requires spoon-feeding for verifying even the simplest results. Worst of all, it's riddled with bugs, and I'm constantly astounded at how stupid it is. That said, Lean is a much newer proof assistant, and while it offers some nice conveniences, it will take at least a decade before its power is comparable to Coq. Mathematics is a solitary activity for good reason. Much of the work happens on pen-and-paper, and it takes months of toil to prove a result. No serious mathematician is going to go through the pain of encoding her proof in a proof assistant, and spoon-feeding it to verify every little result. What's the news? That several computer scientists in the area are doing the work of formalizing simple mathematical results in Lean. Don't mistake Lean for some ground-breaking new technology; sure, it has a thriving community, and offers many conveniences, but the level of abstraction it offers isn't even close to the level of abstraction that my subject offers (I study stable ∞-categories). Sure, if you want to do the thankless work of formalizing well-known results from group theory, ring theory, or vector spaces in Lean, be my guest. But don't be under the illusion that it's going to change the way mathematics is fundamentally done. The work is comparable to type-setting a document, except that it's a LOT more painful.

mathgenius 5y ago
This is just not accurate. "I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research." Peter Scholze [1]. [1] 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-...
ukj 5y ago
It's called "learning a new language". You know what you want to express - you don't know how to express it in a way that your interlocutor will understand. Whether your interlocutor is a computer speaking Lean, or a human speaking your non-native tongue. All the benefits are on the other side of the learning curve.

touisteur 5y ago

I'm wondering about the 'searchability' or canonicalization of such a theorem library. How do you make sure there's no duplicate work? How do you index the thing? Can you match and input / output proposition and look through the whole database and have it find all related theorems? I'm thinking 'automatic lemma matching' for software verification. e.g. In a SPARK proof you might need to use a lemma [0]. If you formal math education is lacking or maybe your theorem library is not encyclopedic, you might want suggestions from 'the hive'... [0] https://blog.adacore.com/gnatprove-tips-and-tricks-using-the-lemma-library https://blog.adacore.com/gnatprove-tips-and-tricks-using-the...

alimw 5y ago
There is a tactic (in Lean) called library_search. I'm not sure it's as smart as you'd like? But it is useful. https://leanprover-community.github.io/mathlib_docs/tactics.html#library_search https://leanprover-community.github.io/mathlib_docs/tactics....
- touisteur 5y ago
  Thanks now I need to install and test this Lean thing.