Just wondering, why do people not use Coq/Isabelle/Agda/etc in order to check such proofs? Wouldn't that save them from the "shame" of producing yet-another-incorrect P(!)=NP proof?
It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. But in reality you'll probably find yourself defining what a Turing machine is, what asymptotic complexity is, deriving results like the master theorem, and a thousand other trivialities you would just skip over in a paper.
It is especially problematic that there isn't a common repository of reference implementations of well-known unproved propositions. It would be so easy to make a subtle mistake in your definitions that allowed an existence proof to go through in a way that wouldn't generalize to the actual definition. For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem.
What about things like Metamath [1]? (Not sure if there is a more mature similar effort, Metamath is just the one I've heard of.) It seems like it has quite a lot of the "thousand other trivialiaties" you mentioned, but maybe it's still not enough to make a real dent?
IE, one definition of a Turing machine might exist but it might not that usable for a given proof's purposes.
I see a bunch of proof referenced here and I recall more elsewhere;
Great example! Do you have an outline of this proof? I can see the error in defining a unitary matrix over R instead of C, but I'm not immediately seeing how you can exploit that error to bypass the halting problem.
I'm guessing the concrete error would be introduced by overlooking that the real-valued matrix won't preserve the correct probability amplitude? If so, what's the next step to (falsely) deciding that a given algorithm will complete?
Let p be the real number where, iff the k'th program halts, the k'th bit of p (after the decimal point, in binary) is 1.
Let M be the operation "toggle a bit with probability p", which has matrix [[1-p, p], [p, 1-p]].
When given a program k to solve, keep applying M while counting up how many toggles you see. Do this until the chance that the k'th bit of the sample mean equals the k'th bit of p is greater than 2/3 or whatever other threshold you want, which will take a finite number of samples. Return the k'th bit of the sample mean. This is a probabilistic algorithm which solves the halting problem with arbitrarily high probability.
In other words that shouldn't be the issue, because the correct "setting" for the stochastic matrix still allows for that possibility. It's not something you introduce by using real entries.
The steps to construct a proof of a theorem are as follows:
1. Formally define a language specification which will ostensibly contain the theorem statement and a proof.
2. Search the language space (the set of all strings of the language) for a proof of the theorem statement.
3. If step 2 fails, change the language specification to include prerequisite mathematics or an alternative statement of the theorem.
Even when you exploit clever structural properties of the theorem statement and the language definition, it's extremely easy to encounter a combinatorial explosion when you search for a proof.
On the other hand, suppose you already have a proof and simply want to verify it using a proof assistant. In order to do so, the language you define must be able to automatically verify all prerequisite mathematics which your proof depends on. Encoding that mathematics into a language is difficult and tedious, and dependency checking is itself vulnerable to combinatorial explosion.
It's a very active area of research in its own right, but it can't obviate this problem for the foreseeable future.
I'm not sure this is true -- I thought the whole idea of these theorem systems was to make the kernel of the proof system as simple as possible (to allow a manual proof, or at least high confidence of correctness).
If your program can produce an instance of a type, and it type-checks, then it true. Type inference can be tricky, and a lot of what makes the systems usable is the fact that you can omit types and allow the compiler to infer them, but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof.
Yes, implementing that is the difficult part. I'm not saying it's infeasible - I'm saying it's very difficult. Writing provably correct software is also very difficult. This kind of theorem checking is becoming more common for theorems in e.g. combinatorics, but it's still very uncommon due to the added effort.
This is not how proof assistants based on type theory work. That would be true if you used a prolog-like thing in order to search for a proof, but in these systems the human constructs the proof (just like how they do for P=NP papers) and the system checks if it is correct (unlike P=NP papers, where the human checks if the proof is correct and is usually wrong).
> and dependency checking is itself vulnerable to combinatorial explosion
I am curious on what you mean by that.
As for what I meant by that last point - there is a huge amount of mathematics to encode, almost all of which has not been formally specified into types, and much of which is structurally redundant. Not only is it difficult to encode necessary prerequisite mathematics for a theorem, but that requires its own effort and care, which multiplies the effort required for a given nontrivial proof to be checked.
Also note that I'm distinguishing between the general infeasibility of automated theorem proving and the otherwise great (but ordinarily feasible) difficulty of automated proof checking.