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

Comments

Starting?

[narcberry]

Maybe we've not run proof validation extensively, but software has been "aiding mathematical proofs" for a long time.

Re:Starting?

[Anonymous Coward]

Seriously, guess they haven't heard of Maple, Mathcad, Mathematica, or Matlab before (any of the BLAS and LAPACK derivatives really)

Re:Starting?

[Anonymous Coward]

If only there was a computerized dupe prover.

Re:Starting?

[644bd346996]

All of those are for computation, not generating or checking proof.

Re:Starting?

[644bd346996]

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:Starting?

[Anonymous Coward]

I guess you didn't quite read the story submission, at least not the last sentence of it.

Re:Starting?

[Anonymous Coward]

Sure, but computation does aid people come up with mathematical proofs.

Re:Starting?

[Anonymous Coward]

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:Starting?

[Iamthecheese]

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.

Awesome

[Anonymous Coward]

I would love to see in fully correct, formal, axiomatized mathematics, why my wife is such a bitch!

Re:Awesome

[Tablizer]

I would love to see in fully correct, formal, axiomatized mathematics, why my wife is such a bitch!

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:Awesome

[ub3r n3u7r4l1st]

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:Awesome

[Anonymous Coward]

Base on the results of Lemma 2 and 5, woman who are married to male nerd have no life.

This does not follow. You fail to prove that a woman can only get life from her husband. You really should have run this through some proof validation software first.

Re:Awesome

[Anonymous Coward]

I would love to see in fully correct, formal, axiomatized mathematics, why my wife is such a bitch!

Actually a disproof; she seemed quite pleasant when I was banging her the other day...

Re:Awesome

[4D6963]

Get a wife

Re:Awesome

[4D6963]

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:Awesome

[4D6963]

Wait.. I don't get it myself...

Re:Awesome

[antispam_ben]

One photo is worth a thousand proofs:
http://greggsutter.com/mt/archives/manWomanControlPanel.jpg

Re:Awesome

[Anonymous Coward]

You misspelled "life" in a common phrase that resulted in a word relevant to the topic. This is assuming it was intentional, of course, making you a comic genius.

Re:Awesome

[Tablizer]

Those are conflicting requirements.

Re:Awesome

[Tablizer]

A + B + C -> Your head is infested with earthworms!

And my stupid doctor says it's only an ear infection.
         

Re:Awesome

[4D6963]

Ha, thank you, I get it now lol.

Re:Awesome

[ub3r n3u7r4l1st]

I am a student. Not Enough $$$.

I am a chair.

[Tablizer]

Let's see it prove I am not a chair ;-)

Re:I am a chair.

[ceoyoyo]

Assume: A: Chairs do not post on Slashdot.
B: Tablizer posted on Slashdot.

Therefore, Tablizer is not a chair.

Re:I am a chair.

[EverStoned]

What if I write a comment posting program called SlashBot, then sit on the computer running it?

Re:I am a chair.

[WK2]

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:I am a chair.

[Lord Lode]

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. Therefore, chairs can't post on slashdot.

Re:I am a chair.

[Daimanta]

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:I am a chair.

[rtaylor]

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.

Re:I am a chair.

[Hotawa Hawk-eye]

Assume: A: Chairs do not post on Slashdot.

[checks for the existence of a user with username chairs, finds no such user] Your assumption A holds ... for right now.

Re:I am a chair.

[poopdeville]

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.

I wonder...

[rascher]

if the proof-verifying-algorithm is polynomially verifiable.

Theorem provers still not generally useful?

[Anonymous Coward]

I was under the impression that current theorem provers can't even deal with integers very well (ie. their applicability is highly limited to working on certain classes of problems with non-numerical finite domains).

Perhaps someone more knowledgeable than I can comment further?

one proof engine

[emeraldemon]

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.

Re:one proof engine

[richkh]

So you've been spending a lot of time playing with co... nevermind.

Re:one proof engine

[ErichTheWebGuy]

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:one proof engine

[Anonymous Coward]

