Longest maths proof would take 10 billion years to read

[Jim__]

From phys.org:

An Anglo-American trio presented the prize-winning solution to a 35-year old maths problem Friday, but verifying it may be a problem in itself: reading it would take 10 billion years.

"Boolean Pythagorean Triples" is not a shameful contagious disease, but a long-unsolved enigma within a field called Ramsey Theory.

...

It asks if it is possible to colour positive whole numbers (such as 1, 2 or 3) either red or blue such that no sequence of numbers that satisfy Pythagoras's famous equation—a² + b² = c²—are the same colour.

If a and b are red, for example, then c could be blue. But all three could not be blue or red.

[greiner3]

1. Where's Occam when you need him

[bvf]

2. I'm still waiting on news

re the abc conjecture.

[Lionel Mandrake]

3. This is not a proof.

Just as a search for odd perfect numbers may show that there are none less than some enormous number, such a result does prove that there are none at all.

[struggle4progress]

4. It may actually be a proof but one too long for human survey

My current understanding is that it exhibits a specific integer n > 0 such that every 2-coloring of the integers 0<= j <= n contains a monochromatic Pythagorean triple

If this is true, then any 2-coloring of the positive integers would induce a 2-coloring of the integers 0 <= j <= n and so would contain a monochromatic Pythagorean triple

The first part of their accomplishment is finding such a specific integer n > 0

Their n, however, is large enough that a brute computer search through all 2-colorings of the integers 0<= j <= n is infeasible

The second part of their accomplishment is an analysis that reduces the needed computer search to something feasible

The third part of their accomplishment is a program that performs the necessary reduced computer search

But it's still a monster computation by human standards: no human can directly verify the results of the reduced computer search

[Jim__]

5. Here is a link to their paper describing the proof.

This is a link to the paper that describes the proof.

The abstract from the paper:

Abstract.The boolean Pythagorean Triples problem has been a long-standing open problem in Ramsey Theory: Can the set N = {1; 2; ...} of natural numbers be divided into two parts, such that no part contains a triple (a; b; c) with a² + b² = c²? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisability proofs of SAT solvers, we produced and veried a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking