T3.JPGBoolean Pythagorean Triples problem is, can the set N = {1,2,. . .} of natural numbers be divided into two parts, such that no part contains a Pythagorean triple (a; b; c) with (a^2 + b^2 = c^2) ?  In the 1980s, Ronald Graham offered a prize for anyone who could solve it.  Mathematicians Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek solved and verified the Boolean Pythagorean Triples problem via Cube-and-Conquer paradigm(C&C).  Exploiting recent progress in unsatisfiability proofs of SAT solvers (Propositional satisfiability), these 3 Mathematicians produced and verified a proof in the DRAT(Deletion Resolution Asymmetric Tautology) format, which is almost 200 terabytes in size.  In simple terms the question ‘Can the set of natural numbers be divided into two parts such that no part contains a Pythagorean Triple?’ answered in 200 terabytes.  No Mathematical proof of this size existed ever before.  A fundamental question is whether the Theorem has a mathematical(human-readable) proof, or whether the gigantic(sophisticated) case-distinction, which is at the heart of this proof, is the best there is?  What they just proved is the set {1, . . ., 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . ., 7825}.  Previous best result was partition by Joshua Cooper and Ralph Overstreet of the set {1; . . . ,7664} into two parts.

 

https://arxiv.org/pdf/1605.00723v1

Advertisements