14 ms·

The Future of Mathematics? [pdf]

152 points by mathgenius 7y ago

chris5745 7y ago
https://leanprover.github.io/about/ https://leanprover.github.io/about/
- joe_the_user 7y ago
  The entire article makes it sound like Lean is significant step in usability and power over other systems. That seems like an important thing and makes me interested to download it and play with it. Microsoft Research seems to have done some exciting things with provers over the years - Z3 is another significant program. All under the direction of Leonardo de Moura, notably.
  - 0815test 7y ago
    Power, perhaps. But I'm a bit skeptical about usability. Lean doesn't even use one of the most obvious things that make interactive proof systems far more usable - a declarative mode instead of the usual tactics-based scripts. (Yes, you can kinda sorta fake the former with "structuring" tactics, except not really - declarative proofs are really their own kind of thing.) There even used to be systems that automatically rendered inputed definitions and declarative proofs in natural language (given that the basic terms and symbols were previously defined of course) which does enable even an average mathematician to easily figure out what the system is up to. You just can't do this properly if all you have is a list of "tactics" fiddling with the prover state.
    - krapht 7y ago
      "Lean doesn't even use one of the most obvious things that make interactive proof systems far more usable - a declarative mode instead of the usual tactics-based scripts." Citation needed. I can make a perfectly reasonable Isar-style declarative proof in Lean. Just because most users of Lean choose not to do this doesn't mean it can't be done. I should mention that users are more willing to write imperative proof code instead of declarative in Lean is because 1) the interactive debugger is responsive and easy to use, and 2) writing a nicely structured declarative proof is more work than an imperative proof.
      - ratmice 7y ago
        Indeed, most of the book https://leanprover.github.io/logic_and_proof/ https://leanprover.github.io/logic_and_proof/ is entirely term mode proofs, with tactics largely absent.
adamnemecek 7y ago
I agree with this wholeheartedly. The down side is that it's going to take forever to get everyone on board. Mathematicians are very hostile to outside influences. Constructive mathematics should be more of a thing too.
- danharaj 7y ago
  How do you figure?
  - adamnemecek 7y ago
    Old school mathematicians don't understand the value of theorem provers and aren't all that excited about learning it.
    - danharaj 7y ago
      Understandable. I've been fucking with them for years as a professional programmer and I think they suck eggs.
      - adamnemecek 7y ago
        I agree but so does the math syntax.
    - ncmncm 7y ago
      The problem might be that once you try to get your theorem into a proof system, you're not doing maths anymore: now you're programming. Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard. Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already. We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever. Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof? Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system. Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering. Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?
Myrmornis 7y ago
> Possible: tools such as Lean will begin to do research semi-autonomously, perhaps uncover problems in the literature. Maybe these tools will replace research mathematicians. > In April, Christian Szegedy from Google told me that he believes that computers will be beating humans at math within ten years. I wonder whether automated mathematics software would really be able to compete with humans at explaining how areas of mathematics fit together and what roles different mathematical objects play. I'm not a mathematician so sorry for the simplistic example, but for example, would automated mathematics software be able to do something like (a) invent the complex numbers (i.e. as an object in algebra -- a "field extension" of the reals), and (b) also make a statement like "these are useful for modeling cyclical/oscillatory behavior"?
- Someone 7y ago
  One could cluster theorems and types by “connectedness”, but even then, I don’t think “algebra” would stand out as separate from, say, “geometry” or “number theory”. Those are just stickers ignorant humans put on things they thought to be significant entities centuries ago. Chances are not even “arithmetic” would stand out as a separate entity. Even if it did, the computer couldn’t give it a name that makes sense to humans. And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever.
  - Myrmornis 7y ago
    > And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever. I don’t think that’s really true. There are cyclical/oscillatory behaviors within pure mathematics, for which complex numbers are useful. Just look at the other math article that’s on HN front page currently, on the Riemann Zeta function (John Baez blog post).
- whatshisface 7y ago
  I think the image is the computer acting as the world's most brilliant grad student, solving lemmas instantly while the mathematician makes value judgements while driving.
