The Boolean Pythagorean triples problem is a problem from Ramsey theory about whether the positive integers can be colored red and blue so that no Pythagorean triples consist of all red or all blue members. The Boolean Pythagorean triples problem was solved by Marijn Heule, Oliver Kullmann and Victor W. Marek in May 2016 through a computer-assisted proof. [1]
The problem asks if it is possible to color each of the positive integers either red or blue, so that no Pythagorean triple of integers a, b, c, satisfying are all the same color.
For example, in the Pythagorean triple 3, 4 and 5 (), if 3 and 4 are colored red, then 5 must be colored blue.
Marijn Heule, Oliver Kullmann, and Victor W. Marek demonstrated that it is possible to partition the set into two subsets such that neither subset contains a Pythagorean triple. However, such a partition is not possible for the set . This result was achieved by analyzing a vast number of possible colorings, which initially amounted to about combinations.The researchers reduced this to around a trillion cases, which were then tested using a SAT solver. The computational process required approximately 4 CPU-years over two days on the Stampede supercomputer at the Texas Advanced Computing Center. The resulting proof, initially 200 terabytes in size, was compressed to 68 gigabytes.The findings were published in the SAT 2016 conference paper "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer," which received the best paper award.
In the 1980s Ronald Graham offered a $100 prize for the solution of the problem, which has now been awarded to Marijn Heule. [1]
As of 2018, the problem is still open for more than 2 colors, that is, if there exists a k-coloring (k ≥ 3) of the positive integers such that no Pythagorean triples are the same color. [2]
In computational complexity theory, co-NP is a complexity class. A decision problem X is a member of co-NP if and only if its complement X is in the complexity class NP. The class can be defined as follows: a decision problem is in co-NP if and only if for every no-instance we have a polynomial-length "certificate" and there is a polynomial-time algorithm that can be used to verify any purported certificate.
In mathematics, a Diophantine equation is an equation, typically a polynomial equation in two or more unknowns with integer coefficients, for which only integer solutions are of interest. A linear Diophantine equation equates to a constant the sum of two or more monomials, each of degree one. An exponential Diophantine equation is one in which unknowns can appear in exponents.
In computational complexity theory, NP is a complexity class used to classify decision problems. NP is the set of decision problems for which the problem instances, where the answer is "yes", have proofs verifiable in polynomial time by a deterministic Turing machine, or alternatively the set of problems that can be solved in polynomial time by a nondeterministic Turing machine.
A Pythagorean triple consists of three positive integers a, b, and c, such that a2 + b2 = c2. Such a triple is commonly written (a, b, c), a well-known example is (3, 4, 5). If (a, b, c) is a Pythagorean triple, then so is (ka, kb, kc) for any positive integer k. A triangle whose side lengths are a Pythagorean triple is a right triangle and called a Pythagorean triangle.
Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm that, for any given Diophantine equation, can decide whether the equation has a solution with all unknowns taking integer values.
Van der Waerden's theorem is a theorem in the branch of mathematics called Ramsey theory. Van der Waerden's theorem states that for any given positive integers r and k, there is some number N such that if the integers {1, 2, ..., N} are colored, each with one of r different colors, then there are at least k integers in arithmetic progression whose elements are of the same color. The least such N is the Van der Waerden number W(r, k), named after the Dutch mathematician B. L. van der Waerden.
In mathematics, the probabilistic method is a nonconstructive method, primarily used in combinatorics and pioneered by Paul Erdős, for proving the existence of a prescribed kind of mathematical object. It works by showing that if one randomly chooses objects from a specified class, the probability that the result is of the prescribed kind is strictly greater than zero. Although the proof uses probability, the final conclusion is determined for certain, without any possible error.
In combinatorics, Ramsey's theorem, in one of its graph-theoretic forms, states that one will find monochromatic cliques in any edge labelling (with colours) of a sufficiently large complete graph. To demonstrate the theorem for two colours (say, blue and red), let r and s be any two positive integers. Ramsey's theorem states that there exists a least positive integer R(r, s) for which every blue-red edge colouring of the complete graph on R(r, s) vertices contains a blue clique on r vertices or a red clique on s vertices. (Here R(r, s) signifies an integer that depends on both r and s.)
In graph theory, a branch of mathematics, list coloring is a type of graph coloring where each vertex can be restricted to a list of allowed colors. It was first studied in the 1970s in independent papers by Vizing and by Erdős, Rubin, and Taylor.
In discrete mathematics, Schur's theorem is any of several theorems of the mathematician Issai Schur. In differential geometry, Schur's theorem is a theorem of Axel Schur. In functional analysis, Schur's theorem is often called Schur's property, also due to Issai Schur.
A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.
In mathematics, the Herzog–Schönheim conjecture is a combinatorial problem in the area of group theory, posed by Marcel Herzog and Jochanan Schönheim in 1974.
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.
Van der Waerden's theorem states that for any positive integers r and k there exists a positive integer N such that if the integers {1, 2, ..., N} are colored, each with one of r different colors, then there are at least k integers in arithmetic progression all of the same color. The smallest such N is the van der Waerden numberW(r, k).
In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem. On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently.
In graph theory, the De Bruijn–Erdős theorem relates graph coloring of an infinite graph to the same problem on its finite subgraphs. It states that, when all finite subgraphs can be colored with colors, the same is true for the whole graph. The theorem was proved by Nicolaas Govert de Bruijn and Paul Erdős, after whom it is named.
7825 is the natural number following 7824 and preceding 7826.
Marienus Johannes Hendrikus Heule is a Dutch computer scientist at Carnegie Mellon University who studies SAT solvers. Heule has used these solvers to resolve mathematical conjectures such as the Boolean Pythagorean triples problem, Schur's theorem number 5, and Keller's conjecture in dimension seven.
