**The world's most long-winded proof**

In the 1980s, the famous mathematician Ronald Graham asked if it's possible to color each positive integer either red or blue, so that no triple of integers a, b and c obeying Pythagoras’ famous equation:

a² + b² = c²

all have the same color. He offered a prize of $100.

Now it's been solved! The answer is

*no*. You can do it for numbers up to 7824, and a solution is shown in this picture. But you can't do it for numbers up to 7825.

To prove this, you could try all the ways of coloring these numbers and show that nothing works. Unfortunately that would require trying

3 628 407 622 680 653 855 043 364 707 128 616 108 257 615 873 380 491 654 672 530 751 098 578 199 115 261 452 571 373 352 277 580 182 512 704 196 704 700 964 418 214 007 274 963 650 268 320 833 348 358 055 727 804 748 748 967 798 143 944 388 089 113 386 055 677 702 185 975 201 206 538 492 976 737 189 116 792 750 750 283 863 541 981 894 609 646 155 018 176 099 812 920 819 928 564 304 241 881 419 294 737 371 051 103 347 331 571 936 595 489 437 811 657 956 513 586 177 418 898 046 973 204 724 260 409 472 142 274 035 658 308 994 441 030 207 341 876 595 402 406 132 471 499 889 421 272 469 466 743 202 089 120 267 254 720 539 682 163 304 267 299 158 378 822 985 523 936 240 090 542 261 895 398 063 218 866 065 556 920 106 107 895 261 677 168 544 299 103 259 221 237 129 781 775 846 127 529 160 382 322 984 799 874 720 389 723 262 131 960 763 480 055 015 082 441 821 085 319 372 482 391 253 730 679 304 024 117 656 777 104 250 811 316 994 036 885 016 048 251 200 639 797 871 184 847 323 365 327 890 924 193 402 500 160 273 667 451 747 479 728 733 677 070 215 164 678 820 411 258 921 014 893 185 210 250 670 250 411 512 184 115 164 962 089 724 089 514 186 480 233 860 912 060 039 568 930 065 326 456 428 286 693 446 250 498 886 166 303 662 106 974 996 363 841 314 102 740 092 468 317 856 149 533 746 611 128 406 657 663 556 901 416 145 644 927 496 655 933 158 468 143 482 484 006 372 447 906 612 292 829 541 260 496 970 290 197 465 492 579 693 769 880 105 128 657 628 937 735 039 288 299 048 235 836 690 797 324 513 502 829 134 531 163 352 342 497 313 541 253 617 660 116 325 236 428 177 219 201 276 485 618 928 152 536 082 354 773 892 775 152 956 930 865 700 141 446 169 861 011 718 781 238 307 958 494 122 828 500 438 409 758 341 331 326 359 243 206 743 136 842 911 727 359 310 997 123 441 791 745 020 539 221 575 643 687 646 417 117 456 946 996 365 628 976 457 655 208 423 130 822 936 961 822 716 117 367 694 165 267 852 307 626 092 080 279 836 122 376 918 659 101 107 919 099 514 855 113 769 846 184 593 342 248 535 927 407 152 514 690 465 246 338 232 121 308 958 440 135 194 441 048 499 639 516 303 692 332 532 864 631 075 547 542 841 539 848 320 583 307 785 982 596 093 517 564 724 398 774 449 380 877 817 714 717 298 596 139 689 573 570 820 356 836 562 548 742 103 826 628 952 649 445 195 215 299 968 571 218 175 989 131 452 226 726 280 771 962 970 811 426 993 797 429 280 745 007 389 078 784 134 703 325 573 686 508 850 839 302 112 856 558 329 106 490 855 990 906 295 808 952 377 118 908 425 653 871 786 066 073 831 252 442 345 238 678 271 662 351 535 236 004 206 289 778 489 301 259 384 752 840 495 042 455 478 916 057 156 112 873 606 371 350 264 102 687 648 074 992 121 706 972 612 854 704 154 657 041 404 145 923 642 777 084 367 960 280 878 796 437 947 008 894 044 010 821 287 362 106 232 574 741 311 032 906 880 293 520 619 953 280 544 651 789 897 413 312 253 724 012 410 831 696 803 510 617 000 147 747 294 278 502 175 823 823 024 255 652 077 422 574 922 776 413 427 073 317 197 412 284 579 070 292 042 084 295 513 948 442 461 828 389 757 279 712 121 164 692 705 105 851 647 684 562 196 098 398 773 163 469 604 125 793 092 370 432

possibilities. But recently, three mathematicians cleverly figured out how to eliminate most of the options. That left fewer than a trillion to check!

So they spent 2 days on a supercomputer, running 800 processors in parallel, and checked all the options. None worked. They verified their solution on another computer.

This is the world's biggest proof: 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.

