How computers could change pure mathematics

http://www.slate.com/articles/health_and_science/science/2015/03/computers_proving_mathematical_theorems_how_artificial_intelligence_could.html?wpsrc=sh_all_dt_fb_top

by j2kun • 11 years ago

42 28 11 years ago

slate.com

KhalilK• 11 years 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_correspon...

wolfgke• 11 years 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_p...).

kmicklas• 11 years 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

xyzzy123• 11 years 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.

iamcurious• 11 years ago

That is interesting. Do you know of any attempt?

jbapple• 11 years 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

fsk• 11 years 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.

acadien2• 11 years 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.

avn2109• 11 years ago

> "Do you really want to spend 5-10 years learning enough to check one of these proofs?"

The other replies here all seem to be "Pssh, I can already read math, and I'm a layman."

As a counterpoint, I often try to read my friends' crypto or applied math papers and literally cannot imagine understanding any of it, even given infinite time. Some stuff is just so opaque to me that I'm pretty sure it's permanently unattainable for someone with my intelligence. At the very least I'm much further than 10 years from following the state of the art in big-boy mathematics.

I would gladly use computerized comprehension-improving tools if I could get them, but then again I'm just a dumb engineer.

graycat2• 11 years 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.

BrainInAJar3• 11 years 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.

omaranto• 11 years ago

Well, and the complex numbers, they're the only algebraically closed field.

That is very, very far from being true! There are algebraically closed fields of every characteristic and of arbitrarily large cardinality. What did you mean?

bjwbell• 11 years ago

Sometimes I wonder if the usefulness of calculus is overstated compared to other areas of math. Linear algebra & discrete math pop up a lot more than integrals in CS.

I loved my real & complex analysis courses but my courses on linear algebra, abstract algebra, & discrete math have been much more useful.

graycat2• 11 years ago

I can understand and essentially agree with everything you said except your first sentence, and I'm not sure the rest of what you said does much to support your first sentence!

One point is, CS isn't the only area for applications!

E.g., in the software for my startup, sure, I have some matrix theory, right there in the code, but it turns out the matrix theory is what is left for the actual code after some earlier derivations very much in calculus!

When I was a prof in a B-school and teaching linear programming, right, awash in linear algebra, I mentioned to my students, all of whom had had the required courses in calculus, that I regarded it as a "pillar of Western Civilization". I still do.

Without Newton's second law, Maxwell's equations, etc., I strongly suspect that Western Civilization would be a very different and much less good place.

E.g., my father in law eventually slowed down his farming and got a job in town. He was head of the REMC -- Rural Electric Membership Cooperative. So, it was the local electric utility. They handled only the last few miles and bought their electric power from the grid, really from one private power company.

Some of his customers were factories, and at one point he asked me why his engineers put large capacitors outside some of the factories. Well, I'd been a ugrad math major but, except for one course I wanted instead of another that would have been required, also a physics major, and had done well in ordinary differential equations, so had see the differential equations of basic passive AC circuit theory, that is, with resistors, capacitors, and inductors.

So, sure, the factories had a lot of big electric motors with a lot of inductance. So, the utility pushed current to the motors but half a cycle later the motor pulled more current. So, net, the utility was moving a lot more electrons than necessary to deliver the power it was getting paid for and, thus, was getting more power losses in its lines. So, put a capacitor just outside the plant, and then the plant looks like a pure resistor to the electric company and all the extra electron moving is just between the motors and the capacitor just outside the plant. Ah, applied calculus!

There are many more such examples; the examples say that calculus is really important but don't really settle your question about "overstated"; for that question, I don't know what to say!

enupten• 11 years ago

Also, http://www.math.rutgers.edu/~zeilberg/Opinion137.html

(Doron Zeilberger's opinion can only be gleaned from a large sample of his writings.)

brandonb• 11 years 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

(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• 11 years 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• 11 years 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• 11 years 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-... [2]:https://gowers.wordpress.com/2013/04/14/answers-results-of-p...

How computers could change pure mathematics

Related Stories