Proofs at this level are nowhere near formal enough for existing mechanical tools to understand. I've seen researchers cite "translated proof X into an automatically-verifiable form" as a major achievement -- even for very simple proofs.
Doesn't that mean that verifying proofs is then based on a super handwavy process where a bunch of researchers come to a consensus and say "yes, this is correct"? Ugh!
What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions?
When you describe a proof with words like you say, aren't there quibbles over semantic things? But I thought the whole point of a proof was that you leave nothing to semantics. Everything logically follows from each other.
I thought the main issue with proofs systems was that encoding the concepts into code was tedious. Could we maybe have a common database of well-known proofs, axioms, concepts etc, so that you wouldn't have to rewrite common ideas from scratch? Like a package manager with proof-libraries?
Or is this an issue with the expression power of proofs languages?
Often times, a proof is (much) more complicated than just mixing theorems A, B, and C together to get result D. Many times proofs will require developing entirely new mathematical structures, or can be done only in steps.
As an example, a friend of mine just proved a great theorem about whether or not Hessenberg varieties can be paved by affines. Ignoring what this actually means, the proof involved firstly recognizing that a Hessenberg variety actually fits within a spectrum - it is somehow "between" other types of well- (or better-) understood varieties. These are paved by affines in (somewhat) obvious ways, and so it is natural to try to use the "between-ness" of the Hessenberg variety to construct a "between-ish" paving. This isn't a proof, but it is a direction (one that turned out to be fruitful). It would be very hard for a computer to have made this intuitive leap.
And it almost works. Except now you can't reduce things like you would like, and you need to construct multi-level fiber bundles in order to get the triviality that you want. And wait - this only works if the Hessenberg variety that we started with has such-and-such property.
So she's reduced the problem to a simpler problem. How does she know it is simpler? Intuition. A computer would have a very hard time recognizing whether or not this is actually simpler (even if it could get there). It turns out that this property holds when our Hessenberg variety is constructed from an element whose semisimple part under the Jordan decomposition is regular. So she has proved it for a huge class of varieties, but not all. Such a partial result would also be very difficult for a computer, since it isn't exactly what she set out to do. She's only partly there. But even this part is huge.
And there isn't anything hand-wavy about her argument, either. It's perfectly grounded in well-established theorems, all of which she understands the proof for. It's just that the original concept was shakey - the "between-ness". She had to work to ground it. It would have been exceptionally hard for a computer to make several of the intuitive leaps necessary to come up with the ideas for the proof in the first place.
>Wait, so you're saying it's easier for humans to prove complex theorems than computers?
Of course! If proving theorems could be readily automated, this would have been done already. Indeed, automation has succeeded for some kinds of problems (e.g. google Wilf and Zeilberger's "WZ method" in combinatorics for a particularly successful example)
>Doesn't that mean that verifying proofs is then based on a super handwavy process where a bunch of researchers come to a consensus and say "yes, this is correct"?
Basically, yes.
>What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions?
This happens surprisingly rarely. It helps that we are trained to constantly question our entrenched assumptions.
>Could we maybe have a common database of well-known proofs, axioms, concepts etc, so that you wouldn't have to rewrite common ideas from scratch?
Various books fill this purpose. But the problem is that theorems are difficult to encapsulate. For example, a theorem will say "Assume X, Y, and Z. Then A and B are true." and you need to use it in some situation where Z isn't true, but some appropriate variant of Z is, and any expert would know how to conclude that A and B are true. This is when the handwaviness comes in.
Mistakes do happen. But surprisingly rarely.
But - and this is key - these errors are usually fixable or the area is not understood well enough and requires more attention to detail. The human intuition is quite powerful.
Usually a lot of previously known errors will crop up despite that the system already works mostly as intended.
>This happens surprisingly rarely. It helps that we are trained to constantly question our entrenched assumptions.
It also helps that finding a counterexample to a widely accepted proof tends to enhance one's career and reputation.
It doesn't need to create the proof, just validate it. See P vs NP.
In some sense we won't really know whether a proof is rock-solid until we have run it through a verifier, using a proven-correct verifier on proven-correct hardware.
If theorem provers grow to be more easy to use, we may require proofs to be verified, but we aren't there yet by a wide stretch.
For an idea about how hard this can be, check out http://www.cs.ru.nl/~freek/comparison/comparison.pdf:
"In 1998, Tom Hales proved the Kepler Conjecture […] with a proof that is in the same category as the Four Color Theorem proof in that it relies on a large amount of computer computation. For this reason the referees of the Annals of Mathematics, where he submitted this proof, did not feel that they could check his work. And then he decided to formalize his proof to force them to admit that it was correct. He calculated that this formalization effort would take around twenty man-years"
(that effort is ongoing at http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet)
Complicated theorems, like the four-color theorem, are different point. Note there though that the original proof of the four-color theorem, which was based on a computer enumeration, was not convincing to many mathematicians when it first came out, in part because it wasn't feasible to verify manually. Researching now, I see that a proof verified by Coq now exists, which I think reduces the amount of distrust.
Yes, mathematicians "come to a consensus." And they make mistakes. Proofs are sometimes believed to be correct for several decades before being shown to be incorrect, though for important proofs - proofs that others depend on - that's extremely rare. But it isn't super handwavy. They've developed processes over time to help identify flaws. This link outlined a few of them: many people work in the same area, so they can cross-check, and workshops and other meetings serve as a way to spread knowledge and get feedback. Note how it will be a couple of years before the proof is published.
If there's a missing crucial aspect, then that may reveal new types of math. Consider the work of Cantor. Quoting Wikipedia, it was "so counter-intuitive—even shocking—that it encountered resistance from mathematical contemporaries such as Leopold Kronecker and [others], while Ludwig Wittgenstein raised philosophical objections. Some Christian theologians (particularly neo-Scholastics) saw Cantor's work as a challenge to the uniqueness of the absolute infinity in the nature of God ... The objections to his work were occasionally fierce: Poincaré referred to Cantor's ideas as a "grave disease" infecting the discipline of mathematics, and Kronecker's public opposition and personal attacks included describing Cantor as a "scientific charlatan", a "renegade" and a "corrupter of youth.""
Nowadays, Cantor's work is considered the origin for set theory.
Part of the training in math is to make those "semantic things" well-defined.
If you go further into the philosophy involved, then you start dealing with formalism, where everything is reduced to symbols manipulated by a grammar (hence how Stephenson's 'Anathem' refers to computers as 'syntactic devices'), and with Zermelo–Fraenkel set theory, which is one of the most common foundations of mathematics. However, then you have things like the continuum hypothesis and the axiom of choice which are not part of the the ZF set theory, leading to ZFC set theory. And at this point I'm well beyond what I know about the philosophy of mathematics.
Suffice it to say that a full formalist description of a theorem, such that it can be reduced to a machine proof, is hard. Take a look at "Principia Mathematica" by Whitehead and Russell. Among other things, it used logic to show that 1+1=2. (See the end of the proof at http://en.wikipedia.org/wiki/File:Principia_Mathematica_theo... - "The above proposition is occasionally useful.") That might give you a idea of what the effort looks like.
Formally, a proof is a sequence of assertions, where each one is an axiom or follows from previous ones. Humans are better at proofs because they have good and well-developed intuition; it's bit like coding in assembly vs coding in a high level language. The fact that you deal with infinite objects is not relevant.
In more concrete terms .. and I am so far outside my knowledge that I barely know what I am saying ... I read in the Coq FAQ that "The axiom of unique choice together with classical logic (e.g. excluded-middle) are inconsistent in the variant of the Calculus of Inductive Constructions where Set is impredicative. As a consequence, the functional form of the axiom of choice and excluded-middle, or any form of the axiom of choice together with predicate extensionality are inconsistent in the Set-impredicative version of the Calculus of Inductive Constructions."
In other words, proofs involving "axiom of unique choice together with classical logic" cannot be expressed in at least Coq. While it might be possible to use a machine to check tools which assume the axiom of unique choice, it would no doubt take a lot of work if one needs to build such a system from scratch.
And that is the scenario - where it's much more difficult to develop a mechanical tool than to come up with a proof that enough for humans - that I am contemplating.
For every set A and function f : A -> P(A) there exists y in P(A) such that for all x, f(x) /= y.
Proof: Define y = {a: a is not in f(a)}. If f(x) = y, then f(x) = {a: a is not in f(a)}, but this implies x is in f(x) <=> x is not in f(x), contradiction.
It does not mention infinity anywhere! It only says that there cannot be a surjection between one set and the other. We could call this situation "transfinite" but this is only a name; under the hood, this is a normal proof of properties of functions, using very natural reasoning rules. That's why I disagreed - there's nothing special in Cantor's proof from a formal viewpoint, possible concerns are of psychological/historical nature, which are not relevant to a machine.
It is true that changing foundations might require rewriting the prover. However, humans also need time to adjust to a new formal system. For example, it takes a lot of effort to get a good grasp of intuitionistic logic. This might be a concern, but ZFC is a very well-grounded common framework for mathematicians, and this is extremely unlikely to change. Perhaps calculus of constructions, as a version of lambda calculus, is closer to computation, and this is why it was chosen in Coq. I'm not sure. Mizar (another theorem-proving environment) is based on an extension of ZFC. [ZFC is untyped - everything is a set, while CoC has a rich type system.]
Small nitpick: It's not like proofs involving unique choice + excluded middle cannot be expressed in Coq; they can, but as the system is inconsistent, they have no value, as everything is provable.
NB I am a programmer and very weak in theory.
at the time there was still a school of artificial
intelligence that assumed that a big computer running a
really sophisticated program could be equivalent to a
human mind
Currently, yes. But I don't see that this is necessarily true. Why do you think it is?
These two statements seem to contradict, unless you grant that the mind either fudges the proof or constructs new axioms such that the proof can be valid. Why do you assume a program can never do this?
Really? I don't see what reason we have to believe that this is true.
Do you have an example of this? I have an extremely difficult time comprehending it. Also, I was under the impression that there weren't necessarily propositions that are not algorithmically possible to reach, but rather, there are always propositions a given algorithm cannot solve.
I just meant undecidable propositions.
> Do you have an example
Maybe check out the conclusion on p.76 of this book[1] by Penrose (and the argument supporting it that begins on p.72.): "Human mathematicians are not using a knowably sound algorithm in order to ascertain mathematical truth".
His example is our knowledge that a certain computation will not halt, and the impossibility of constructing an algorithm that can prove that fact.
More flippantly, you know that you can examine the soundness of your own reasoning, but no algorithm can reach conclusions about its own correctness.
http://terrytao.wordpress.com/career-advice/there%E2%80%99s-...
Computer proofs tend to be brute force. For example: Are all games of Freecell winnable? But a brute force run of all Freecell games just tells us that all but one game is winnable, but tells us nothing about what's happening or why.