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."
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
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.
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?
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.
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.