It's interesting that these 200 terabytes were used to solve a yes-or-no question, whose answer takes a single bit to state:

*no*.

I'm not sure breaking the world's record for the longest proof is something to be proud of. Mathematicians prize

*short, elegant*proofs. I bet a shorter proof of this result will eventually be found.

Still, it's fun that we can do such things. Here's a story about the proof:

http://www.nature.com/news/two-hundred-terabyte-maths-proof-is-largest-ever-1.19990

and here's the actual paper:

• Marijn J. H. Heule, Oliver Kullmann and Victor W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, http://arxiv.org/abs/1605.00723.

The

**cube-and-conquer**paradigm is a "hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers"... whatever that means. It would be interesting to learn about this. But it's time for breakfast!

Anyone who makes a joke about Fermat's remark:

*"I have discovered a truly marvellous proof of this, which this margin is too narrow to contain."*

loses 10 points, for not reading my whole post.

#bigness

View 69 previous comments

- +Marco Devillers wrote: "At some point I expect a mathematician to prove that there simply are classes of problems for which only 'disgusting' proofs exist."

There's a fair amount known about this, but I would like to know more.

I believe it was Gödel who showed that for any recursive function F: N -> N, there are, for any n, theorems whose statement contains about n symbols but whose shortest proof contains at least F(n) symbols. Here by "proof" I mean "proof in any fixed consistent recursively enumerable axiom system extending Peano arithmetic".

There are two nice ways to prove this result. One is to note that if it were false, the provability of statements would be decidable: to see if a sentence of length n is provable or not, just search all potential proofs of length less than F(n). But we know that provability is not decidable in axiom systems of the sort I'm talking about here.

Another is to construct explicit examples. The easiest method is to use standard tricks to create sentences that say things like this:

"This sentence has no proof with fewer than a googol symbols".

If our axiom system is consistent, we can show this sentence indeed has no proof with fewer than a googol symbols, and yet it can be proved - simply by listing all proofs with fewer than a googolplex symbols.

What I want to see is*mathematically natural*theorems whose only proofs are disgustingly long. There are some examples, but not enough.

For more:

https://johncarlosbaez.wordpress.com/2012/10/19/insanely-long-proofs/May 28, 2016 - What I would find very interesting indeed, and maybe this is what +Marco Devillers is really talking about, would be a measure of disgustingness that's less crude than mere length. Are there theorems out there with the following properties all at once?

(i) They have proofs that are not excessively long.

(ii) The only proofs are ones that "just happen to work" and that don't give any explanation at all about why the proof is true -- just a certificate of its truth.

Is it possible to formalize, and, even better, rigorously answer this question?

A possible candidate for such a theorem is the solution to the Robbins conjecture. This is the statement that certain axioms characterize Boolean algebras. The proof is not all that long, and simply consists of applying the axioms in an appropriate order until everything cancels down to what you want. So it's not that hard to follow the argument. But finding the argument in the first place took a huge computer search, and as far as I know nobody has an explanation for why it ended up being successful -- it just did.May 28, 2016 - In another discussion of this, Rich Schroeppel wrote,

"The Lucas-Lehmer test that M74207281 is prime requires 74M steps. Writing down the remainders of the X²-2 (mod P) iteration, at 22M digits each, would take 1.6Q characters. If we included the arithmetic to confirm each squaring step, another factor of 22M, we have 35 sextillion characters. We could reduce this a lot with Karatsuba or FFT multiplication, but we're still at 1.6Q * log2(74M) ~= 40 quadrillion characters."May 28, 2016 - +Timothy Gowers Something like that. I am myself am somewhat aware of short one axiom boolean bases over the Sheffer stroke.

I expect there are classes where you cannot do better than aggressive, admittedly short-sighted, bit-by-bit reasoning over the problem expressed as a boolean term.

Just calling it brute-force somewhere doesn't do justice to this approach. It's a somewhat novel manner of automated reasoning by lifting all you know about propositional logic; it's much more than dumb brute-force search. A substantial effort which opens up new mathematical tools.

And of course. Personally. Not a mathematician; math is what I can explain to a machine. Finite constructivism. Brouwer. Something like that. So, of course, I don't share your sensitivities. (I respect your view, of course.)May 28, 2016 - From a computational standpoint, Stampede is not normally used for very wide jobs (those using a large number of nodes all at once). That means its scheduling is such that smaller jobs often have a much easier time getting slotted in. This isn't even necessarily about priority, so much as things like small jobs being allowed to run for a long time, making it very hard to come up with a lot of nodes for a big job all at once.

All this is to say that if 800 nodes could do the job in 2 days, trying to run it on 1600 nodes might have added more than a day to the time spent waiting in the queue, blowing out the prospective savings.May 28, 2016 - Good to hear some details about Stampede!May 29, 2016

Add a comment...