Slashdot Mirror
Are Computers Ready to Create Mathematical Proofs?
DoraLives writes "Interesting article in the New York Times regarding the quandary mathematicians are now finding themselves in. In a lovely irony reminiscent of the torture, in days of yore, that students were put through when it came to using, or not using, newfangled calculators in class, the Big Guys are now wrestling with a very similar issue regarding computers: 'Can we trust the darned things?' 'Can we know what we know?' Fascinating stuff."
A computer could quite easier come up with a very complex answer simply because it can do more calculations in a given second than a human can. Of course humans take in a lot more variables at a given time so the numbers are actually very opposite but I'm sure you get my point.
I think you test it with progressively more different problems, if the answers come out precise and accurate then you can build your level of trust in the system. Kind of like the process of getting users to trust saving to the server after a bad crash wiped everything because the previous admin was a moron.20th century mathematics has seen some pretty amazing things, but at the same time, there are very real questions as to what constitutes "proof" any more.
consider this: the hypothesis of the famous Riemann Zeta problem has been tested for trillions of different solutions, and it has held true in every case. (If you want an explanation of the Zeta problem, look elsewhere, I don't have the time)
Now that means that it's *probably* true, but nobody accepts that as mathematical proof.
On the other hand, the classification problem for finite simple groups has been rigorously solved, but the collected proof (done in bits by hundreds of mathematicians working over 30 years) is tens of thousands of pages in many different journals. given the standards of review, it is a virtual certainty that there is an error somewhere in there that hasn't been found. So, again, the solution to this problem is *probably* right, but it has been accepted as solved.
What's the difference between these two cases really? What's the difference between these and relying on computer proofs that are, again, *probably* right?
In this light, the math of the late 19th century and early 20th century was something of a golden age, modern standards of logical rigor were in place, but the big breakthroughs were still using elementary enough techniques that the proofs could be written in only a few pages, and the majority of mathematically literate readers could be expected to follow along. These days proofs run in the hundreds of pages and only a handful of hyper-specialized readers can be expected to understand, much less review them.
In Capitalist America, bank robs you!
Sometimes a precise mathematical analysis can lead to startling insights. Perhaps there are multiple solutions equally optimal. Perhaps it gives a general algorithm that works for other shapes.
Automated theorem provers have been around for a long time, if you can express your thoughts using first order logic. Here's a program from 1986... lisp code
As far as calculator example goes, I believe a person should understand the fundamentals before using the calculator. Don't give a power tool to a kid. Somebody with an understanding of the fundamentals can wield the tool correctly and wisely whereas some cowboy is just dangerous. The old saying comes to mind "know just enough to be dangerous". As far as those oranges in the article, well somebody had better figure out a way to confirm the computer answer, without having to go through the exact same meticulous steps. Don't put your trust in technology without the proof to back it up, because technology built by people is prone to error. Now I'm sure the orange problem won't cause harm to anybody, however I hope I never read such an article about a nuclear power plant!
Change the title to: "Are Computers Able to Verify Mathematical Proofs Beyond All Doubt?"
Though Dr. Hoare danced around that question a little, presumably that aspect of the project would have to be done by hand, a monumental task to say the least.
-
My father sent this to me first thing this morning. I told him that I didn't think that rigorous mathematical proofs should be based on software either in whole or in part. All software of any complexity is inherently buggy. That doesn't mean that rigorous mathematical proofs are flawless by nature. That's why they have peer review. But peer review on software still isn't always sufficient.
Another issue is that you're then excluding any mathematicians who aren't also fairly adept programmers, from really understanding your proof.
All of this said, computers are necessary to do math these days and I think mathematicians should make use of them. I just don't believe we've reached a level of maturity in software development that meets the stringent requirements of mathematical proofs.
Another post mentioned that computers could come up with the proofs but it would be too hard for a human to verify. At what point can be start to both trust the output and to build upon that trusted output by further trusting future output. It could be an interesting time in which we don't understand how things are done but we are able to do them none the less. It all comes down to the question, how much do you want to trust a machine?
involved, not complicated - like the Four Color [Conjecture]. Noone could figure out a way to actually prove it, so some one (or group of someones) wrote a program to systematically determine all the possible arrangements of regions in a simplified series of maps, and then figure out how to color each of those maps. The involved part was .. well, all of it. It wasn't necessarily very complicated, just labor-intensive. Computers are perfectly suited for tedium.
Read; Write; Execute
Prior to september 11, that attitude meant his days were numbered. After september 11, that attitude shows he's in charge.
Sometimes it is enough to know that something is *true* or *false* without having to know the details of the in-between steps.
I'll give some trivial examples to illustrate:
For a famous example, it would provide a great deal of peace of mind if we could prove that P != NP. It wouldn't matter that we understand that proof so much as that it is *provably true*. If, on the other hand, it is proven false that is just as important (if not more so) and while an understanding of the proof might lead more easily to examples of such, we would know (for certain) that trusting public key encryption over the long run would be a Bad Idea(TM) (for example) and that it is just a matter of time before a polynomial time algorithm is developed.
(Not that such will necessarily be fast, mind you, but we would know it would exist).
For another example--there are certain things that can be inferred if Poincare Conjecture is true for N=3. If we can prove the Poincare Conjecture is true (and it is now thought that it might be) it means things to physicists, even if we don't know why it is true.
The bigger question here is "can we trust it if we can't verify it by hand."
Integrate Keynote and LaTeX
We trust everyone, Trust but verify. Why should machines be any differnt. If I ask you to do a math problem do I trust you with the correct answer, sure I do, but I still verify. I preform the calculation my self, and allow others to preform the calculation. If we all come up with the same result we most likly have the correct answer. We must be careful not to allow the problem to define the solution method as that allows for us all to preform the same mistakes. Just like the Seti@home and distributed crack peopel found out that not everyone can be trusted that the only thing todo is have many people test the same key space no one should trust only one answer but rather develop consenous
Don't we already have tons of resources devoted to verifying the accuracy of a computing environment? If we verify the logic and accuracy of the computer, much like the axioms of mathematics, cannot we then say that the resulting proof must be valid?
Of course, if it can't be understood by humans, it doesn't really help anything, as one of the main points of proving things is to gain insight into how to prove other things. But wouldn't building the system to proove proofs be itself a different but valuable tool?
The ______ Agenda
You know what? I work for Intel. My company paid 1/2 billion dollars replacing Pentium chips with that bug that nobody would ever notice except maybe six people. Software vendors get away with murder. They don't even have to replace their product even if it is not fit for it's stated purpose. The FDIV bug was a typo in some kind of table. Doesn't that make it software in a way? One little bug years ago and still people laugh about it (SCORE:4, Funny).
once upon a time, only advanced mathematicians knew calculus, but now we learn it in high school. Just wait until warp theory is an entry level college engineering course
Once upon a time, the majority of adult males knew how to trap a rabbit (or similar creature), gut it, skin it, start up a fire, cook it, and eat it.
I don't.
Heck, I couldn't even look up at the sky at night and tell you which way was north.
Once upon a time, most people could.
All I'm saying is that the amount of knowledge and skills the average human being can possess will not increase expontentially over time (barring artificial manipulation). We gain new skills as a population and lose old ones.
Yes. Mathematics is just Symbol Manipulation. And so is science, and poetry, and everything else written.
If you are still trying to learn how to add in calculus class then there are bigger problems.
It is one thing to deride the use of cacluators because they are crutches, it is another thing altogether to deride them because you are a technophobe.
Technology is extremely useful in aiding understanding and exploration of mathematics. If you eliminate calculators and computers in schools, even high schools, you may hurt the chances of your students to succeed in an increasingly technical world.
As usual, I think the correct response is a balanced response. Demonstrate how to use technology as a tool and provide assessment that requires demonstration of ability without the use of a calculator as a crutch.
In a calculus class, for example, divide the exams into two parts, or alternate between calculator allowed, and calculator disallowed exams.
Of course, this has little to nothing to do with the nytimes article but it always seems to come up in these discussions.
plurvert
That's exactly the case. I had Ken Appel as a professor, and he mentioned the 4-color theorem a couple of times. As he put it, the math wasn't intensive, but actually doing the work the computer was able to do would have taken an army of grad. students years to finish. The way he saw it, the proof was understandable, just extraordinarily, arduously long. That's when they decided to use a computer to solve the problem. Unfortunately, there are still many pure mathematicians who shun computer-based proofs because they (or their grad. students) are not working things out with their own pencils. Unfortunately, I don't think that's a problem that's going away, but I do think it opens up some interesting doors such as writing program A to prove a theorem, and then haveing to prove program A's correctness, for which you write program B and so forth.
See the problem is humans can only program a computer to do something the human coding it knows how to thoroughly describe. It is also why you won't see a computer naturally speaking, showing emotions, or doing anything else we cannot describe today.
It is amusing to see computers being used as proof bringers when you usually need a proof to program the darn things.
take A!=A as an axiom, and you have a whole new field in mathematics.
um.... your wrong about that... and alot of people dont understand this either.
... is can we program this truths into a computer... give a program a problem... have it randomly(or not for the ai people) apply some theory.. and get an actual answer?
all of our knowledge is based upon assumptions. For instance when it comes to the number systems... we have a set of assumtions that we say are true.. and there is no arguing about it. For instance in the binary system. We say the language only consists of 0 and 1. We say there are two operators and define there operations. AND/OR... we say 0 and 0 is 0.... we say 1 and 1 is one. There is NO PROOFING THIS... its a given. We can PROOF things like demorgans therom.
This applies to many many areas... geometry... algebra.. calc... logic... etc. There are a list of assumptions that are given to be true. You could argue that calc is just an extention of algebra and geometry... but thats another matter.
The question I think this article is asking
In my own personal opinion, I think this would work. I think if you took it far enough.. giving information about math... chemistry and physics and electronics.... I think it would be possible to have a computer design a better computer.
Selling software wont make you money, selling a service will.
What you've done is shown that for a subset of the sets of oranges and a subset of the sets of stacks the pyramid is better.
A mathematical proof shows something is true for every single element of the sets.
because we have no way of KNOWING if the computer has built up the proof correctly, except that it says it has
Sure we do -- typical theorem provers spit out a proof that can be checked by hand (god forbid), or else checked by a simple procedure. Understanding that a theorem prover is implemented correctly is tough, but understanding that a checker is implemented correctly isn't. I trust such proofs more than I trust hand-checked proofs, because humans are more susceptible to mistakes than computers are.
Most people probably knew the "four quadrants of knowledge" thing, but didn't know they knew (DK). That is, they have enough to put it together, but have probably never put it into words before. Intuitive knowledge is one way of putting it. The bulk of most people's knowledge probably falls into this category, which is fine - language is often overrated as a conduit of knowledge (not that it's not incredibly useful and important, but other means exist and are constantly used).
;)
I don't actually believe particularly firmly in that model, though, because I don't agree with the D-K dichotomy that underlies it. It's your usual classical Greek quadrant, which means it springs from a dual dichotomy, or in this case a dual-aspect single one. Dichotomy (or even one-dimensional spectra) is not the only way to look at things, but it is a dangerously compelling model - that is, when people have been presented with a dichotomy, they typically become unable to consider without it. And the defence of a dichotomy is usually a tautology - I mean it's obvious, isn't it, you either know something or you don't?
Still useful and interesting if you can get it out of your head when needed, though.
'Can we trust the darned things?' 'Can we know what we know?'
It's not an issue of can we trust them, at least not in general. (We won't go into the question of current machines - I'll agree they're generally not there for rigorous proofs.) We're going to have to either trust some form of computation aid in proof work, or throw up our hands and abandon the field - the human brain and lifespan impose definite limits beyond which we cannot go without aid, and since I can't think of any limit human beings have willingly accepted as a group somehow I doubt this will be the first. So, instead, the question should be
"How do we create computers we can trust?"
If that is impossible, then that's it. Mathematics will be come like experimental high energy physics - 20 years effort by 100s of people to achieve one result. But I'm not ready to concede that its impossible. I know it is provable that computers can't solve all problems in general, but the same proof indicates humans can't either. The question I'm curious about is whether the behavior of a computer is too general to be attacked by useful proof methods. Most actions taken with a computer assume a definite action and a definite outcome (spreadsheets and databases, for example, do not do novel calculations but perform the same operations on well defined data.) Mathematical proof is a different question, but the ultimate question is whether a properly designed and built computer (i.e. built as rigorously as possible in a technical and algorithmic sense) would be completely unable to handle problems that are interesting to human beings in the proof field. That is a completely different question from generality statements, and from the standpoint as computers as a trustworthy tool I think it is the more interesting one.
"I object to doing things that computers can do." -- Olin Shivers, lispers.org
The question should not be whether computers can calcualte flawlessly - that's obviously wrong. The question is whether the probability of all the different configurations of computers consistently giving the same wrong answer to a problem is greater than the probability of all the human mathematicians agreeing on the same wrong answer. To me, it seems obvious that the computers are better off...
Insightful up to the last paragraph. Sure I can only learn so much (knowledge and skills). Becoming good at playing the guitar means a trade off, and perhaps by making that choice you don't learn to skin rabbits, fly airplanes, and so on. Yet some have done several of the above. There is enough knowledge that you cannot learn it all. As a population we do not lose old skills, at least not near as often as we learn new ones.
Some things take years to learn, some take minutes to learn and years to master, and some take just minutes to learn. Some are worth teaching everyone (reading for example), some are worth learning despite no practical use (playing guitar for example), and some are hobbies that a few people learn for the fun of it (skinning rabbits). Few skills are lost over time though, and now that reading is universal less are lost because those who know can write down for latter use.
Look around and you will find a few people who can tat, make chain mail, build a bark canoe and so on. All useless skills in this modern world, but kept alive because someone made it their hobby. I've seen books on all of the above, and many more.
If the doom sayers worst perdictions come true and you are one of the few people to survive [whichever disaster is in vogue today] you can go to a library and get books for the skills you need. Find someone to have kids with, and you are likely to pass reading and simple math onto them, and they to their kids. Eventually civilization will return with population, and your many times great grandkids will have an advantage in that they can read our books to tell them what works so they don't make the mistakes we did.
There was a young man who said, "though
it seems that I know that I know,
what I would like to see
is the I that sees me,
when I know that I know that I know."
Great poem, Alan Watts used to quote it alot when talking about the illusion of the ego.
"It is not how things are in the world that is mystical, but that it exists." -Ludwig Wittgenstein
"On two occasions, I have been asked [by members of Parliament], 'Pray, Mr. Babbage, if you put into the machine wrong figures, will the right answers come out?' I am not able to rightly apprehend the kind of confusion of ideas that could provoke such a question."
-- Charles Babbage (1791-1871)
Computers only do what they are told (excepting "hardware failure", which is not the topic).
Shouldn't the validity of computational proofs be able to be determined by proving the meta-logic of the solver?
i.e. proving that a strategy for finding a proof is valid (and therefore trusting its results).
Maybe those wary mathematicians are just unaccustomed to working on a problem meta-logically, and prefer to find proofs directly themselves (with the meta-logic being defined solely within their own minds)?
In such cases, perhaps peer review should not require human verification of a computational proof, but rather another independent meta-logically valid computational proof?
Simple. The student should know the value of pi to a certain number of significant figures.
Why? Einstein was once asked how many digits of Pi he could remember. He replied "maybe three or four". The interviewer then exclaimed: "But Sir, some people have memorized hundreds of digits!" Einstein's reply was: "Ah, but I know where to look them up if I need them."
With a calculator, they're just typing in 3*pi and getting an answer with 8+ significant digits. Without a calculator, they're actually calculating the answer as close as they can based on how many significant digits they know.
Wrong, wrong, wrong. If the answer to some problem is 9 Pi then the answer to that problem is 9 Pi, not 28.274333882308139146163790449516.
That's a better test of who's mastering mathematics.
Memorizing Pi and doing multiplication on paper has almost no relevance at all to "mastering mathematics".
The mathematical literature is full of errors, oversights, invalid proofs, unstated assumptions, and probably even a certain share of deliberate fraud. See Lounesto's misconceptions of research mathematicians for one expert digging into the mathematical literature.
Computers are far better at ferretting out oversights, missing assumptions, and making sure that every t is crossed and i is dotted. If a software system for doing proofs has shown itself to be fairly reliable on a bunch of samples, I'd trust it a lot more than I'd trust any working mathematician to carry out a complex proof correctly.
People attempting the proofs are no less vulnerable to making mistakes than those who wrote computer software to develop the proofs. Thus a system to verify the proofs should be in place for both groups of people. Any person working on a doctoral discertation will have their work reviewed by a board. Any proof generated by a computer shout too be reviewed by a board before it can be considered correct. I don't see where the issue is.
Kent Simon Multitheft Auto