Difference between revisions
boolean-pythagorean-triples
Status and infobox
- status:
—→ solved - tier:
—→ V3 - kind:
—→ problem - year:
—→ 1980 - statement:
—→ Can the positive integers be colored red and blue so that no Pythagorean triple is monochromatic?
Source +29 −0
+---
+title: Boolean Pythagorean triples problem
+kind: problem
+status: solved
+tier: V3
+year: 1980
+authors: Ronald Graham
+statement: Can the positive integers be colored red and blue so that no Pythagorean triple is monochromatic?
+space: combinatorics
+---
+No: the integers 1 to 7,825 cannot be colored that way, while 1 to 7,824 can. A SAT solver proved it and produced a 200-terabyte certificate that independent checkers verified. Graham paid the $100 prize he had offered. It is the pure form of a machine-verified prize.
+
+*Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.*
+
+Posed 1980s, Ronald Graham. Closed 2016, Marijn Heule, Oliver Kullmann and Victor Marek.
+
+## What would settle it
+
+DRAT proof certificate, independently checked
+
+## Prize
+
+$100 from Ronald Graham, paid
+
+## Sources
+
+- [Wikipedia: Boolean Pythagorean triples problem](https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem)
+
+[[Space:combinatorics|Combinatorics]] · [[Continent:mathematics|Mathematics]]
Revision 39 as rendered
No: the integers 1 to 7,825 cannot be colored that way, while 1 to 7,824 can. A SAT solver proved it and produced a 200-terabyte certificate that independent checkers verified. Graham paid the $100 prize he had offered. It is the pure form of a machine-verified prize.
Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.
Posed 1980s, Ronald Graham. Closed 2016, Marijn Heule, Oliver Kullmann and Victor Marek.
What would settle it
DRAT proof certificate, independently checked
Prize
$100 from Ronald Graham, paid