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. The image included in the paper shows a possible coloring scheme for that avoids monochromatic Pythagorean triples.
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 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 mathematics, the four color theorem, or the four color map theorem, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. Adjacent means that two regions share a common boundary of non-zero length. It was the first major theorem to be proved using a computer. Initially, this proof was not accepted by all mathematicians because the computer-assisted proof was infeasible for a human to check by hand. The proof has gained wide acceptance since then, although some doubts remain.
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.
Ramsey theory, named after the British mathematician and philosopher Frank P. Ramsey, is a branch of the mathematical field of combinatorics that focuses on the appearance of order in a substructure given a structure of a known size. Problems in Ramsey theory typically ask a question of the form: "how big must some structure be to guarantee that a particular property holds?"
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 and theoretical computer science, the monochromatic triangle problem is an algorithmic problem on graphs, in which the goal is to partition the edges of a given graph into two triangle-free subgraphs. It is NP-complete but fixed-parameter tractable on graphs of bounded treewidth.
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 combinatorial number theory, the Erdős–Graham problem is the problem of proving that, if the set of integers greater than one is partitioned into finitely many subsets, then one of the subsets can be used to form an Egyptian fraction representation of unity. That is, for every , and every -coloring of the integers greater than one, there is a finite monochromatic subset of these integers such that
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).
The mutilated chessboard problem is a tiling puzzle posed by Max Black in 1946 that asks:
Suppose a standard 8×8 chessboard has two diagonally opposite corners removed, leaving 62 squares. Is it possible to place 31 dominoes of size 2×1 so as to cover all of these squares?
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.
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.
