6 ms·

How computers could change pure mathematics

42 points by j2kun 12y ago

KhalilK 12y ago
It is worth noting that according to the Curry-Howard isomorphism[0], programs are equivalent to proofs and vice versa. 0.https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- wolfgke 12y ago
  You have to pay close attention what system of logic the proofs are written in. So, for example, it is an open problem, how and whether proofs written in homotopy type theory can be interpreted computationally (source: http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_programming http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_p...).
  - kmicklas 12y ago
    I thought this was more or less solved with the recent developments on the cubical sets models? There is even a toy interpreter with univalence and higher inductives: https://github.com/simhu/cubical https://github.com/simhu/cubical
    - jonsterling 12y ago
      They've done a lot of good work, but it's not quite done yet. The original conjecture has not been answered in the affirmative, and there are also further questions...
xyzzy123 12y ago
We're already in a world where mathematicians publish proofs that only a few other people in the world can (and have the time to) understand or verify. I'm thinking of e.g. Shinichi Mochizuki. I think a lot of the art will be getting the computer to emit proofs in a form amenable to human understanding.
- deleted 12y ago
  [deleted]
- iamcurious 12y ago
  That is interesting. Do you know of any attempt?
  - jbapple 12y ago
    There have been quite a few; Gowers himself (mentioned in the article) is working on one: "A fully automatic problem solver with human-style output" M. Ganesalingam, W. T. Gowers http://arxiv.org/abs/1309.4501 http://arxiv.org/abs/1309.4501
- fsk 12y ago
  99.9%+ of all papers published by Math professors are incomprehensible to all but a few experts. You know all those famous problems that were solved recently? How do you know they were actually solved? Maybe the Math professors are just pretending to check each others' proofs, playing a gentleman's game, and they don't want to admit that these achievements were wrong? How do you know? Do you really want to spend 5-10 years learning enough to check one of these proofs? If it's a computer-generated proof, and people checked the source code but can't read the proof (because it's terabytes of details), is that a valid proof? It isn't really leading to any greater understanding.
  - acadien 12y ago
    >99.9%+ of all papers published by Math professors are incomprehensible to all but a few experts. That's just flat out not true. In fact I would hazard a guess that the reverse is true (0.1% of math papers are incomprehensible to most). Not to say that math is simple but that just because something is highly specialized does not mean it is incomprehensible. Of course my only evidence is that the vast majority of specialized physics papers that I read only require some background in quantum mechanics, statistical mechanics and some of the problem domain. I read some papers in math journals too and feel like they're about on par in general. There are certainly some mathematicians that publish in super highly specialized fields that are remarkably difficult to understand but these are a teensy tiny minority.
graycat 12y ago
The scenario in the OP is not very promising: E.g., we can study the natural numbers and the integers, rationals, algebraics, and reals, but why the reals? Well, they are the only complete, Archimedean ordered field. Why do we care? We want the order because we want to consider bigger and smaller. We want a field because we want to be able to do basic arithmetic. But why do we want completeness? Because it says that pi, e, square root of 2, derivatives, and the Riemann integral exist with few or no more additional assumptions. Why? With completeness we get compactness, continuity, and uniform continuity and, thus, know that the Riemann integral of a real valued continuous function on a closed interval of finite length exists and we also get the fundamental theorem of calculus. Why do we care about calculus? Because it is the main way to discuss, analyze, and understand continuous change, e.g., Newton's second law and planetary motion, fluid flow, heat flow, electro-magnetism, etc. And why do we care about such analysis? Because it has been one of the pillars of physical science, engineering, the industrial revolution, and the growth of technology and economic productivity since Newton -- that is, we care about applications. So, to understand mathematics and why we do it and why some math is important, need also to understand applications to the betterment of human life on this planet, and I'm not holding my breath while waiting for the automation of that! Apparently now there is a big theme, climb on the bandwagon, ride the wave along with everyone else trying to get people up on their hind legs to grab their eyeballs for ad revenue, of with artificial intelligence, the machines are about to take over. We've had many waves before -- they come and they go. And we've had that wave of the computers about to take over before, and apparently we will more times before computers can get even remotely close to any such thing. Ah, basic rule: "Always look for the hidden agenda.". Here, it feels to me like some people are grabbing at me, by the heart, the gut, maybe below the belt, definitely below the shoulders and not between the ears.
- BrainInAJar 12y ago
  > E.g., we can study the natural numbers and the integers, rationals, algebraics, and reals, but why the reals? Well, they are the only complete, Archimedean ordered field. Well, and the complex numbers, they're the only algebraically closed field.
  - 12y ago