- AlexCoventry 7y ago
solinent 7y ago
The biggest problem in mathematics has never been proving theorems. Mathematics was never focused on proof until the formalization of math became popular approximately 100 years ago. Mathematics is used as a tool to explain the world and to create the least-complex model which predicts the data. So computers can aid us in verifying our work--but ultimately we aren't interested in determining all the possible logical theorems. Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely. It's a subtle difference, but for computers to solve that problem requires for them to have a certain understanding of humans and our goals with science. I think that's more than 10 years out.
- Jimmy 7y ago
  >Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely. That's just empirically false though. Take the "perfectoid spaces" mentioned in the article. Do you think mathematicians are interested in them because they "explain the patterns in the world concisely"? No, they're interested in them because of their mathematical significance, and their applications to problems within mathematics. Mathematicians are not physicists.
  - solinent 7y ago
    > mathematical significance, and their applications to problems within mathematics These external problems ultimately are about explaining patterns in the world. I'm just saying you'll never replace the relationship between the mathematician and the physicist by simply replacing the mathematician. Instead, you'd have to replace the whole academic process, making fully autonomous universities. In which case they're still not interested in exactly same problems unless they are constructed in the same way (which they are not, since they are not human). I'm not saying that computers won't be able to aid us with these meta-theories which help push our main theories forward. So I do agree that they can come up with some theory, but not all of it, and not most of it.
- baby 7y ago
  What? Number Theory was a field of study that saw literally 0 applications up until cryptography became a serious field of study.
RyanAF7 7y ago
"I'm sorry, the what proof?" "The Coq proof." "I'm sorry, the what proof?" "The Coq proof." "I'm sorry, the what proof?" "The Coq proof." Maths really can be fun!
ivan_ah 7y ago
Could someone with knowledge of both COQ and LEAN provide more info/comparison? Are they based on the same foundation or are there differences? Might it be possible to automatically convert proofs between the two? What about "strategies" ? I was able to find a basic example of the natural numbers and the operation `plus` in both languages, and it seems like the structure is quite similar. Coq: Inductive nat : Type := | O : nat | S : nat → nat. (* S stands for successor *) Fixpoint plus (n : nat) (m : nat) : nat := match n with | O ⇒ m | S n' ⇒ S (plus n' m) end. via https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab30 https://softwarefoundations.cis.upenn.edu/lf-current/Basics.... Lean: inductive nat : Type | zero : nat | succ : nat → nat def plus : nat → nat → nat | m nat.zero := m | m (nat.succ n) := nat.succ (plus m n) via https://leanprover.github.io/introduction_to_lean/ https://leanprover.github.io/introduction_to_lean/
- krapht 7y ago
  There are subtle differences. What ostensibly they are both based on the calculus of inductive constructions, there are incompatible extensions to the logic in the kernel. The majority is convertible, though. If I had to make a programming analogy, it would be like converting between C++ and D, or different Lisp dialects. The difference is bigger than Python 3 vs Python 2, but less than F# vs OCaml. Clearly possible, in a sense, and if you can read one language, you can read the other, but automatic conversion is just out of reach due to edge cases.