just in case someone wonders, coq is, of course, open source.

Re:one proof engine

[JamesP]

No, you see, coq is french for rooster

So he actually spent lots of time playing with a rooster.

Oh wait...

Re:one proof engine

[jd]

HOL is said to be usable, but doesn't have the same opportunities for name abuse, though 2001 fans could come up with a whole bunch of new ideas. Isabelle, however, would provide such opportunities, if you were to combine it with the package that started this thread. ACL2 is the least abusable name of all, so is quite useless.

Re:one proof engine

[Anonymous Coward]

So HOL is the opposite of coq ... hmmm no signs of abuse there ...

Times a wastin'

[Anonymous Coward]

Quick! Somebody misquote Godel!

Re:Times a wastin'

[Garridan]

"Oops. I broke it." -- Godel

Pipe Dream?

[Anonymous Coward]

While I understand the desire for completeness, there are certain regularly skipped statements that would probably either require a huge (or specialized) library or give really annoying errors as it tries to trace the proof - ex: the complete graph on 6 vertices, K_6 has 15 edges. This would also require fully standardized notation - stable set vs independent set of vertices for example sticking with graph theory. Realistically, this sort of thing might be useful for the tenth 'completeness' seeking project in an area, but would be a ridiculous burden to apply to papers submitted to journals - we want the all star mathematicians proving new ideas, even if there is a small flaw in it, not filling in trivial details that the interpreter cannot accommodate. Given that as a new graduate student I'm still using LaTeX and XFig to write papers, I'm not optimistic about routine use in general mathematics - I have yet to meet anyone happy with the handling of graphics that we are reduced to in LaTeX. I can see use for algorithm verifying, but I don't see the algebraists going for it, nor will there be a good way to accommodate 'proof by picture' where a human reader glances at a diagram and sees the obviousness, but to formally state it would require multiple pages of tedium.

Re:Pipe Dream?

[Garridan]

Kick XFig to the curb, and learn PSTricks. Or, if you're doing algebra, use XYMatrix.

Re:Pipe Dream?

[poopdeville]

tikz wins.

Re:Pipe Dream?

[Garridan]

Wow. This looks *nice*! Thanks! Kick PSTricks to curb! (xymatrix stays, though)

Nothing but calculators

[Anonymous Coward]

Every formal system is limited by GÃdel's incompleteness theorems.

Computers are formal systems.

Re:Nothing but calculators

[techno-vampire]

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.

Re:Nothing but calculators

[lashputin]

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!

Re:Nothing but calculators

[techno-vampire]

Some answers, but first, hang on! What do you mean "what makes Arithmetic complicated ... is the inclusion of infinity?"

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.

Re:Nothing but calculators

[lashputin]

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! :)

Re:Nothing but calculators

[EvanED]

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.

Please read, understand, and mod up

[Anonymous Coward]

"Mathematical proofs are supposed to establish absolute certainty, since each statement is a pure deduction from fundamental axioms."

Does the writer even understand what has been written in the quote and how horribly deficient the statement is? How misleading it is to the average reader? What is being miscommunicated by leaving out the important part? By leaving out the actual subject referred to? By lacking crucial introductory and explanatory powers and instead going for hyperbole and flair?

Ask yourself absolute certainty of what? Logical (and in this case mathematical) tautologies!

Tautology verification machines sound extremely nice until you realize that every single piece of correct mathematics is just that and nothing more. Everything in correct math is a "pure deduction from fundamental axioms" or it wouldn't be math but gibberish!

Fight scientism for the sake of science!

Next Logical Step?

[Nebulious]

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?

Re:Next Logical Step?

[evilbessie]

Right so eliptic curves being intimately related to modular forms, which in turn can be used to prove Fermat's last theorem would be easy to do with a computer. Plus any program for finding proofs would be so complicated that there would be bugs in the code, leading to problems with the proofs it generated. That and mathematicians would not generally accept the results until they have been checked by peer review.

