>The method is called ‘proof by exhaustion’, because it involves reducing the problem to 10,000 special cases and then settling each one with detailed calculations… thus exhausting anybody who tries to check the proof by hand.
It should be noted that there is some reason to aesthetically dislike computer-generated proofs.
It's not mentioned by Baez, but one of the first breakthroughs in the Erdos discrepancy problem was a very verbose (running into a few GBs if I remember right), computer generated proof, for a subcase. Terry Tao later presented a general proof which was far far shorter.
Obviously there are cases like the 4-color theorem which have withstood the test of time and prejudice, but there is something sad about not being able to make sense of such math.
Name one? I think I understand that it's unsatisfying that there are instances where mathematics cannot be done with just pencil and paper. However, it's a reproducible proof. And folks in science have long gotten over the fact that there are important results that can only be achieved with lots of computing power, and not just pencil and paper.
The point of mathematics is not just to know whether some proposition is true, it's to understand the mathematical objects under study. A beautiful proof sheds light, it explains why.
yeah. adding to this, a great proof that uses new techniques can also generate whole new areas of math to explore or solve other seemingly unrelated problems.
That's your view on the point of math. I would be perfectly content to have a long, computer generated proof of P ?= NP. Of course I prefer beauty and elegance in proofs, but I think leveraging the computer as a tool to prove things for us is quite an elegant thing by itself.
I think P vs. NP is one proof where insight matters a lot. As Scott Aaronson said, if CS were physics, we would have declared P != NP a law of nature a long time ago. We basically know it to be true already. A proof that we can't understand adds almost no information in this case.
It would be horrible if we had an impossible to understand, but correct, proof of P = NP that gave no hint of how to actually construct polynomial algorithms for those problems.
Interestingly, there are algorithms for solving NP-complete problems which are provably polynomial time iff P = NP. So the moment P = NP is proven, we immediately know of polynomial-time algorithms for NP-complete problems. We have the algorithms today, we just don't know if they are in P.
For one thing, the point of a proof is not its use merely for showing the validity or invalidity of a statement, but in the generation of new approaches/theories.
Atleast that's my view of Math; this is not to say either that being able to verify proofs is bad (this is orthogonal), nor is to say that there aren't proofs that can't be worked out by pencil-paper.
On a meta level, it seems unlikely that a computer will be able to create theories and abstractions while trying to solve such problem, given the current state of AI, in the conceivable future. I do believe such "unsupervised learning" is necessary for doing math.
This of course is quite a different line of work than in PL/Verification where one only cares if something they've written can be proved to satisfy some properties. However, I've heard often that a proof of a program is often as long as the program itself; this is often reflected in the difficulty people have in parsing code without adequate high-level milestones.
For one thing, there can be subtle errors in a computer proof (overflow is obvious, but compiler bugs, CPU bugs, and RAM errors are not). If you can create a brief proof, then you can avoid all those problems.
It should also be noted that with a finite vocabulary, the vast majority of interesting mathematical theorems cannot be stated in a reasonable amount of time.
I'm having trouble understanding this statement and its motivation. Under what definition of "interesting" can any "unreasonably" long theorem statement be of interest to humans, and what makes you this class of theorems is numerous?
Proof: Assume there are uninteresting theorems. Let T be the shortest such theorem (under some fixed encoding). Having the special property of being the shortest uninteresting theorem makes T interesting. qed.
It seems to be part of our habit in mathematics to first make many discoveries using brute-force and large enumerations, and then later extend the results with more sophisticated methods if we can find them. For one practical example, if you were doing a lot of computation in the 1960's you might carry around a book of trig functions, or a slide rule, but after microprocessors came about a pocket calculator could do all those functions with better precision. With proofs, many questions are proven up to some number n, which is only further extended by feeding the algorithm into a powerful computer. But occasionally we discover a way of reframing the problem so that it can be solved with relatively little computation.
I believe programming has some analogous quality to it: It's much easier to solve just one problem and gradually find ways to generalize it.
> if you were doing a lot of computation in the 1960's you might carry around a book of trig functions, or a slide rule, but after microprocessors came about a pocket calculator could do all those functions with better precision
The pocket calculator is doing a huge amount of computation to find those results, an amount which would be impractical for the human to do (hence the use of slide rules instead of laborious pen-and-paper arithmetic). It’s just a different flavor of brute force. The calculator is basically going back to the pre-logarithm method, carrying out elementary school arithmetic algorithms very fast.
To be honest, the slide rule method – converting multiplication problems to addition problems via a logarithm lookup table encoded on a stick – is quite a bit more “elegant” than what the calculators are doing. The invention of logarithms in ~1600 was one of the most important advances in the history of science and technology.
* * *
The same is true in many other kinds of mathematical problem solving. In the past, we only had access to manual effort and limited human time/attention, so the available brute computation was quite limited and many problems were entirely intractable, and great cleverness was required to solve others. The goal of symbolic reasoning was to reframe problems to eliminate as much manual computation as possible. For that reason, it was necessary to learn how to manipulate trigonometric identities, solve nasty integrals by hand, etc. We had to be able to rewrite any problem in a form where each concrete computation only required a few simple arithmetic steps plus as few table lookups as possible. Despite such simplifications, actually performing computations often required teams of people mechanically performing arithmetic algorithms all day. https://en.wikipedia.org/wiki/Human_computer
Now that computation is cheap, we can dispense with many of the clever/elegant methods of the past, and just throw silicon at our problems instead. This lets us treat a wider variety of problems in a uniform way, and get away from doing nearly so much tricky algebra.
> The pocket calculator is doing a huge amount of computation to find those results, an amount which would be impractical for the human to do (hence the use of slide rules instead of laborious pen-and-paper arithmetic). It’s just a different flavor of brute force. The calculator is basically going back to the pre-logarithm method, carrying out elementary school arithmetic algorithms very fast.
I think the point is more that all those computations are packaged up into a black box where the user doesn't need to think about its internals. Elegant/short proofs are often like this too: they build on deep/high-power/complicated-to-prove results, using them as black boxes. Of course the actual proofs of those theorems might be ugly (e.g. a proof that uses the four colour theorem), but the statement can still be neat.
Your mention of "invention of logarithms" raises a couple of questions.
First: is there a good, accessible (college calculus, some diff eq, some linear algebra) history of mathematics you might recommend?
Second: I've been kicking around an ontology of technological dynamics (or mechanisms) for a few months. In it I classify mathematics under symbolic representation and manipulation, along with what I see as related tools of speech, language, writing, logic, programming, and AI. If that sets off any lights, bells, or whistles, I'd be happy to hear ideas or references.
> This is one of the world’s biggest proofs: it’s 200 terabytes long! That’s about equal to all the digitized text held by the US Library of Congress. There’s also a 68-gigabyte digital signature—sort of a proof that a proof exists—if you want to skim it.
This sort of comparisons always bothers me, they make no sense.
Also according to the Nature post linked, the 68G "digital signature" is just the 200T compressed, just another sign that talking about the file sizes is meaningless.
OK look, running a^2 + b^2 = c^2 a few trillion times and calling that a "long proof" is disingenuous - it's really long if you include every single operation, but must you? I just described it here in a few sentences. I guess what's more interesting is a sort of kolmogorov complexity of the proof, perhaps.
You've described a very short algorithm for finding a very long proof. But what the algorithm finds is indeed a very long proof, not a short one, and the reason I say that is because the short algorithm description you gave doesn't convince me of the truth of the statement "Every coloring of positive integers up through 7825 contains a monochrome Pythagorean triple"; you could give similarly short descriptions of algorithms searching for hypothetical proofs of any number of false claims. It's only the long-ass step-by-step completed execution of that algorithm which does the convincing.
Isn't that just a fancy way of asking "does there exist a more concise proof for this theorem?" That is to say wouldn't we rather assign a kolmogorov complexity to a theorem instead of a specific proof for that theorem.
I'm not even sure what we would mean by assigning a complexity to a specific proof. The proof is the proof. Would it basically mean "is this specific proof compressible?" But then I think thats essentially the same as asking "is there a shorter proof?" As the new shorter proof is the compressed representation + the decompression program.
But what we're really interested in, is what is the shortest representation that proves the theorem as thats what we're ultimately interested in, right?
This specific proof is a large case-analysis, though much smaller than brute force of all possible cases. There may however be a simpler more beautiful and shorter proof. If so, then that demonstrates that the theorem has a lower kolmogorov complexity than the current best known proof suggests.
"As the new shorter proof is the compressed representation + the decompression program." A proof is a sequence of deductions, not a program that generates a sequence of deductions.
You might be interested in reading about the Curry Howard Correspondence.
From wikipedia: "In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects." https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Yes, I've encountered one form of the Curry-Howard correspondence before. Are you claiming that, via the Curry-Howard correspondence or some related phenomenon, the corresponding proof of a program used to compress a proof is the same (or at least, proves the same theorem) as the original proof that the program was meant to compress? That is interesting and I would appreciate if you could expand on it.
If you’re using the right language, proofs are programs; it’s as simple as that. “Compressing” a proof, then, amounts to doing what good programmers are already doing — noticing patterns and eliminating redundancy.
The Curry-Howard correspondence does not apply here though. The coloring theorem is not encoded in the type of the program that enumerates and checks the possible colorings. The program itself is a restatement of the coloring theorem, with the result type being boolean (all the enumerated colorings satisfy the property, or not). So the proof would consist of proving that the program must terminate with a true value. Of course that is not actually useful as it does not simplify anything.
This is a simple mechanization of the proof steps, on par with using a calculator for arithmetic.
Depending on what programming language you use for your Curry-Howard correspondence, there is actually a related thing. Probably the most well known realization of C-H is dependent type theories like Coq and Agda. And those support a proof method called "proof by reflection".
The idea is that in those languages, types can contain program terms as subexpressions, and two types are considered "the same" if they evaluate to the same expression. Because the languages enforce that all expressions terminate, it's still decidable whether a program is well-typed or not, so the language can still be considered a proof system, but the type checker can take almost arbitrarily long time to check a program because it has to evaluate subexpressions to values in order to check type equality.
Anyway, the point is that this can be used to write down short programs that act as proofs. For example, suppose you want to prove there are no counterexamples to Fermat's last theorem for exponent 5 and numbers less than 100000000. In this case, you would write down a function
f : nat -> bool
which evaluates the expression for all numbers less than the argument and returns whether there is a counterexample, then you would prove a lemmma
soundness : forall n, (f n = false)
-> forall x y z,
(x < n) -> (y < n) -> (z < n)
-> (x^5 + y^5 ≠ z^5)
and then the proof of the final theorem is just
soundness 100000000 eq_refl
In order to check the eq_refl part, the type checker would evaluate (f 100000000) and verify that it evaluated to false. But all that computation is not recorded in the proof term. So the program that represents the proof is very small, and constant size in the bound.
This is actually very useful in practice, because storing and manipulating big proof terms is slow and memory-hungry, so it's useful to be able to push the computation under the carpet in this way. On the other hand, it is sometimes considered a little philosophically dubious.
That doesn't make proofs any shorter or any more elegant, though. The same "noticing patterns" can be done on the proof in non-FP form. C-H is basically an observation about encoding.
Yes, in fact every single mathematical proof can be reduced to a few lines of code! You just write a program that verifies a proof, and another program that brute forces through the space of all possible proofs. It should fit onto a page or two. So the kolmogorov complexity of any proof has a pretty small upper bound.
That isn't a proof, it's a procedure for finding a proof. The procedure might fail, and whether it will fail or not cannot be checked without running it - which is not guaranteed to halt! Of course, to guarantee that it halts, you could include an upper bound on the size of the proofs it searches in your program. So then at least your "proof" is checkable. However, it is not in general efficiently checkable - that is, checkable in polynomial time. If it were, it could only produce polynomial compression!
(Though admittedly, polynomial compression is pretty good, practically speaking.)
As for Kolmogorov complexity, there are infinitely many distinct proofs, so their Kolmogorov complexity cannot possibly be bounded.
I think you're missing an important point though. The article's proof is guaranteed to be verifiable in a known finite amount of time. Your example does not so it's hard to take commentary from it onto the article's subject.
I think you're missing the important point that Houshalter was being sarcastically critical of makmanalp's dismissive top-level comment, not the proof in the article.
I don't see how Houshalter's post can possibly be read as sarcastic, it looks like a technical comment that makes an interesting point that is slightly tangential. I simply don't know how to read that comment as if there were a /s at the end. And I don't see how the top level comment can be considered dismissive, it too is making an interesting point that we should use another metric.
If you demand that the program terminates (through higher order structural recursion, i. e. by induction) then this would be a proof in type theory. It's called proof by reflection. When Martin Löf (the father of type theory) saw this trick for the first time he apparently exclaimed "but this is not a proof!" so make of that what you will.
I think there are some proofs that are /just/ complicated. I'm certainly not an expert on this subject but for example a few years ago, Deolaikar's (ultimately erroneous) P/=NP proof paper was 66 pages. 66 full, information dense pages.
Also, can't there be a measure of complexity without the absurd extreme of "in my special language, there is a single function call that proves X"?
In your example, it's not the proofs that can be reduced to a few lines of code, it's the thing that generates the proofs. That little program wouldn't contain information about which proofs are "interesting" or "correct", since that's the reason it exists in the first place. Adding in that information would make it much larger.
Anyway, it just seems disingenuous to call that proof 200 terabytes. You don't need most of those 200 terabytes to understand the proof, and neither do you have to even store those 200 terabytes to know that none of the numbers you went through worked.
Houshalter is pointing out that your definition of "just complicated" is not sufficient (in the usual way we mathematicians do, with counterexamples). He's showing that once you know a theorem is true (even if it's P != NP), every proof has essentially constant Kolmogorov complexity. Kolmogorov complexity does not take into account computational complexity of the program outputting the target string. There is time-bounded Kolmogorov complexity, but I don't know if I'd call it a standard measure.
There is also a measure called "proof complexity" that compares the length of a proof to the length of the statement being proved. If the relationship is polynomial then the proof is considered "interesting." If it's exponential, uninteresting. You also need a parameter, which in this case there isn't since it's a specific n, but you can extrapolate the proof technique to asymptotic n and call it exponential from that perspective and I don't think anyone would argue with you.
Right, yes, I should have been clearer, Kolmogorov complexity was just an example of the kind of thing I'm going for. I understand that Kolmogorov complexity doesn't quite cover it, though I don't think this precludes the notion of a measure that /does/ cover the idea of the fundamental complexity of a proof. It sure feels like there's something different about a proof that repeats the same functional form over and over again for 200TB vs 200TB of more complex statements.
For example, perhaps there exists somewhere a language that includes the most basic atoms of mathematics, and when you express a proof in that language - like the Principia Mathematica, perhaps - then maybe it's guaranteed to be in irreducable canonical-form, and then you can go on the complexity of that.
But I do now see that the 200TB should be considered part of the proof because you haven't verified the proof until you've tried every single item, versus when you've gone through normal short proof you're certain of the result by the end of it.
> You don't need most of those 200 terabytes to understand the proof,
I believe that you do. I would argue no human "understands" a 200 terabyte proof. Maybe they understand the procedure that arrived at the proof, but my point is that isn't a proof itself, or understanding why it is true.
Maybe we could define the Kolmogorov complexity of a proof as the number of lines of code, PLUS the size of the proof that the proof-generating program halts.
Or the total number of lines of code in a sequence of programs, where the first program generates a proof of the original theorem, and every other program generates a proof that the preceding program halts, PLUS the size of a proof that the final program halts.
Many folks would say that's not a proof, because it's not efficiently checkable. To tell whether it actually proves the thing, I have to go off and check every number, which takes an enormous amount of time compared to the length of the "proof".
Of course, the solution of listing every single case seems about equally unhelpful. The whole thing leads one to question whether proofs are really the goal of mathematics, or just a useful proxy.
I think it's checkable. You just have to write another program to check the proof, and maybe a meta program that checks that your proof-checking program is correct.
I think there is a good chance that in the future we have computers coming up with and proving theorems that we don't fully understand (but for which we understand the practical value) and the human contribution will be to write a program that verifies that the proof is indeed correct.
In classical logic your statement entails that there is a proof that cannot be checked (marked "true") by an algorithm (note, that the proof itself cannot be checked, not a fact, for which there is no proof) or that there is an algorithm marking something "true" that doesn't constitute a proof (trivially the thing that is marked "true" is proven). I doubt you'll find counterexamples to either of them, as an infinite, yet valid, proof is hardly believable (nobody of us could ever finish reading it) and a terminating ("marking true") algorithm always computes something.
>The method is called ‘proof by exhaustion’, because it involves reducing the problem to 10,000 special cases and then settling each one with detailed calculations… thus exhausting anybody who tries to check the proof by hand.
Ha.