inflatableDodo 7y ago
"So if proper mathematicians aren’t interested in a proof of the odd order theorem, what are they interested in? Example: Perfectoid spaces. (Topic) - Proof of odd order theorem - Perfectoid spaces Got author a Fields Medal? - Yes (1970) - Yes (2018) High level mathematics? - No - Yes Lots of PhD students and post-docs working in the area? - No - Yes Talks happening about these things all over the world? - No - Yes Mathematicans interested in 2019? - No - Yes Earlier this year, Patrick Massot, Johan Commelin and myself formalised the definition of a perfectoid space in Lean. I am getting invitations from across the EU to speak in mathematics departments about the work. Serious piece of research, or elaborate PR stunt? Maybe both." They may be learning more than programming from their contacts in the computer department. Is always much easier to get something out there when it is fully buzzword compatible.
ocfnash 7y ago
I've been following Buzzard's evangelism of proof assistants for some time. A few months ago I decided to try formalising some old mathematics olympiad problems in Coq. Part of my motivation was to get a sense for how much work would be involved in proving something slightly non-trivial but still very elementary. I managed it, but it was _a lot_ more work than expected (results here: https://github.com/ocfnash/imo-coq https://github.com/ocfnash/imo-coq). Partly based on this exercise, I think that while it is possible that mathematics may go the way of chess, so to speak, it is a lot more distant than the ten years mentioned in this article. I strongly support, very much hope, and even expect, that the use of proof assistants may become mainstream in mathematics within a generation or so but I think it is impossible to guess the exact role they will play accurately.
- meuk 7y ago
  I like to think that I'm good at these combinatorics-kind of questions, but I can't wrap my head around this one. I can follow the construction of the matrix, but I don't understand how you came up with the formula.
  - ocfnash 7y ago
    I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse. Reusing the notation of my post, here's how the formula arises. The argument based on counting cells that are either row/column good/bad requires the following of the parameter k: 1. k-1 < r/m 2. k-1 < c/n 3. k−1 < cr/(c(m-1) + r(n-1)) These are equivalent to: 1. k <= ceil r m 2. k <= ceil c n 3. k <= ceil cr (c(m-1) + r(n-1)) And so it is sufficient to have: k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1))) We can then rearrange this to the headline formula by noting: * ceil r m = ceil (cr) (cm) * ceil c n = ceil (cr) (mr) And then simplifying by repeatedly using the fact that for any x, y, z: * min (ceil x y) (ceil x z) = ceil x (max y z) All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd09f86faf9cba62a25677/q3_2001/inequalities.v#L50 https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...
xvilka 7y ago
There are way more libraries and plugins for Coq though. Using Lean would require writing them by yourself.
joker3 7y ago
No one is going to care until an important proof can't be verified and a counterexample to some step is found. At that point, you'll see a sea change. This could take twenty years, or it could happen next year.

152 points by mathgenius 7y ago

chris5745 7y ago

https://leanprover.github.io/about/ https://leanprover.github.io/about/

joe_the_user 7y ago
The entire article makes it sound like Lean is significant step in usability and power over other systems. That seems like an important thing and makes me interested to download it and play with it. Microsoft Research seems to have done some exciting things with provers over the years - Z3 is another significant program. All under the direction of Leonardo de Moura, notably.
- 0815test 7y ago
  Power, perhaps. But I'm a bit skeptical about usability. Lean doesn't even use one of the most obvious things that make interactive proof systems far more usable - a declarative mode instead of the usual tactics-based scripts. (Yes, you can kinda sorta fake the former with "structuring" tactics, except not really - declarative proofs are really their own kind of thing.) There even used to be systems that automatically rendered inputed definitions and declarative proofs in natural language (given that the basic terms and symbols were previously defined of course) which does enable even an average mathematician to easily figure out what the system is up to. You just can't do this properly if all you have is a list of "tactics" fiddling with the prover state.
  - krapht 7y ago
    "Lean doesn't even use one of the most obvious things that make interactive proof systems far more usable - a declarative mode instead of the usual tactics-based scripts." Citation needed. I can make a perfectly reasonable Isar-style declarative proof in Lean. Just because most users of Lean choose not to do this doesn't mean it can't be done. I should mention that users are more willing to write imperative proof code instead of declarative in Lean is because 1) the interactive debugger is responsive and easy to use, and 2) writing a nicely structured declarative proof is more work than an imperative proof.
    - ratmice 7y ago
      Indeed, most of the book https://leanprover.github.io/logic_and_proof/ https://leanprover.github.io/logic_and_proof/ is entirely term mode proofs, with tactics largely absent.

adamnemecek 7y ago

I agree with this wholeheartedly. The down side is that it's going to take forever to get everyone on board. Mathematicians are very hostile to outside influences. Constructive mathematics should be more of a thing too.

danharaj 7y ago
How do you figure?
- adamnemecek 7y ago
  Old school mathematicians don't understand the value of theorem provers and aren't all that excited about learning it.
  - danharaj 7y ago
    Understandable. I've been fucking with them for years as a professional programmer and I think they suck eggs.
    - adamnemecek 7y ago
      I agree but so does the math syntax.
  - ncmncm 7y ago
    The problem might be that once you try to get your theorem into a proof system, you're not doing maths anymore: now you're programming. Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard. Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already. We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever. Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof? Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system. Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering. Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?

