Slashdot Mirror
Software Is Starting To Aid Mathematical Proofs
An anonymous reader writes "Mathematical proofs are supposed to establish absolute certainty, since each statement is a pure deduction from fundamental axioms. But the reality is that mathematicians make mistakes. Proof-validation software can do what mathematicians never do: spell out every last step, making sure everything is right. Such software has been around for 20 years, but mathematicians and computer scientists now say they are nearing the point where every mathematician will routinely use the software before submitting a new result to a journal, producing a fully correct, formal, axiomatized mathematics."
Let's see it prove I am not a chair ;-)
Table-ized A.I.
Simple:
A. You are a nerd
B. Your wife wants a life
C. If a woman gets no life, she becomes a bitch
D. Nerds have no life
A + B + C + D -> Your wife is a bitch
Next!
Table-ized A.I.
You need to write this in the right way.
Theorem 1: Your wife is a bitch.
Lemma 2: All woman wants a life. (Assume proved elsewhere)
Lemma 3: If a woman gets no life, she becomes a bitch. (Assume proved elsewhere)
Definition 4: Assume you are a male nerd.
Lemma 5: Nerds have no life. (Assume proved elsewhere)
Proof of Theorem 1: Base on the results of Lemma 2 and 5, woman who are married to male nerd have no life. Therefore by Lemma 3, woman who are married to a nerd becomes a bitch.
Q.E.D.
New Economic Perspectives
if the proof-verifying-algorithm is polynomially verifiable.
For what it's worth, I've had good experiences with coq: http://coq.inria.fr/ Although I've never used it for anything large, it has the nice ability to make proofs about code, and export the code to haskell, scheme, or ML. I had a fun time proving that the min function always returns the lesser of the two values.
If only there was a computerized dupe prover.
Get a wife
You just got troll'd!
A. Your logic is weak
B. Earthworms are weak
C. Logic resides inside your head
A + B + C -> Your head is infested with earthworms!
You just got troll'd!
Wait.. I don't get it myself...
You just got troll'd!
All of those are for computation, not generating or checking proof.
Yep. I guess the AC who submitted the story didn't quite RTFA, since TFA mentions the 1976 proof of the four color theorem. TFA doesn't say that proof checking software is new, just that it is gaining in popularity.
One photo is worth a thousand proofs:
http://greggsutter.com/mt/archives/manWomanControlPanel.jpg
Tag lost or not installed.
Kick XFig to the curb, and learn PSTricks. Or, if you're doing algebra, use XYMatrix.
"Oops. I broke it." -- Godel
Not quite. Every sufficiently complicated formal system is limited by Goedel's incompleteness theorem. (Emphasis added.) Although IANAMathmatician, I've always understood that what makes Arithmetic complicated enough for the theorem to apply is the inclusion of infinity. As computers can't really handle infinity (just numbers outside their range) I don't know if they're complicated enough. If anybody does know, I'd appreciate an answer.
Good, inexpensive web hosting
what makes Arithmetic complicated enough for the theorem to apply is the inclusion of infinity.
Some answers, but first, hang on! What do you mean "what makes Arithmetic complicated ... is the inclusion of infinity?" Anyway, What Godel tells you is that if you have any system which is strong enough, ie., satisfies the Peano Axioms, then indeed, incompleteness applies. I suspect that by what you mean by "inclusion of infinity" is that collection of all natural numbers is a set?
In proving this (it's been a while since I looked at the proof), you don't really need the natural numbers to be a "set", because you can construct the Godel sentence in logic. The quantification is over the natural numbers, but I think that it's okay for it to be a proper class. But don't quote me.
As computers can't really handle infinity (just numbers outside their range) I don't know if they're complicated enough. If anybody does know, I'd appreciate an answer.
When checking proofs, you don't need to have computers explicitly handle infinity. The very idea of "proof" is that it takes you from the theorems you've proved so far, to the statement you're trying to prove, in a finite number of steps. Most mathematicians don't write out every line of a proof explicitly, so this is a very important purpose of proof checkers - to be able to formalise every step of the proof. There are a few things. Although the most common set of Axioms used for Mathematics (Zermelo-Frankel Axioms + Axiom of Choice or BNF if you want to do Category Theory) actually has infinitely many axioms, you can write them down as finite number of sentences in logic. So certainly, you can equip your program with that. Ie., you can give you computer "knowledge" of these axioms. Then we bootstrap. The first step would be to prove all the basic theorems of your favourite set theory. Then you keep adding results that are positively proved by the system, increasing the complexity of your genome. You can enter more and more results. In effect, your prover becomes a huge database of theorems. In most cases (which probably doesn't mimic the way the Four Colour Theorem was proven) the idea is that the mathematicians go off and produce a proof. So, you have good belief that the proof works, so what you really have is an outline. You really should be able to enter the outline of the proof into the computer, and it should be able to formalise and fill in the details, and actually verify the proof is correct. In any case, everything here happens in a finite number of steps. So there's no issue about computers being unable to handle infinity. I mean, we really can't either, otherwise, it would have been simply possible to check Fermat's Last Theorem for every n... Hope this helps!
Many years ago, I was talking about this with a friend with a degree in Math, who'd actually studied this. He told me that, as an example, the arithmetic of all integers between zero and one million, inclusive, would not be sufficiently complex. I don't remember if he explicitly said that any system that couldn't take infinity into account wasn't enough for Goedel's theorem to apply, but that's the impression I came away with.
So there's no issue about computers being unable to handle infinity. I mean, we really can't either, otherwise, it would have been simply possible to check Fermat's Last Theorem for every n... Hope this helps!
Yes, and no. I didn't mean that we can handle infinity in the sense that computers can handle floating point numbers. I meant that the Arithmetic of Natural Numbers can express any finite integer, and that the concept of infinity is part of our tool box, if you will. Again, I'm writing as a layman, so my understanding may, and probably is as incomplete as math itself.
Good, inexpensive web hosting
So now that we have software that can extensively check proofs, what's next? I don't think it's too far-fetched to someday expect programs that can construct a proof from a given statement. I imagine some sort of approach where axioms are manipulated to reach a desired conclusion either through blind or guided permutations, or even the beginnings of coded innovation. Considering how logical and orderly mathematics is, could discoveries be left to computers while humans are forced to specialize in adapting mathematical models to solve problems?
To address the title first:
There is experimental Mathematics that uses programs to search problems for "interesting features." Then one can take pencil to paper to look into that specific area of the "problem." You know, to actually prove something. Software can also be used to search for counter-examples to conjectures or look for evidence that a conjecture is true or not. So, in that way, software does aid Maths. As in, software can be used to search for "things" or to be used as a "microscope." It's been like this for some time.
But, most people don't actually understand what Mathematics actually is. Hell, even in Applied Mathematics, one must actually prove something. But, that proof, and here is where the misunderstanding comes in, is not an exhaustive search nor similar. That is a "show." Proving something is very different. Proving something not only gets you to a conclusion, but you learn something a long the way. The proof always points to "other things." A "show" doesn't provide this.
Now to answer what was written in the post:
These "proof checkers" are, to put it politely, a misnomer. I find it sad that people actually think that they will work as advertised. First off, if anyone would actually look at the "code" that is needed to be entered in (at least) many of these "proof checkers" they'd realise just how problematic data entry will be. Not to mention the... numerous bugs that WILL be in the compiler and checker itself. Not to mention the impossible requirement for a zero defect environment. I could go on.
But, there are also many other concerns that make this a practical fools errand. Namely, how do you translate something like, "A sufficiently well behaved function" (no that's not ad hoc, it quite rigorous within context), or "We take (37) and proceed by parts which results in:", etc, etc, etc. To accommodate this, the proof checker will either need someone to manually code every last detail expanding details as needed, something that is intractable, or AI that is, more than likely, more than a century more advanced than what we have today.
I'll also point out that we already have a formal, axiomatized, correct Mathematics. The only problems with correctness that come up are recent results and those are typically found quickly. It's called a retraction and it happens regularly. As in, the Mathematics community already has facilities to accommodate for incorrectness in published solutions. Lets not blow everything out of proportion because some clowns with nothing better to do with there time think otherwise.
In all honesty, how many of these fallacious stories are going to be published here? Because, this has been a repeated topic over the past couple weeks. Or does /. have the same technique as FOX "News"; say it enough times and it /becomes/ true?
Many years ago, I was talking about this with a friend with a degree in Math, who'd actually studied this. He told me that, as an example, the arithmetic of all integers between zero and one million, inclusive, would not be sufficiently complex. I don't remember if he explicitly said that any system that couldn't take infinity into account wasn't enough for Goedel's theorem to apply, but that's the impression I came away with.
Yes, he's correct in this. If you have a system which only contains integers 0 to n, then that doesn't satisfy the Peano axioms.
Yes, and no. I didn't mean that we can handle infinity in the sense that computers can handle floating point numbers. I meant that the Arithmetic of Natural Numbers can express any finite integer, and that the concept of infinity is part of our tool box, if you will. Again, I'm writing as a layman, so my understanding may, and probably is as incomplete as math itself.
Infinity isn't a concept in mathematics, it is what we call an entire class of sets. If a set S cannot be put into a one-one correspondence with a finite number (a number itself is a set), then we say that S is infinite. The existence of such sets is given by the "Axiom of Infinity." This is all just a part of the formalisation of Set theory. Such a formalisation is simply a set of "beliefs." A theorem prover is simply an AI which has the axioms (or synonomously the beliefs) of set theory at it's core. What I'm trying to get at is that there is no difference in the way we produce proofs compared to a computer. Just as we can never truly realise an infinite process (because we'll be going on forever), we can formalise it, and then prove results about. The point is that a theorem prover is given knowledge that "infinity" exists, because at the core, all you have is a set of beliefs, and your proofs are simply formal derivations from those beliefs. In actual fact, the Turing machine idea of computability was really created to understand the process of mathematical proof. The fundamental difference is that Turing machines had infinite memory. But for any single program which terminates, only finite amount of tape is used. A proof, by definition, is a finite "program" - so this idea of theorem proving goes way back to the 1920's! So, given any proof, we can accommodate a finite amount of memory for that and run it to check that the proof is indeed correct. Hope this clarifies things! :)
No. The 1976 proof of the four-color theorem has nothing to do with "proof checking". This is the process of writing your paper as formal logic, not as prose (which nobody does becomes its absurdly impractical for hard results), then using a computer to test that your formal logic is error-free. The four-color theorem proof was completely different. That was using math to say the theorem is equivalent to some simple property being true on a large database of special cases, and this property was tested by computer. It was about saving time, not about adding certainty.
The summary is sensationalist nonsense anyway though. One person did this on one result. One other person is trying on another result, and after 10 person-years is about halfway through. And this work isn't going into making the programs better or anything - it's going into manually translating from prose to formal logic. So there's no reason to think the process is going to get easier in the future. Until it does, this will be a marginal technique at best.
So? The Church-Turing hypothesis would say we have the same limitations of formal systems.
Furthermore, it's like program verification and such, an active area of research. (That's a substantial part of what falls under "programming language" research nowadays.) The halting problem, and by extension Rice's theorem, say that you can't do what this entire area is trying to do in general. But for programs that people actually write, it's becoming increasingly practical. In the same way, probably just about all statements that mathematicians actually make in practice are possible to prove rigorously, it's just such a PITA that no one actually does.
When a computer can put together some reasonable proofs in algebraic topology or geometry then we might have something.
Not everything is mathematics is a clean series of algebraic steps. Sure you might be able to get a computer to prove the Snake Lemma, but what about a real theorem?
Holy crap! COMPUTErs used to COMPUTE stuff?! Unbelievable! Who thought up this off the base out of the box idea?!
Bot Assisted Blogging
Dear slashdot mod: How the heck could the first post be redundant?
Copyright infringement is "piracy" in the same way DRM is "consumer rape"
Those are conflicting requirements.
Table-ized A.I.
And my stupid doctor says it's only an ear infection.
Table-ized A.I.
Ha, thank you, I get it now lol.
You just got troll'd!
I work as an assistant professor in mathematics. This sort of program really won't address the needs of the vast majority of publications for any highly regarded professional math journals because math publications are typically very concise and rarely fill in very many of the details. It is not too uncommon for steps in proofs well beyond most talented undergraduates to be taken as "obvious". If they don't want to bother entering all the steps into a paper, you can be sure they don't want to be bothered to enter them into a piece of software and the sheer quantity of math and the wide variety of subtle distinctions in the ways it is used mean this just isn't going to happen. Whats more, Mathematicians really aren't worried that their proofs are incorrect.
I am a student. Not Enough $$$.
New Economic Perspectives
"fully correct, formal, axiomatized mathematics" (facepalm)
tikz wins.
After all, I am strangely colored.
Yes, because translating problems from English to Programming languages is a really small part of solving problems with computers. Lady Lovelace wasted a good deal of time on something like that. Too bad she didn't realize what a waste of time it is.
If video games influenced behavior the Pac Man generation would be eating pills and running away from their problems.
Wow. This looks *nice*! Thanks! Kick PSTricks to curb! (xymatrix stays, though)