An awful lot of proofs actually go in non logical directions and incorporate very different areas of mathematics. In order to get this level of information in a program it would have to be extremely complex and open to inconsistencies.

You can read http://en.wikipedia.org/wiki/Four_color_theorem which shows that mathematicians do not all accept unverifiable proofs, such as those generated from a computer. Mathematicians like fact, absolute truth, not some method which cannot be checked. http://xkcd.com/435/

There may be some programs which can produce interesting information on which areas in maths may be linked (pattern matching) or for giving ideas as to the validity of statements but they will never become a large method of solving proofs*.

*until the busy beaver function has been solved

Re:Next Logical Step?

[Anonymous Coward]

Pardon me, but how is a proof generated by a computer unverifiable? Shouldn't it be as verifiable as a proof submitted to a journal by a human being?

It seems to me as though any truly unverifiable argument can never ever constitute a proof in mathematics.

Depends on what you mean by aiding

[Secret Rabbit]

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:Depends on what you mean by aiding

[Anonymous Coward]

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

Re:Depends on what you mean by aiding

[thecod]

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 construct these formal proofs, which are checked by the kernel. As you can see, only the kernel needs to be trusted.

Secondly, as TFA states, a big difficulty with formal theorem proving is that in a formal proof, EVERY little detail has to be spelled out. This is a necessary evil for having error-less mathematical developments. The point, again stated in TFA, is that more and more of these trivial steps can and are handled automatically by the proof checking software itself. I think that what research in interactive proof systems has brought is indication that this will not need "AI that is more than a century more advanced than what we have today".

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.

From TFA:

To guard against this possibility, the designers of the proof-checking software make the "kernel" of code that implements the axioms and rules of inference as short and simple as possible.

I would like to add that these interactive proof systems are invariably open source. Why don't you go check for bugs yourself?

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)

I would like you to try and submit an article that contains these words! If "well behavedness" is MATHEMATICALLY defined, then there is no difficulty in integrating this into a proof checking system. In any other case... good luck with publishing that article.

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.

Except that there are a certain number of proofs that mathematicians have a notoriously hard time trusting. The most famous example is the four color theorem, which was formalised in 2004. TFA also mentions the proof of Kepler's conjecture, there has been a fair amount of work on the huge proof of the classification of finite simple groups as well.

Formalising proofs have another important application as well: proof of correctness of computer programs. These proofs usually have the following characteristics: -They are easy: proofs of correctness do not usually rely on complex mathematics, little more than a formalisation of program semantics and elementary arithmetic are needed. - They are tedious: 10000 lines of code make for a very, very long proof. The proof will be filled with very trivial lemmas, and thousands of variations on the same argument. This makes it clear that proving correctness of programs is work that it is quite natural to partially automate. In fact much of the work on formal theorem proving has concentrated on this area. You might know this if you knew anything about formal theorem proving. Or were you suggesting that formalising classical mathematics can not possibly be useful to formalising other areas of science?

Re:Depends on what you mean by aiding

[Anonymous Coward]

Well here you go wrong. It's an illusion to assume mathematics is correct. It's more realistic to say, a typical theorem like the "Cauchy's integral theorem" is correct with chance 1-10^-100 (or something ridiculous close to 1). However more to the frontier of mathematics a realistic probability for a error are much bigger (although still very small). So running verified proof checkers on different computers (to eliminate any mechanical failures) might very well produce results which quickly are much less probable to contain errors. And indeed you are right that to code up a proof in a format that a proof checker can verify will be a pain in the ass. But is what needs to be done if you would convince some other mathematician that all details are correct.

Re:Depends on what you mean by aiding

[Secret Rabbit]

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:Depends on what you mean by aiding

[khallow]

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 proof checker. In the former case, you have a relatively static error finding process versus an asymptotically perfect error finding process.

Re:Depends on what you mean by aiding

[Secret Rabbit]

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 behaved function": You're taking what I wrote completely out of context (see (1)). Note the ()'s after that in which you quote: rigorous within context