Myrmornis 7y ago

> Possible: tools such as Lean will begin to do research semi-autonomously, perhaps uncover problems in the literature. Maybe these tools will replace research mathematicians. > In April, Christian Szegedy from Google told me that he believes that computers will be beating humans at math within ten years. I wonder whether automated mathematics software would really be able to compete with humans at explaining how areas of mathematics fit together and what roles different mathematical objects play. I'm not a mathematician so sorry for the simplistic example, but for example, would automated mathematics software be able to do something like (a) invent the complex numbers (i.e. as an object in algebra -- a "field extension" of the reals), and (b) also make a statement like "these are useful for modeling cyclical/oscillatory behavior"?

Someone 7y ago
One could cluster theorems and types by “connectedness”, but even then, I don’t think “algebra” would stand out as separate from, say, “geometry” or “number theory”. Those are just stickers ignorant humans put on things they thought to be significant entities centuries ago. Chances are not even “arithmetic” would stand out as a separate entity. Even if it did, the computer couldn’t give it a name that makes sense to humans. And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever.
- Myrmornis 7y ago
  > And b) ‘useful’ isn’t mathematics, it’s physics/biology/economics/whatever. I don’t think that’s really true. There are cyclical/oscillatory behaviors within pure mathematics, for which complex numbers are useful. Just look at the other math article that’s on HN front page currently, on the Riemann Zeta function (John Baez blog post).
whatshisface 7y ago
I think the image is the computer acting as the world's most brilliant grad student, solving lemmas instantly while the mathematician makes value judgements while driving.
AlexCoventry 7y ago

solinent 7y ago

The biggest problem in mathematics has never been proving theorems. Mathematics was never focused on proof until the formalization of math became popular approximately 100 years ago. Mathematics is used as a tool to explain the world and to create the least-complex model which predicts the data. So computers can aid us in verifying our work--but ultimately we aren't interested in determining all the possible logical theorems. Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely. It's a subtle difference, but for computers to solve that problem requires for them to have a certain understanding of humans and our goals with science. I think that's more than 10 years out.

Jimmy 7y ago
>Instead, we're only interested in finding the logically valid theorems which serve the above purpose of explaining the patterns in the world concisely. That's just empirically false though. Take the "perfectoid spaces" mentioned in the article. Do you think mathematicians are interested in them because they "explain the patterns in the world concisely"? No, they're interested in them because of their mathematical significance, and their applications to problems within mathematics. Mathematicians are not physicists.
- solinent 7y ago
  > mathematical significance, and their applications to problems within mathematics These external problems ultimately are about explaining patterns in the world. I'm just saying you'll never replace the relationship between the mathematician and the physicist by simply replacing the mathematician. Instead, you'd have to replace the whole academic process, making fully autonomous universities. In which case they're still not interested in exactly same problems unless they are constructed in the same way (which they are not, since they are not human). I'm not saying that computers won't be able to aid us with these meta-theories which help push our main theories forward. So I do agree that they can come up with some theory, but not all of it, and not most of it.
baby 7y ago
What? Number Theory was a field of study that saw literally 0 applications up until cryptography became a serious field of study.

RyanAF7 7y ago

"I'm sorry, the what proof?" "The Coq proof." "I'm sorry, the what proof?" "The Coq proof." "I'm sorry, the what proof?" "The Coq proof." Maths really can be fun!

ivan_ah 7y ago

Could someone with knowledge of both COQ and LEAN provide more info/comparison? Are they based on the same foundation or are there differences? Might it be possible to automatically convert proofs between the two? What about "strategies" ? I was able to find a basic example of the natural numbers and the operation `plus` in both languages, and it seems like the structure is quite similar. Coq: Inductive nat : Type := | O : nat | S : nat → nat. (* S stands for successor *) Fixpoint plus (n : nat) (m : nat) : nat := match n with | O ⇒ m | S n' ⇒ S (plus n' m) end. via https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab30 https://softwarefoundations.cis.upenn.edu/lf-current/Basics.... Lean: inductive nat : Type | zero : nat | succ : nat → nat def plus : nat → nat → nat | m nat.zero := m | m (nat.succ n) := nat.succ (plus m n) via https://leanprover.github.io/introduction_to_lean/ https://leanprover.github.io/introduction_to_lean/

