Problema del triplet booleano

El problema del triplet booleano és una qüestió relacionada en ternes pitagórico, que es va resoldre utilisant una prova assistida per ordenador en maig de 2016.

Este problema s'emmarca en la teoria de Ramsey, i formula la pregunta de si és possible colorear cada u dels sancers positius, ya siga de color roig o de color blau, de modo que cap triplet pitagórico dels sancers a, b i c, que satisfaça la condició $a^2+b^2=c^2$ siguen tots del mateix color. Per eixemple, en el triplet pitagórico 3, 4 i 5 ($3^2+4^2=5^2$), si 3 i 4 són de color roig, llavors 5 deu ser de color blau.

Marijn Heule, Oliver Kullmann i Victor Marek varen investigar el problema i varen demostrar que a lo manco existix un cas en el que tal coloració és impossible. Fins al número 7824 és possible colorear els números de modo que tots els triples pitagórico siguen admissibles, pero la prova mostra que dit color no es pot estendre per a també colorear el número 7825. Es va confirmar l'afirmació de la teorema, en el que s'afirma que:

El conjunt {1, . . . , 7824} pot ser separat en dos parts, de manera que cap de les dos continga una terna pitagórico, lo que és impossible per a {1, . . . , 7825}.

Hi ha 2⁷⁸²⁵ coloració possibles per als números fins a 7825. Estes possibles coloració es varen reduir llògica i algorítmicamente a al voltant d'un trilló de (encara altament complexos) casos, i es varen examinar utilisant un resolucionador de problemes de satisfacibilidad booleana. El desenroll de la prova va requerir aproximadament 4 anys de treball, aixina com dos dies de càlcul en el superordenador Stampede del Texas Advanced Computing Center. Va generar una prova proposicional de 200 terabytes, que es va comprimir a 68 gigaoctets.

El document que descriu la prova es va publicar en arXiv el 3 de maig de 2016, i va ser acceptat per a la conferència SAT 2016, a on va guanyar el premi al millor artícul.

En la década de 1980, el matemàtic Ronald Graham havia oferit un premi de 100 dólars per la resolució del problema, otorgat a Marijn Heule en 2016.