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."
> 'Can we know what we know?' Fascinating stuff.
Reminds me of Rumsfeld... "Reports that say that something hasn't happened are always interesting to me, because as we know, there are known knowns; there are things we know we know. We also know there are known unknowns; that is to say we know there are some things we do not know. But there are also unknown unknowns -- the ones we don't know we don't know."
...precisely why it's so hard to see that a pyramid of cannonballs is an optimal stack? This seems almost axiomatic.
I guess the obvious Monte Carlo simulation doesn't constitute "proof," but still, what exactly is the big question here?
The headline does a slight disservice in describing the article that way: Whether or not computers can create proofs isn't an issue. The problem comes when the resulting proof is too involved to be verified by a human, and so the computer's work has to be trusted.
Depends whether it's a Pentium with an FDIV bug, I imagine...
--
Don't like it? Respond with words, not karma.
I think the issue will become: can we learn anything on our own, we don't want to rely on imposibly long proofs. My calc teacher hates us using calculators, she thinks it will be the end of calculus as we know it.
I mean, we've used computers to prove much of boolean and linear algebra. The most famed result in the field is that of the Robbins Conjecture, proven entirely by computer. The computer produced a very "inhuman" proof...
and there are already programs out that help with this. Here's one for example...
When the results become too inaccurate then you have to change your tools, so unless accuracy is key, such as NASA's calculations and the likes then you work on making a computer do as much as possible to eliminate human error and humans can be there to adjust the almost mythic fudge factor
In Math, Computers Don't Lie. Or Do They?
By KENNETH CHANG
Published: April 6, 2004
leading mathematics journal has finally accepted that one of the longest-standing problems in the field -- the most efficient way to pack oranges -- has been conclusively solved.
That is, if you believe a computer.
The answer is what experts -- and grocers -- have long suspected: stacked as a pyramid. That allows each layer of oranges to sit lower, in the hollows of the layer below, and take up less space than if the oranges sat directly on top of each other.
While that appeared to be the correct answer, no one offered a convincing mathematical proof until 1998 -- and even then people were not entirely convinced.
For six years, mathematicians have pored over hundreds of pages of a paper by Dr. Thomas C. Hales, a professor of mathematics at the University of Pittsburgh.
But Dr. Hales's proof of the problem, known as the Kepler Conjecture, hinges on a complex series of computer calculations, too many and too tedious for mathematicians reviewing his paper to check by hand.
Believing it thus, at some level, requires faith that the computer performed the calculations flawlessly, without any programming bugs. For a field that trades in dispassionate logic and supposedly unambiguous truths and falsehoods, that is an uncomfortably gray in-between.
Because of the ambiguities, the journal, the prestigious Annals of Mathematics, has decided to publish only the theoretical parts of the proof, which have been checked in the traditional manner. A more specialized journal, Discrete and Computational Geometry, will publish the computer sections.
The decision represents a compromise between wholehearted acceptance and rejection of the computer techniques that are becoming more common in mathematics.
The debate over computer-assisted proofs is the high-end version of arguments over using calculators in math classes -- whether technology spurs greater achievements by speeding rote calculations or deprives people of fundamentals.
"I don't like them, because you sort of don't feel you understand what's going on," said Dr. John H. Conway, a math professor at Princeton. But other mathematicians see a major boon: just as the computers of today can beat the grand masters of chess, the computers of tomorrow may be able to discover proofs that have eluded the grandest of mathematicians.
The packing problem dates at least to the 1590's, when Sir Walter Raleigh, stocking his ship for an expedition, wondered if there was a quick way to calculate the number of cannonballs in a stack based on its height. His assistant, Thomas Harriot, came up with the requested equation.
Years later, Harriot mentioned the problem to Johannes Kepler, the astronomer who had deduced the movement of planets. Kepler concluded that the pyramid was most efficient. (An alternative arrangement, with each layer of spheres laid out in a honeycomb pattern, is equally efficient, but not better.) But Kepler offered no proof.
A rigorous proof, a notion first set forth by Euclid around 300 B.C., is a progression of logic, starting from assumptions and arriving at a conclusion. If the chain is correct, the proof is true. If not, it is wrong.
But a proof is sometimes a fuzzy concept, subject to whim and personality. Almost no published proof contains every step; there are just too many.
The Kepler Conjecture is also not the first proof to rely on computers. In 1976, Dr. Wolfgang Haken and Dr. Kenneth Appel of the University of Illinois used computer calculations in a proof of the four-color theorem, which states that any map needs only four colors to ensure that no adjacent regions are the same color.
The work was published -- and mathematicians began finding mistakes in it. In each case, Dr. Haken and Dr. Appel quickly fixed the error. But, "To many mathematicians, this left a very bad taste," said Dr. Robert D. MacPherson, an Annals editor.,
To a
Computers are a human creation...it's not a matter of whether we can trust the computer, but rather a matter of can we trust that the people who built the computer and coded the software it runs knew what they were doing and didn't make any errors. Computers can only do what we tell them to...so really it was humans who indirectly made the proofs by producing a system capable of doing so. All it really boils down to is whether the folks who made the system and it's software knew what they were doing or not and whether they made any errors or not.
no.
q.e.d.
-
ping -f 255.255.255.255 # if only
Theorem provers have been around for a long time. A net search should turn up a ton of hits. The key is to implement a system that can be verified by hand, and then build on it.
(S(SKK)(SKK))(S(SKK)(SKK))
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!
???
BOOM!
"Cleanup in aisle 10"
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!
The question is whether the people setting up to create mathematical proof are ready themselves?
So many times I see people use programs like MAPLE to show something mathematical, and it ends up a disaster.
Problems is the brain on the chair, not brain on machine.
I don't see what the big deal is; not only is the general problem of proving mathematical statements undecidable (even without considering Godel's theorem) but even solvable problems require a lot of human intervention to get solved. Most problems (ie - examples out of math textbooks) aren't going to come up with a proof in any reasonable amount of time by simply dropping it into a theorem prover and pushing "go".
"Automated theorem proving" is less an automatic process (like you'd get with an automated production line) and more of a mechanical assistance to the job (like using a fork-lift to move heavy things faster than you could by hand).
It not only takes work to convert a problem into a good representation, but then you have to structure the problem statement in such a way that a theorem prover can make optimal use of it. Often times, you're forced to, upon following the output, prove lemmas (sub-proofs).
Then, when you finally get a proof, you get the joy of trying to simplify it to something that -can- be understood by a person; again, this is part of the process that can't really be automated well.
my sig's at the bottom of the page.
Change the title to: "Are Computers Able to Verify Mathematical Proofs Beyond All Doubt?"
Doesn't the Godel incompleteness theorem say they can't?
The answer is left as an exercise for the reader.
That's ok, Jesus likes me anyway.
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.
-
Mathematics is just Symbol Manipulation. I suspect computers are pretty good at that.
;)
Also, chess is just Pattern Matching... I don't know if humans have the edge there or not.
http://www.nytimes.com/2004/04/06/science/06MATH.h tml regfree link
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.
..if you can prove the program. I know that a lot of people look down on axiomatic semantics and model checkers; but I also know some people that started in that area a long time ago that still believe in it, and even more that are trying to get faculty appointments out of this rebounding field. If you can prove a program does what you expect it to and it, it turn, can be shown to prove what you really wanted, I don't see the problem. Maybe some of our theoretical mathematicians just need a dose of practical computer science.
The obvious solution is to have the computer create a new proof that shows that the algorithm it used to create the original proof is, in fact correct.
A marriage is always made up of two people who are prepared to swear that only the other one snores.
This story and this issue are not about whether or not the mathematical community trusts a computer created proof. The issue is whether or not the community can trust the human behind the computer to create a computer program/system that is "flawless enough". Issues and bugs may arise, and the community can't trust that these issues will 1. be found and 2. be severe enough to affect the validity of the proof.
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?
The problem with computer generated proofs is that in order to trust the result of the computer, you have to trust:
And of course, our understanding of the hardware depends on how accurate our understanding of the laws of physics is. Any mistake in either the source code, compiler, or hardware, and potentially the proof produced is incorrect. That's an awful amount of stuff you have to check just to make absolutely sure the computer is correct. Then, consider how many bug-free pieces of software you've encountered. ... Yeah, I can see why mathematicians would not trust computer generated proofs.
Of course, people are not infallible either, but that's well known and expected. It's all about how much uncertainty people are willing to accept.
as a graduate in the fields of mathematics, i spent a large portion of my five undergraduate years doing proofs. there are a great many ways to prove things, sometimes applicable sometimes not. (e.g. using inductive proofs for numeric theorems is all well and good but completely useless for any sort of ring-theory or spatial proofs)
there are also several levels of depth for proofs, ranging from "i've found a counter example so i can write the whole thing off as garbage" to "i have exhaustively and rigorously proved this starting with the basic axioms of number theory and worked my way on up"
the latter is really the only acceptable way to prove anything seriously. sometimes when you are reworking an already- done proof to illustrate a point, other mathematicians will allow a bit of latitude when it comes to cutting corners, but for a proof as far-reaching as the one in the article, i would only be interested in a "rigorous" proof, that is, one that started with the foundational tenets of mathematics and combined those to form and prove other postulates, etc. very much a form of abstraction, not unlike large development projects.
the problem arises when one (or several) humans have to be able to objectively check the whole thing. to use my prior example of a large development project, no one developer at microsoft understand the whole of windows. it's too big for a single human to understand. each developer knows what he needs to do to complete his part, and so on and so forth.
traditionally, for proofs, a single mathematician (or a small group) would hammer out the whole proof, so the level of complexity remained at a human-understandable level. (even if tedious) my concern, as a mathematician, with using an automated solution would be the rapidly growing order of complexity needed to properly back up increasingly complex proofs. as stated in the article, it's like trying to proofread a phonebook. (only, you must also consider that for every element of the proof (a particular listing) there are several branching layers of complexity (fundamental, underlying proofs many layers deep) underneath. this gets more complicated in an exponential fashion) obviously this approach will only remain human-checkable for relatively small problems. (programmers: think of some horrible nondeterministic- polynomial problem like the "traveling salesman" problem. systems, like humans, are a finite resource, but if you increase the size of the problem, the complexity will quickly grow far beyond your ability to compute. large proofs suffer from the same difficulties, if not quite as concrete and pronounced as NP algorithms)
in closing, i would have to agree that proofs, no matter the effort and computing time put into them, really should not be viewed as being as rigorous as those provable "by hand" and human- understandable, even if the computer has arrived at a satisfactory conclusion, because we have no way of KNOWING if the computer has built up the proof correctly, except that it says it has.
In Soviet Russia jokes are formulaic and decidedly non-humorous.
I think the "as we know it" is the key word here. It creates a new juggling act that teachers have to deal with. On one hand, calculators are extremely useful for the things at which humans are error prone. If students can use calculators or Mathematica or something, they can check their arithmetic much more reliably, which is great for isolating problems with learning concepts from basic mathematical errors. Granted, some people don't see this as a bonus since it's good to be able to do arithmetic reliably without aid. For smaller numbers I agree, but in the real world people use calculators for arithmetic with numbers that have a lot of sig figs. Making students do this arithmetic by hand is just distracting them from learning the concepts they are supposed to be learning.
On the other hand, many students are prone to using these devices and applications as crutches and try to get away with doing things like using their calculator's implementation of Newton's Method instead of solving the problem themselves.
Some professors have found solutions to this problem, others havent. When I was at college, I think our math department had achieved a pretty good level of harmony with Mathematica - we were expected to do a lot of stuff by hand or in our heads - Gaussian elimination, for example - but in order to make the math seem useful, we were also exptected to be able to solve real-world problems with the stuff we learned. Not contrived "real-world" problems from your high-school textbook, but stuff like interpreting large and dirty scientific datasets where the specific technique we would have to use to solve the problem was something we could figure out, but not something that had been explicitly laid out by the textbook or in lecture. We had to apply the concepts we had learned to figure out the problem, but there was no way we were going to chug out that arithmetic by hand - when was the last time you tried to work on a 16x16 matrix using a pencil and paper? How about a 100x100 one?
Mathematics is one of the most intensely human of human endeavours. Everything in it is a production of the human mind entirely. Yes, the real world can sometime lead us into an interesting area of inquiry, but at its core the uncoverings of truth from axioms is a human endeavour.
A computer can be a useful tool (I'll be doing computational graph theory this summer), but it is not human. It does not have the ability to hold the possiblities of ideal forms within it and understand. It does not think.
The use of numeric methods to solve applied problems, or symbolic methods to pure problems is good and useful, but it does not constitute proof.
A human being, given an understanding of the underlying mathematics, must be able to go through the proof step by step, and see that, from the givens, the conclusion is inevitable.
I don't accept the Four-Colour theorem as proven true. I strongly suspect it to be so, but my suspicion does not truth make.
The Riemann hypothesis, on the other hand, is much, much further from being proved then the Four-Colour Theorem. Yes, millions of zeroes have been checked...but there are infinitely many zeroes, and all it takes for it to be false is for ONE of those zeroes to fall off the Re=1/2 part of the complex plane.
If I were giving odds, then millions divided by infinity is awfully close to zero.
Insanity is contagious. - Yossarian
I professor showed me the Robbins Algebra proof a while ago. I was going to link here, but first I searched the page for (Score:5, Informative), and there you were :)
Here's an excerpt:
In 1933, E. V. Huntington presented [1,2] the following basis for Boolean algebra:
x + y = y + x. [commutativity]
(x + y) + z = x + (y + z). [associativity]
n(n(x) + y) + n(n(x) + n(y)) = x. [Huntington equation]
Shortly thereafter, Herbert Robbins conjectured that the Huntington equation can be replaced with a simpler one [5]:
n(n(x + y) + n(x + n(y))) = x. [Robbins equation]
Robbins and Huntington could not find a proof. The theorem was proved automatically by EQP, a theorem proving program developed at Argonne National Laboratory.
PUBLIC SPLIT ON WHETHER BUSH IS A DIVIDER -CNN scrolling banner, 10/15/2004
Come on, this is just comparing Appels and oranges
No matter what the proof, don't we still have to accept blindly on faith that A=A?
Sure, it seems highly probable but.. I just.. I guess I'm a skeptic. All of logic seems like a joke to me, as long as this one little potentially huge loophole looms in the background...
Spoon not. Fork, or fork not. There is no spoon.
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.
Here's a link to the Flyspeck Project, briefly mentioned at the end of the article, which aims to give a formal proof of the theorem.
"I don't know, a proof is a proof. What kind of a proof is a proof? A proof is a proof and when you have a good proof it's because it's proven."
(PM Jean Chretien, when asked what kind of proof he would need of weapons of mass destruction in Iraq before deciding to send Canadians along on the Bush invasion-September 5th on CTV news)
What strange timing -- I just saw a talk this morning from Hales at CMU about his work on formalizing the Kepler conjecture ("theorem") in HOL Light.
I can understand not wanting to trust a big piece of C code that purports to check a huge number of cases of a proof doing numerical analysis. It took 6 years of 4 people trying to verify his computer proof of the Kepler conjecture--before they gave up. If a program is that hard to believe, then it does indeed deserve lesser status than a handwritten proof that can be checked by mathematicians in shorter time.
On the other hand, there are other computer tools that we really should trust, and that are revolutionizing mathematics. The idea is simple: write your proofs in such detail that they can be mechanically checked by a simple (easy to verify) procedure. This is much better than paper proofs, because the potential for human error is minimized. (I don't think anyone will argue that published proofs have often been wrong, and the proofs have not been caught by the peer reviewers!) Since it's really, really bad to believe wrong proofs, there's a very real benefit that is offset by the sometimes tedious work necessary in formalization.
That's what Tom Hales is doing with flyspeck, and I think it is the future of mathematics. (In fact, I have recently become addicted to mechanizing my own proofs in Twelf--it's not only immensely satisfying, but it helps me sleep better at night and makes for stronger papers.)
I know I am splitting hairs (but who isn't in this kind of discussion), but I can't wrap around my head around the difference DK and DD to the person in question .
:P.
What i mean is,effectively not knowing you know something is the same as not knowing you don't know something, since you are ignorant of it anyway. Of course, one can remind me that I know something, (e.g. "You idiot! That's just the Laplace-Beltrami operator you learned in class!"), but then to me I am now KK, not DK.
Maybe DK is just a very confusing way of saying "forgot for a moment".
Ok, my head is spinning again. Maybe the hairs are too fine to split anyway
Mode (3) smart-aleck mode. Press * to return to main menu.
Godel, Escher, Bach: an Eternal Golden Braid
I am only half way through it, and it handles this topic far more gracefully than the original article. Very entertaining if you happen to be a math, music, or art geek. Strange mix, but Douglas Hofstadter really nailed it.
www.jmagar.com
-
'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
Perhaps I'm missing something here, but I think the approach of verifying the validity of the proofs that come out of the kind of system described in the article is fundamentally the wrong approach.
Instead, mathematicians ought to focus on formally proving the proof generator. If it could be fomally proved that the proof generator only generated valid proofs, we could automatically trust all the proofs that it generated. Program proof and verification is a complex topic, but it's a quickly maturing area of CS.
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.
For some cases of proof solving, a human is often behind the scenes, and has reduced the number of cases that a computer has to check from infinity to say 10^25 or some other large, but finite number.
Computers nowadays can handle symbolic calculations and prove identities and likewise, but for identifying what is interesting to have proved or not, a human may still be there with interpreting that, no matter how sophisticated computers or software can get...
The people at the Risc Institute are creating cool stuff like Theorema, which helps in automatically proofing things. Some of these people teach math at a university in Hagenberg where I got the chance to see this thing in action, it is really amazing how well this works.
Open Source Alternatives
About 20 years ago, I worked for a company near Boston, and played in a co-ed softball league made up of teams from other companies in the area. One of the teams had an extremely attractive third basewoman, who was also quite friendly, which I discovered during a game where I had actually made it to third base. At the beer hall we went to after the games, I asked her what she did; she told me she was the head of Q&A for a product that would supposedly produce provably correct programs. You used some kind of GUI to draw something like a flowchart, typed in a few constraints, and then clicked on a button, and out would come bug-free code (in Fortran or something). "Sounds cool" I said, but she laughed and said that the development team had been having a really hard time getting the bugs out of the tool's parser. For the next few weeks, the joke was about the shortsightedness of her company's management - "Why don't they just do the obvious thing, and use their tool to generate the code for the parser?". They never were able to get all the bugs out, and went out of business a short time later.
"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?
Hm. I always thought that Godels theory actually goes further than "There is no proof for this statement.".
We know that given any collection of nontrivial axioms there will always be a statement that is consistent with all axioms and valid proofs that cannot be prooved or disprooved within that set of axioms. In other words, no matter how many axioms we select no nontrivial mathematical system with a finite number of axioms is complete. Secondly, as you said there are mathematical constructs that can not be proved or disproved, and so it is impossible to show that all existing proofs are consistent with the chosen axioms.
"As a writer / novelist you might want to spellcheck your sig.
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