krapht 7y ago
There are subtle differences. What ostensibly they are both based on the calculus of inductive constructions, there are incompatible extensions to the logic in the kernel. The majority is convertible, though. If I had to make a programming analogy, it would be like converting between C++ and D, or different Lisp dialects. The difference is bigger than Python 3 vs Python 2, but less than F# vs OCaml. Clearly possible, in a sense, and if you can read one language, you can read the other, but automatic conversion is just out of reach due to edge cases.

inflatableDodo 7y ago

"So if proper mathematicians aren’t interested in a proof of the odd order theorem, what are they interested in? Example: Perfectoid spaces. (Topic) - Proof of odd order theorem - Perfectoid spaces Got author a Fields Medal? - Yes (1970) - Yes (2018) High level mathematics? - No - Yes Lots of PhD students and post-docs working in the area? - No - Yes Talks happening about these things all over the world? - No - Yes Mathematicans interested in 2019? - No - Yes Earlier this year, Patrick Massot, Johan Commelin and myself formalised the definition of a perfectoid space in Lean. I am getting invitations from across the EU to speak in mathematics departments about the work. Serious piece of research, or elaborate PR stunt? Maybe both." They may be learning more than programming from their contacts in the computer department. Is always much easier to get something out there when it is fully buzzword compatible.

ocfnash 7y ago

I've been following Buzzard's evangelism of proof assistants for some time. A few months ago I decided to try formalising some old mathematics olympiad problems in Coq. Part of my motivation was to get a sense for how much work would be involved in proving something slightly non-trivial but still very elementary. I managed it, but it was _a lot_ more work than expected (results here: https://github.com/ocfnash/imo-coq https://github.com/ocfnash/imo-coq). Partly based on this exercise, I think that while it is possible that mathematics may go the way of chess, so to speak, it is a lot more distant than the ten years mentioned in this article. I strongly support, very much hope, and even expect, that the use of proof assistants may become mainstream in mathematics within a generation or so but I think it is impossible to guess the exact role they will play accurately.

meuk 7y ago
I like to think that I'm good at these combinatorics-kind of questions, but I can't wrap my head around this one. I can follow the construction of the matrix, but I don't understand how you came up with the formula.
- ocfnash 7y ago
  I presume you've been looking at my presentation here http://olivernash.org/2019/07/06/coq-imo/index.html http://olivernash.org/2019/07/06/coq-imo/index.html which I confess is quite concise; apologies if it is too terse. Reusing the notation of my post, here's how the formula arises. The argument based on counting cells that are either row/column good/bad requires the following of the parameter k: 1. k-1 < r/m 2. k-1 < c/n 3. k−1 < cr/(c(m-1) + r(n-1)) These are equivalent to: 1. k <= ceil r m 2. k <= ceil c n 3. k <= ceil cr (c(m-1) + r(n-1)) And so it is sufficient to have: k <= min (ceil r m) (ceil c n) (ceil cr (c(m-1) + r(n-1))) We can then rearrange this to the headline formula by noting: * ceil r m = ceil (cr) (cm) * ceil c n = ceil (cr) (mr) And then simplifying by repeatedly using the fact that for any x, y, z: * min (ceil x y) (ceil x z) = ceil x (max y z) All this is of course in the Coq code. E.g., the last fact mentioned above is here: https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd09f86faf9cba62a25677/q3_2001/inequalities.v#L50 https://github.com/ocfnash/imo-coq/blob/f6d2e8337fadf00583fd...

xvilka 7y ago

There are way more libraries and plugins for Coq though. Using Lean would require writing them by yourself.

joker3 7y ago

No one is going to care until an important proof can't be verified and a counterexample to some step is found. At that point, you'll see a sea change. This could take twenty years, or it could happen next year.