I could go on, but I won't waste my time with someone that clearly hasn't actually read what I wrote.

Re:Depends on what you mean by aiding

[Secret Rabbit]

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:Depends on what you mean by aiding

[thecod]

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 user reported bugs.

3) Having to go in a check the checker defeats the purpose of the checker.

Ah, the famous "Who verifies the verifier?". This question is asked in a different form in mathematical logic, where proving consistency of a formal system seems at best pointless and at worst impossible (Goedel). The point is that every proof or program verified in this system is at least as trustworthy as the proof system (or logic) itself which we hope (and almost certainly is) more trustworthy than the program we started with.

4) It isn't my job to check the checker. Nor is it any Mathematicians job to check the checker.

You are going to make a lot of Computer Scientists that work on the meta theory and the implementation of these systems very unhappy. Or are they not Mathematicians?

5) Re: well defined "A sufficiently well behaved function": You're taking what I wrote completely out of context (see (1)). Note the ()'s after that in which you quote: rigorous within context

What your comment seemed to imply is that there are mathematical texts in which objects are assumed to verify a certain number of conditions which are difficult to formalise rigorously. My point was: if it's that difficult to formalise rigorously, then it should not be in a serious mathematical text. Differential calculus was in this situation at the beginning of the XIXth century where it was unclear exactly what a "continuous function" was. It took all the genius of Augustin Cauchy (who was not himself above reproach in matters of rigour) several decades to better the situation.

I could go on...

Re:Depends on what you mean by aiding

[khallow]

The new errors have to get past the tests. And if they can, then the errors might as well have been there in the first place.

Re:Depends on what you mean by aiding

[martin-boundary]

The number of potential errors/bugs is infinite if you want to be able to check proofs of arbitrary length. Merely claiming a monotonically decreasing number of bugs does not imply you will ever get to zero.

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 successful test cases claimed, there is a monotonic improvement implied.

Re:Depends on what you mean by aiding

[Anonymous Coward]

Actually, I did read your entire post, and if you'd read mine in response, you might have noticed that.

Since you apparently haven't read either the article or my response to you, and it's clear that you haven't used any of the systems you are trashing, it's pretty obvious to me that you're nothing more than a troll. I'd even wager that you're not a mathematician, since most mathematicians I am acquainted with are perfectly capable of having a sensible debate, and most of them prefer not to make uninformed comments on technical matters.

Guess I shouldn't have expected much given that this is /. and all.

Re:Depends on what you mean by aiding

[Anonymous Coward]

The number of potential errors/bugs is infinite if you want to be able to check proofs of arbitrary length.

No, this is wrong. The reason it is wrong is because the underlying type theory is given in terms of a finite number of language constructs. Yes, you can construct proofs of arbitrary length within this type theory, but the number of bugs in the type checker is going to be correlated (potentially) to the number of cases where verification, substitution, etc. occur. The number of these cases is finite because the number of unique language constructs is finite.

Furthermore, does nobody understand that it's possible to verify the *entire* verification kernel itself, either by hand or by another, simpler proof assistant?

The issue of hardware faults is a completely separate issue. For example, a mathematician could be reading a "correct" handwritten proof, but have some sort of neurological anomaly occur at the same time which causes her to believe the proof is correct. Does that really matter? No, because other mathematicians will also verify the proof. Similarly, the mechanized proof is unlikely to be verified only once. In the real world, it is verified by everyone working on the proof, which typically means people in different locations and on different hardware. So that significantly lessens the effect of both chronic hardware failures and transient hardware failures to where they are more or less irrelevant.

Re:Depends on what you mean by aiding

[martin-boundary]

No, this is wrong. The reason it is wrong is because the underlying type theory is given in terms of a finite number of language constructs.

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 mathematicians are not comparable to two hardware architectures running the same software. To be truly independent of systematic errors, it would be necessary to write two completely independent proof checker programs, so in general, somebody would end up writing a new proof checker every time, which is a lot more work than running a single checker.

