The End of Mathematical Proofs by Humans?

vivin writes "I recall how I did a bunch of Mathematical Proofs when I was in high school. In fact, proofs were an important part of Math according to the CBSE curriculum in Indian Schools. We were taught how to analyze complex problems and then break them down into simple (atomic) steps. It is similar to the derivation of a Physics formula. Proofs form a significant part of what Mathematicians do. However, according to this article from the Economist, it seems that the use of computers to generate proofs is causing mathematicians to 're-examine the foundations of their discipline.' However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed. Defenders of the same point out that there are non computer-aided proofs that are also rather large and unverifiable, like the Classification of Simple Finite Groups. Computer-aided proofs have been instrumental in solving some vexing problems like the Four Color Theorem."

Comments

Critics Reaction...

[Suhas]

...From TFA if a computer is used to make this reduction, then the number of small, obvious steps can be in the hundreds of thousands--impractical even for the most diligent mathematician to check by hand. Critics of computer-aided proof claim that this impracticability means that such proofs are inherently flawed.

So basically what they are saying is that if the proof is too long to be checked, then it is flawed? WTF?

Re:Critics Reaction...

[damieng]

Yes, thats right.

If you can't independently examine and verify your "proof" then how can it be considered proof of anything?

Re:Critics Reaction...

[Zork the Almighty]

Whether or not something is a proof is entirely our distinction to make. We choose the axioms on which the proof is based. To paraphrase Bill Klem (a famous umpire): when asked whether a pitch was a ball or a strike, "It isn't anything until I call it".

Re:Critics Reaction...

[g1t>>v]

