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?
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?
You are actually comparing /. to fox news for interest in formal theorem proving? Would that make the logic community the Bush administration? Or are they just Clowns? Wait...
My final suggestion is this: check your facts on proof checking and RTFA.
good day sir