What I mean is that mathematicians don't just follow the exact same steps to verify a proof, they ask if the intermediate results are plausible on completely different grounds, and this often manifests itself in proof variations or simplifications.

Re:Depends on what you mean by aiding

[Anonymous Coward]

No, this is wrong. The reason it is wrong is because the underlying type
theory is given in terms of a finite number of language constructs.

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.

In order for these proof assistants to be able to check a proof, that proof has to be formulated in the language that the proof assistant understands. Some proof assistants use Martin LÃf Type Theory for this, some use the Calculus of Co-Inductive Constructions, others use variants of Set theory. From a formal language point of view, these theories, in which a mathematical proof about *another* mathematical theory (say a theory of arithmetic, or groups, or whatever) must be formulated for the proof assistant to understand, are defined in the typical inductive fashion. In other words, you have a grammar that generates all possible expressions in the language. It just so happens that this language is rich enough to express proofs, unlike the languages most people are used to when they think of grammars in the setting of programming languages or whatever else.

The grammar is more or less a finite tree. The proof checker can be seen as a function that walks over a particular expression that the grammar specifies. Therefore, there are only a finite number of cases to deal with. There should only be a finite number of bugs per case, because the actual code for checking that case is finite as well. Therefore, it's impossible for there to be an arbitrarily large number of bugs given an arbitrarily large proof -- the number of bugs is not correlated to the size of the proof, it's only potentially correlated to the number of cases one needs to check when verifying expressions in the proof language and these finite number of cases are given by the grammar.

And by the way, this doesn't mean you can come up with a universal proof checker or anything like that. Because you have to encode proofs about one theory inside of another theory (in this case the underlying type theory, or proof language), this means there are some proofs that you either can't encode, or aren't verifiable within the proof language. This is a result of GÃdel. In practice, the proof languages for most of these proof assistants are so rich that you would never run into this problem. It would only usually become an issue if you are trying to verify something about another type theory richer than the one in which you are trying to encode the proof to begin with.

What bothers me with your analogy between multiple mechanized verification
and multiple mathematician verification is that two mathematicians are not comparable to two hardware architectures running the same software. To be truly independent of systematic errors, it would be necessary to write two completely independent proof checker programs, so in general, somebody would end up
writing a new proof checker every time, which is a lot more work than running
a single checker.

In practice, most interesting mechanized proofs *are* encoded in more than one proof assistant. There are both technical and sociological reasons for this. The technical reasons have to do with the fact that people often try to simplify a proof once it has been proved, the same way mathematicians typically do. One way of doing this is to try and encode the proof in different theories using slightly different techniques. It's also a way for people to publish papers.

Sociological reasons have to do with the fact that there are often people on different sides of the proof assistant divide that compete with each other. If one side formalizes a proof

Re:Depends on what you mean by aiding

[martin-boundary]

Nice explanation. Thanks.

Re:Depends on what you mean by aiding

[Anonymous Coward]

1) You didn't read what I wrote in what you first quoted of mine. Please actually read before replying to someone.

La la la la, I'm not listening... *plugs ears and sticks out tongue*

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.

Oh really? Here's a three line program in the simply typed lambda calculus with algebraic data:

data Nat where
Zero : Nat
Succ : Nat -> Nat

two = Succ (Succ Zero)

Where's the bug? Oh, that's too trivial for you? Let's try another:

data Nat where
Zero : Nat
Succ : Nat -> Nat

add : Nat -> Nat -> Nat
add m Zero = m
add (Succ m) n = Succ (add m n)

I can *prove* my add function correct here by induction on the second argument. Similarly, I can *prove* that it's an associative and commutative operation. Where's the bug? Oh, you didn't realize you can prove properties about software? Oh, you mean you were full of shit all along? Oh, I see.

By the way, purity (look it up) in proofs and proof irrelevance (look it up) mean that you don't have to "maintain" a proof in the same way you have to maintain some toy piece of software written by some amateur hacker.

3) Having to go in a check the checker defeats the purpose of the checker.