enupten 12y ago
Also, http://www.math.rutgers.edu/~zeilberg/Opinion137.html http://www.math.rutgers.edu/~zeilberg/Opinion137.html (Doron Zeilberger's opinion can only be gleaned from a large sample of his writings.)
brandonb 12y ago
And on the flip side, computers can suggest beautiful theorems to mathematicians by making it easy to run virtual experiments. There's now a burgeoning field of pure math called "Experimental Mathematics," where they do just that. A good intro on how computer experiments can be used in algebraic geometry is here: http://math.uga.edu/~noah/files/spheres.pdf http://math.uga.edu/~noah/files/spheres.pdf (Disclosure: Noah was my college roommate and we published a paper with Henry Cohn on experimental mathematics for high-dimensional sphere packing, so I'm a biased participant.)
- spacehome 12y ago
  I did my PhD in complex dynamical systems, and in that field, computer experimentation is invaluable. The favorite way to generate hypotheses is to explore with computer tools. Once you notice a pattern, then you trot out the theoretical tools to try to solve it.
  - cb18 12y ago
    Could you give some examples of the computer tools/software that are commonly used? Could you provide or maybe point me somewhere where I could get an expansion of the ideas in your last sentence? Is it basically creating a simulation along certain non-linear parameters then running the simulation and watching what results? Like, "hmm... that looks like a phase transition, let me see if I can workout what is going on"?
mixedmath 12y ago
I recall an experiment that Gowers was doing when he had a program that would write proofs to basic theorems and questions that an undergraduate math major might encounter in a first analysis or linear algebra course. His experiment was to see if other could distinguish between proofs written by students and proofs written by the program. You can see some of that in [1] and [2]. Although I was not fooled (nor do I think that people who both understand analysis and have a bit of foresight into the structural approaches such a program would take would be fooled), it was interesting to see. [1]:https://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/ https://gowers.wordpress.com/2013/04/02/a-second-experiment-... [2]:https://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/ https://gowers.wordpress.com/2013/04/14/answers-results-of-p...

42 points by j2kun 12y ago

It is worth noting that according to the Curry-Howard isomorphism[0], programs are equivalent to proofs and vice versa. 0.https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

wolfgke 12y ago
You have to pay close attention what system of logic the proofs are written in. So, for example, it is an open problem, how and whether proofs written in homotopy type theory can be interpreted computationally (source: http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_programming http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_p...).
- kmicklas 12y ago
  I thought this was more or less solved with the recent developments on the cubical sets models? There is even a toy interpreter with univalence and higher inductives: https://github.com/simhu/cubical https://github.com/simhu/cubical
  - jonsterling 12y ago
    They've done a lot of good work, but it's not quite done yet. The original conjecture has not been answered in the affirmative, and there are also further questions...

xyzzy123 12y ago

We're already in a world where mathematicians publish proofs that only a few other people in the world can (and have the time to) understand or verify. I'm thinking of e.g. Shinichi Mochizuki. I think a lot of the art will be getting the computer to emit proofs in a form amenable to human understanding.

deleted 12y ago
[deleted]
iamcurious 12y ago
That is interesting. Do you know of any attempt?
- jbapple 12y ago
  There have been quite a few; Gowers himself (mentioned in the article) is working on one: "A fully automatic problem solver with human-style output" M. Ganesalingam, W. T. Gowers http://arxiv.org/abs/1309.4501 http://arxiv.org/abs/1309.4501
fsk 12y ago
99.9%+ of all papers published by Math professors are incomprehensible to all but a few experts. You know all those famous problems that were solved recently? How do you know they were actually solved? Maybe the Math professors are just pretending to check each others' proofs, playing a gentleman's game, and they don't want to admit that these achievements were wrong? How do you know? Do you really want to spend 5-10 years learning enough to check one of these proofs? If it's a computer-generated proof, and people checked the source code but can't read the proof (because it's terabytes of details), is that a valid proof? It isn't really leading to any greater understanding.
- acadien 12y ago
  >99.9%+ of all papers published by Math professors are incomprehensible to all but a few experts. That's just flat out not true. In fact I would hazard a guess that the reverse is true (0.1% of math papers are incomprehensible to most). Not to say that math is simple but that just because something is highly specialized does not mean it is incomprehensible. Of course my only evidence is that the vast majority of specialized physics papers that I read only require some background in quantum mechanics, statistical mechanics and some of the problem domain. I read some papers in math journals too and feel like they're about on par in general. There are certainly some mathematicians that publish in super highly specialized fields that are remarkably difficult to understand but these are a teensy tiny minority.

