Software Is Starting To Aid Mathematical Proofs 90
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."
Re:Awesome (Score:3, Informative)
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.
one proof engine (Score:4, Informative)
Re:Starting? (Score:3, Informative)
Depends on what you mean by aiding (Score:4, Informative)
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?
Re:Starting? (Score:3, Informative)
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.
Re:Depends on what you mean by aiding (Score:1, Informative)
You raise some interesting points, but I gather from the tone of your post that you haven't actually used a production quality proof assistant before (e.g., coq, isabelle, etc.)
You say that these proof assistants will not work as advertised. I'm curious about why you think this is the case. Many of these proof assistants are not ad hoc pieces of software that some average hacker wrote, expecting it to do their mathematics homework for them. Several of the more prominent proof assistants, such as Coq and Isabelle, have been in development for decades. They are based on sound mathematical theories that have, for the most part, been more rigorously verified than many of the results in mathematics that one might often take for granted. If you disagree with this notion, perhaps you can explain why you believe that the Calculus of Constructions, Martin-Lof type theory, etc. are not suitable for doing mathematics.
I assume that the "code" that you refer to is actually the logical, applicative notation that is used by something like Coq. Yes, formulating your mathematics in a way precise enough to be encoded into the underlying type theory used by one of these proof assistants so that it can be mechanically verified does take more effort than informal mathematics. On the other hand, that's entirely the point. If you require the extra degree of certainty afforded to you by doing this, you can expect there to be some effort required to get there.
Regarding your comment about bugs, I think you are a bit misled here. Yes, it's possible, even likely that there are bugs in some areas of these proof assistants. However, if you RTFA, or if you'd ever actually used one of these assistants, you'd know that the kernel of these proof assistants (the part that does the actual verification), are usually extremely small (they reported that Isabelle's is only 500 lines long). That's small enough to be verified by hand or by other proof assistants, which has often been done. A bug in the frontend is mostly irrelevant at that point because whatever errors it might cause will still not lead the kernel to accept an invalid proof. Furthermore, as I said earlier, these proof assistants have been in development for a very long time. They are in use by quite a few large team of people, many of whom use them regularly in the verification of software systems for defence agencies, banking, airlines, etc. The idea that they might be so buggy that they'd be unusable is simply ridiculous and is not true at all.
As for your comment about "A sufficiently well behaved function", no, I'm sorry, but that is not at all rigorous. Perhaps in context such a comment might make sense, but then you already assume that the details are given within the context. Either that or your mathematics is bullshit nonsense. Sorry, there is no free lunch here. I think this is something anyone who is comfortable with logic can understand.
Regarding your comment about formal, axiomatized, correct Mathematics, which mathematics would that be, exactly? In classical mathematics, typically only ZFC set theory, peano arithmetic, and a few other parts are given in anything approaching what would be considered formal by a logician, and there are parts of those theories that not everyone is convinced are correct, by the way. The point of formulating your mathematics in a type theory verifiable by Coq is that all of your assumptions are laid out on the table. There's no funny business, nothing left out that is "obvious" to you but questionable for other mathematicians.
Finally, about blowing things out of proportion, if you are a classical mathematician, I can see why you might be annoyed by someone coming along and telling you that you need to use a computer to do your work now because you and your colleagues are not trustworthy enough. However, these tools have been in use for a very long time within the logic and computer science communities, and they work very well for our tasks, which typically include verifying mathematical p
Math research is a different animal (Score:2, Informative)