Just like checking your proof defeats the purpose of you having written it, right? Oh wait, have you ever actually written a proof of anything? Have you ever written a *formal* proof of anything? Personally, I doubt either case is true. I think you're the kind of person that sits there and reads about mathematics in popular science articles and then comes on slashdot and tries to act like you're some sort of expert. Maybe I'm wrong though. Perhaps you would be so gracious as to give us some details on your past conquests in formal proofs, or the formal, axiomatic, correct mathematics you referred to earlier.

4) It isn't my job to check the checker. Nor is it any Mathematicians job to check the checker.

Really? I happen to know several mathematicians whose paychecks are causally related to their work on ensuring that various proof assistants are correct. Here are a few of them:

INRIA TypiCal Team

Isabelle at Cambridge

Programming Principles and Tools at MSR

This is only a very, very small sampling of some of the people involved in working on proof assistants and related technology. There are hundreds, potentially thousands of others that use them in secondary projects such as in industry.

These people range from being traditional classical "working mathematicians", to logicians, to computer scientists.

Your claim about mathematicians here is a bit laughable, in part because you have zero credibility -- you haven't responded to a single claims of mine, probably because you can't. You haven't demonstrated how you are in any way representative of the so-called "Mathematician".

5) Re: well defined "A sufficiently well behaved function": You're taking what I wrote completely out of context (see (1)). Note the ()'s after that in which you quote: rigorous within context

I could go on, but I won't waste my time with someone that clearly hasn't actually read what I wrote.

I don't think you personally are capable of even giving a definition of a "well-behaved function" in ANY context, so it's a moot point. Most competent mathematicians, logicians, or computer scientists would have no problem giving such a definition, if it were sensible to do so, but they also wouldn't make the asinine cla

Re:Depends on what you mean by aiding

[Anonymous Coward]

*lol*

data Nat where
    Zero : Nat
    Succ : Nat -> Nat

add : Nat -> Nat -> Nat
add m Zero = m
add m (Succ n) = Succ (add m n)

tag?

[Anonymous Coward]

How do I tag this "goodluckwiththat"?

Open-source

[FreeFull]

The fun in using software for mathematical proofs is that in order for the proof to be valid, the code of the software must be published. If it isn't, the algorithms could be wrong and some code to fake results could be added, but if the source is out then it can be checked if it's valid or not.

Complete Proofs

[jman11]

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!

[Fizzl]

Holy crap! COMPUTErs used to COMPUTE stuff?! Unbelievable! Who thought up this off the base out of the box idea?!

Holy fuck?

[Vexorian]

Dear slashdot mod: How the heck could the first post be redundant?

Re:Holy fuck?

[Anonymous Coward]

Redundant doesn't necessarily mean repetition, check the definition:

adj.
1. Exceeding what is necessary or natural; superfluous.

The American Heritage® Dictionary of the English Language, Fourth Edition
Copyright © 2006 by Houghton Mifflin Company.
Published by Houghton Mifflin Company. All rights reserved.

I'm guessing the mods felt that the comment was unneeded.

metamath since '92

[Anonymous Coward]

Norm Megill has been working on MetaMath since 1992 or earlier, it's
quite an accomplishment and has hundreds of proofs. This isn't a new
idea -- it's very old. It just happens to have buzz lately.

Math research is a different animal

[johnmortal]

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.

Re:Math research is a different animal

[clap_hands]

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

[sherifffruitfly]

"fully correct, formal, axiomatized mathematics" (facepalm)

computer based

[Anonymous Coward]

As of right now I am pursing a degree in computational theory. For one of my "classes" I have to code up proofs. This involves taking what is known (hypothesis) and turning it into multivariate equation. Then find a groebner basis for these equations then determining whether or not the solution equation is inside the groebner basis.

So far I've proved, the intersection of medians of a triangle. And that 4 point of a triangle lie on a circle. I am working on 4-color theorem but everyone knows that's NP-complete hard and the proof checking algorithm for that is long and hard and definitely not P-time because if it was I would be a millionaire .