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."
Starting? (Score:1, Redundant)
Maybe we've not run proof validation extensively, but software has been "aiding mathematical proofs" for a long time.
Re: (Score:3, Informative)
Re: (Score:2)
All of those are for computation, not generating or checking proof.
Re: (Score:2)
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.
Re: (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 co
Re: (Score:2)
Holy fuck? (Score:2)
Re:Awesome (Score:4, Funny)
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!
Re: (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.
Re: (Score:3, Funny)
Re: (Score:2)
Re: (Score:2)
Re: (Score:1)
Those are conflicting requirements.
Re: (Score:1)
I am a student. Not Enough $$$.
Re: (Score:2)
A. Your logic is weak
B. Earthworms are weak
C. Logic resides inside your head
A + B + C -> Your head is infested with earthworms!
Re: (Score:1)
And my stupid doctor says it's only an ear infection.
Re: (Score:2)
One photo is worth a thousand proofs:
http://greggsutter.com/mt/archives/manWomanControlPanel.jpg [greggsutter.com]
I am a chair. (Score:1)
Let's see it prove I am not a chair ;-)
Re: (Score:3, Insightful)
Assume: A: Chairs do not post on Slashdot.
B: Tablizer posted on Slashdot.
Therefore, Tablizer is not a chair.
Re: (Score:2)
Re: (Score:3, Funny)
Assume: A: Chairs do not post on Slashdot.
Why would I assume that? In fact, chairs posting on Slashdot is my hypothesis to explain why the posts seem as intelligent as they are, and why so many Slashdotters are afraid of Steve Ballmer.
Re: (Score:2)
Re: (Score:1)
If a chair would post on slashdot, it wouldn't be a chair, but a computer in the shape of a chair, or a human disguised as a chair.
And what if the computer in the shape of a chair was for sitting on? That would make it a bona-fide chair, with an embedded CPU.
Re: (Score:2)
Assume: A: Ballmer posts on Slashdhot
Therefore, chairs do not post on Slashdot
B: Tablizer posted on Slashdot
Therefore, Tablizer is not a chair.
Re: (Score:2)
[checks for the existence of a user with username chairs, finds no such user] Your assumption A holds ... for right now.
Re: (Score:2)
First we would need to determine the kind of chairs.
Many an emperor has used their slaves as a seat.
You may be in charge of a meeting at some point or an organization.
There is a chance you have musical talent and could be in an orchestra.
I think you should prove you are not a chair first because I'm pretty damn certain is someone offered you a substantial amount of money to act as a seat for a day, you would.
Proving you are not a 4 legged wooden bar chair is fairly straight forward.
I wonder... (Score:1)
if the proof-verifying-algorithm is polynomially verifiable.
one proof engine (Score:4, Informative)
Re: (Score:1)
Re: (Score:2)
No, you see, coq is french for rooster
So he actually spent lots of time playing with a rooster.
Oh wait...
Re: (Score:2)
For what it's worth, I've had good experiences with coq
Don't forget to pay your $699 licensing fee, you coq-smoking teabagger!
Re: (Score:2)
Re: (Score:1)
Re: (Score:1)
Re: (Score:1)
tikz wins.
Re: (Score:1)
Re: (Score:2)
Re: (Score:1)
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", bec
Re: (Score:2)
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,
Re: (Score:1)
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 o
Re: (Score:1)
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
Next Logical Step? (Score:1)
Re: (Score:2)
An awful lot of proofs actually go in non logical directions and incorporate very different a
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: (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
Re: (Score:2)
I only read the first couple paragraphs before I stopped reading as you clearly only skimmed mine. As in, the answers are already there.
Re: (Score:1)
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.
This is completely wrong, on several points:
firstly a proof checker actually does check proofs in a very precise sense: a proof is a rigorously defined, implementable object and a proof checker verifies that this object does indeed consist of a proof of a given proposition. This is (non trivially) decidable; i.e. there exists an algorithm that carries out this task, it forms the basis of any given proof checking software called the kernel. The rest of the software is just an environment to help the user co
Re: (Score:2)
1) You didn't read what I wrote in what you first quoted of mine. Please actually read before replying to someone.
2) I'll paraphrase from the Tao: Though a program be but 3 lines long. Some day, someone will have to maintain it. Similarly, no matter how small a program is, it will contain bugs.
3) Having to go in a check the checker defeats the purpose of the checker.
4) It isn't my job to check the checker. Nor is it any Mathematicians job to check the checker.
5) Re: well defined "A sufficiently well beh
Re: (Score:1)
2) I'll paraphrase from the Tao: Though a program be but 3 lines long. Some day, someone will have to maintain it. Similarly, no matter how small a program is, it will contain bugs.
In the world of software development that the Tao refers to I have no doubt that this is true. But I have a dream... that someday my programms will not be juged by the number of their bugs but by the usefulness of their content...that someday the sons of a former logician and the sons of a former software engineer will be able to sit down together at the shell prompts of brotherhood... Also, it seems that the software that controls, say, a driverless subway system can not really afford to wait around for u
Re: (Score:2)
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.
I believe you're wrong for a very simple reason. The error in a proof checker is strictly decreasing. One can construct increasingly elaborate test cases as the proof checker is developed and vet each change (including new platforms) against this growing body of test cases. In comparison, each new math paper as it stands has a similar chance of evading error. But once these papers are converted to the language of the proof checker, then they too are subject to the asymptotically improving reliability of the
Re: (Score:2)
You're assuming that bug fixes won't introduce new errors. Are you sure that's a good assumption? Because, I've used computers before, and I know that it isn't.
Re: (Score:2)
Re: (Score:2)
The other thing you ignore is the fact that there are external bugs in the operating system and hardware (eg the infamous intel division bug), which can falsify the conclusion that a particular tests was actually passed. Thus it is not actually true that, even with a monotonically increasing number of
Re: (Score:2)
Wouldn't that apply only to a single mathematical theory at a time? Surely you're not claiming a universal proof checker? Then you'd have an infinite number of finite potential bugs. I probably don't understand what you're saying.
What bothers me with your analogy between multiple mechanized verification and multiple mathematician verification is that two mathema
Re: (Score:2)
Complete Proofs (Score:1)
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?
Woah there! (Score:2)
Holy crap! COMPUTErs used to COMPUTE stuff?! Unbelievable! Who thought up this off the base out of the box idea?!
Math research is a different animal (Score:2, Informative)
Re: (Score:2)
A question is, is this a problem? Are those "obvious" steps in proofs ever wrong? Given that, as you say, they are "well beyond most talented undergraduates", aren't there lots of slip-ups?
I hate it when idiots talk about math/physics, etc (Score:1)