In general, it is impossible to prove that such a 'formal logic validator' is correct since it is not possible to prove that an axiom system is correct inside that axiom system (one of Goedel's theorems). So if you would find a proof that your validator is correct, you'd have used reasoning techniques outside the logic of your validator, and do you believe those? (If so, why didn't you include them in the validator, since now your validator clearly does not support a reasoning technique you considered valid in the first place!)

Basically, at a certain point, you just have to "believe" that your axioms, logic, whatever you call it, is consistent. Because to prove it, you'd again need axioms, a logic, etcetera, ad infinitum.

Creativity

[Daxx_61]

Much of mathematics isn't just grunt power, there is also a lot of creative work going on there. Without humans to drive the computers doing the work in the right directions, it could take a long time before a computer would be able to get its proof - it simply doesn't know what it is looking for.

I for one welcome our new robotic theorum proving overlords.

Re:Creativity

[Zork the Almighty]

Without humans to drive the computers doing the work in the right directions, it could take a long time before a computer would be able to get its proof - it simply doesn't know what it is looking for.

To some extent that's true, except in areas where human understanding has reduced mathematical proof to a mechanical process. For example, verifying algebraic identities, or even geometric proofs. A more advanced example is the Risch algorithm for elementary integration. It amounts to a proof that an integral either is or is not expressible in terms of elementary functions. Eventually we come to understand an area to such an extent that we can implement mechanical algorithms and move on. The proper role of the computer is to carry out these algorithms, so that we can use them to discover something else.

If computers could write proofs...

[John Allsup]

Short, sweet, beautiful proofs of interesting and useful theorems, I would welcome them to do so with open arms.

As a tool to produce vast quantities of precise logical porridge quickly, computers have no equal in today's world, yet that is not what real mathematical proofs should be about.

Mathematical proofs should show short, clever ways of connecting otherwise disparate concepts that are only obvious in hindsight. This is where computers will always be weaker.

Computer _aided_ proofs

[irexe]

Computer proofs, like the graph color proof, are not proofs that are completely generated by a computer. The computer is merely used to brute force a fairly large number of 'special' cases which together account for all cases. The construction of the proofing method is and will remain human work, lest we create AI that matches our own I.In short, they are computer aided proofs only.

Further and more importantly, at this point we do not have and are not likely to have a machine that can prove any provable theorem (and fyi, not all truths in mathematics are provable!).

No progress without understanding

[Freaky Spook]

I remember how much I hated learning alegebra, trig, calculus etc & how much the theory sucked, I never saw any point to it & loved it when I discovered my TI-83 could do pretty much everything.

Although I discovered easier ways to do the arithmatic, I still knew the underlying theory of the equations & what the numbers were actually doing, not just what a computer was telling me.

Students should learn this, they are the basic building blocks of a science that dictates pretty much everything on this planet & although they won't have a use for everything they are taught they will have enough knowledge to "problem solve" which is what most of high school maths is designed to do, it trains our brains to think logically & be able to work out complex problems.

How are people going to be able to further phsyics, medicine, biology if they get into their respective tertiary courses without understanding the basic principals of all science & have to learn it all over again??

Or what about when computers just won't work & things have to be done by hand??

Its fair to integrate comuters into maths but not at the expense of the theory that makes us understand how things work, we should not put all our faith in technology just because its the easy thing to do.

Re:Science by AI

[Zork the Almighty]

Well at least in regards to math, I stongly doubt that this will ever be the case. Mathematics is developed over decades and centuries. With a few notable exceptions, it doesn't just fall out of the sky in textbook form. Most areas of math started out as a giagantic mess (ex; calculus, linear algebra, even geometry), and it has taken the work of countless researchers, authors, and teachers to distill and refine it. This process will continue, and it is inevitable that the subjects which baffle us today will be hammered out and taught to grade school students eventually. Well developed theory makes mathematics easier, and this in turn fuels new discoveries.

Blowhard critics could use a logic course...

[geekpuppySEA]

However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed.

Because if there's one thing that humans are better at than computers, it's performing large numbers of repeated steps. Flawlessly.

Re:Blowhard critics could use a logic course...

[mcc]

One could argue that if a proof ever contains repetitive elements, then this is a bad thing and you want to be adding some sort of abstraction to the proof anyway.

Anyway, the problem isn't the ability for the computer to perform flawlessly, the problem is in our ability to accurately specify to the computer what we want it to do. It's the whole "fast working idiot" thing, mechanical perfection isn't much good if we wind up just directing the computer to perfectly, flawlessly do the wrong thing very quickly. We have enough trouble convincing ourselves real-world software is going to do what we wanted it to after it compiles; and in that case we at least have the advantage we can run it and test it to see if it does what we expect. With software-generated proofs, not so much, since the program IS the test.

I think computer aided logic can be useful if we just think of a proof-generating software program as a funny, mechanically verifiable sort of abstraction, but you find yourself making an argument that rests on assuming that a computer program you wrote does what you think it does then this is problematic.

Re:Consider the source

[sien]

Umm. So does this mean right wingers can't do maths?

Secondly, the claim that a magazine that opposes the death penalty and supports gay marriage is right-wing rag (which presumably you meant in US terms, is kinda amusing.

The Economist, correctly stated, is a liberal magazine. It supports liberal economics and liberal social policy. Unfortunately the word 'liberal' in the US has been badly distorted.

Re:Science by AI

[rookworm]

I concur. Math will always be about insight. The best math is simple and shows why the result is true. Most mathemeticians are unsatisfied by the four-colour proof because it does not satisfy these two conditions. Even if computers are eventually able to discover such proofs, mathematicians will still have to ask the computers to search for them. We must remember that problems like solving certain differential equations used to be difficult and involved, but now thanks to computers, we don't have to worry about them as much. The same will apply for very specialized results. The big theorems will still be up to humans to prove. Think of computer- assisted math as a kind of spellchecker or Googe suggest. Computers replacing mathematicians completely is about as far-off as computers replacing poets or historians.

Re:The best math is always elegant.

[PaschalNee]

For every complex problem there is an answer that is clear, simple, and wrong. H. L. Mencken

Metaphor

[Lifewish]

As a maths degree student I can confirm that a very large portion of mathematics is devoted to finding new metaphors and angles of attack for a given situation.

This takes a ridiculous amount of pattern recognition skill (which is one area where computers tend to be outperformed by all comers) and the ability to find new ways to abstract data. A computer could possibly come up with an idea like more-than-3-dimensional space on its own, but I'd be very surprised if even the best one could think of something like topology or tensors on its own.

Production of unusual metaphors for things we thought we knew is a major driving force for the most important mathematical developments. It's not something I can see computers managing at any time in the near future.

Re:Science by AI

[tgibbs]

It has been PROVEN (and it's a well-known fact) that it's impossible to create a Turing machine which will determine if a given expression is true or false (see Incompleteness theorem [wikipedia.org] for details).

This actually is more about the limitations of logic than the limitations of computers. Indeed, Godel's Incompleteness Theorem has nothing to do with computers--it is a proof that in any system of logic (that meets some very broad criteria) there must exist statements that are true but that cannot be derived from the postulates of the system by any sequence of logical steps. Adding additional axioms does not solve this; there always remain unprovable propositions. This limitation applies to proofs by humans as well as proofs computers. However, the fact that there are some theorems that cannot be proved does not mean that there are not many others that can be.

However, the fact that there are some truths that are literally inaccessible from the postulates certainly suggests that there may be others that are accessible only by a very large number of steps, effectively requiring computers. I wonder if anybody has ever attempted to prove this?