graycat 12y ago

The scenario in the OP is not very promising: E.g., we can study the natural numbers and the integers, rationals, algebraics, and reals, but why the reals? Well, they are the only complete, Archimedean ordered field. Why do we care? We want the order because we want to consider bigger and smaller. We want a field because we want to be able to do basic arithmetic. But why do we want completeness? Because it says that pi, e, square root of 2, derivatives, and the Riemann integral exist with few or no more additional assumptions. Why? With completeness we get compactness, continuity, and uniform continuity and, thus, know that the Riemann integral of a real valued continuous function on a closed interval of finite length exists and we also get the fundamental theorem of calculus. Why do we care about calculus? Because it is the main way to discuss, analyze, and understand continuous change, e.g., Newton's second law and planetary motion, fluid flow, heat flow, electro-magnetism, etc. And why do we care about such analysis? Because it has been one of the pillars of physical science, engineering, the industrial revolution, and the growth of technology and economic productivity since Newton -- that is, we care about applications. So, to understand mathematics and why we do it and why some math is important, need also to understand applications to the betterment of human life on this planet, and I'm not holding my breath while waiting for the automation of that! Apparently now there is a big theme, climb on the bandwagon, ride the wave along with everyone else trying to get people up on their hind legs to grab their eyeballs for ad revenue, of with artificial intelligence, the machines are about to take over. We've had many waves before -- they come and they go. And we've had that wave of the computers about to take over before, and apparently we will more times before computers can get even remotely close to any such thing. Ah, basic rule: "Always look for the hidden agenda.". Here, it feels to me like some people are grabbing at me, by the heart, the gut, maybe below the belt, definitely below the shoulders and not between the ears.

BrainInAJar 12y ago
> E.g., we can study the natural numbers and the integers, rationals, algebraics, and reals, but why the reals? Well, they are the only complete, Archimedean ordered field. Well, and the complex numbers, they're the only algebraically closed field.
- 12y ago

enupten 12y ago

Also, http://www.math.rutgers.edu/~zeilberg/Opinion137.html http://www.math.rutgers.edu/~zeilberg/Opinion137.html (Doron Zeilberger's opinion can only be gleaned from a large sample of his writings.)

brandonb 12y ago

And on the flip side, computers can suggest beautiful theorems to mathematicians by making it easy to run virtual experiments. There's now a burgeoning field of pure math called "Experimental Mathematics," where they do just that. A good intro on how computer experiments can be used in algebraic geometry is here: http://math.uga.edu/~noah/files/spheres.pdf http://math.uga.edu/~noah/files/spheres.pdf (Disclosure: Noah was my college roommate and we published a paper with Henry Cohn on experimental mathematics for high-dimensional sphere packing, so I'm a biased participant.)

spacehome 12y ago
I did my PhD in complex dynamical systems, and in that field, computer experimentation is invaluable. The favorite way to generate hypotheses is to explore with computer tools. Once you notice a pattern, then you trot out the theoretical tools to try to solve it.
- cb18 12y ago
  Could you give some examples of the computer tools/software that are commonly used? Could you provide or maybe point me somewhere where I could get an expansion of the ideas in your last sentence? Is it basically creating a simulation along certain non-linear parameters then running the simulation and watching what results? Like, "hmm... that looks like a phase transition, let me see if I can workout what is going on"?

mixedmath 12y ago

I recall an experiment that Gowers was doing when he had a program that would write proofs to basic theorems and questions that an undergraduate math major might encounter in a first analysis or linear algebra course. His experiment was to see if other could distinguish between proofs written by students and proofs written by the program. You can see some of that in [1] and [2]. Although I was not fooled (nor do I think that people who both understand analysis and have a bit of foresight into the structural approaches such a program would take would be fooled), it was interesting to see. [1]:https://gowers.wordpress.com/2013/04/02/a-second-experiment-concerning-mathematical-writing/ https://gowers.wordpress.com/2013/04/02/a-second-experiment-... [2]:https://gowers.wordpress.com/2013/04/14/answers-results-of-polls-and-a-brief-description-of-the-program/ https://gowers.wordpress.com/2013/04/14/answers-results-of-p...