Boolean Pythagorean triples problem

rdf:langString Problema del triplete booleano

rdf:langString El problema del triplete booleano es una cuestión relacionada con ternas pitagóricas, que se resolvió utilizando una prueba asistida por ordenador en mayo de 2016.​ Este problema se enmarca en la teoría de Ramsey, y formula la pregunta de si es posible colorear cada uno de los enteros positivos, ya sea de color rojo o de color azul, de modo que ningún triplete pitagórico de los enteros a, b y c, que satisfaga la condición sean todos del mismo color. Por ejemplo, en el triplete pitagórico 3, 4 y 5, si 3 y 4 son de color rojo, entonces 5 debe ser de color azul. Marijn Heule, Oliver Kullmann y Victor Marek investigaron el problema y demostraron que al menos existe un caso en el que tal coloración es imposible. Hasta el número 7824 es posible colorear los números de modo que todos los triples pitagóricos sean admisibles, pero la prueba muestra que dicho color no se puede extender para también colorear el número 7825. Se confirmó la afirmación del teorema, en el que se afirma que: Hay 27825 coloraciones posibles para los números hasta 7825. Estas posibles coloraciones se redujeron lógica y algorítmicamente a alrededor de un trillón de (aún altamente complejos) casos, y se examinaron utilizando un resolucionador de problemas de satisfacibilidad booleana. El desarrollo de la prueba requirió aproximadamente 4 años de trabajo, así como dos días de cálculo en el superordenador Stampede del . Generó una prueba proposicional de 200 terabytes, que se comprimió a 68 gigabytes. El documento que describe la prueba se publicó en arXiv el 3 de mayo de 2016,​ y fue aceptado para la conferencia SAT 2016, donde ganó el premio al mejor artículo.​ En la década de 1980, el matemático Ronald Graham había ofrecido un premio de 100 dólares por la resolución del problema, otorgado a Marijn Heule en 2016.​