Problema booliano dos trios pitagóricos

O problema booliano dos trios pitagóricos é um problema relacionado aos trios pitagóricos que foi resolvido usando uma demonstração assistida por computador em maio de 2016.

Este problema é da teoria de Ramsey e pergunta se é possível colorir cada um dos inteiros positivos com as cores vermelho ou azul de modo que nenhum trio pitagórico de números inteiros a, b e c, sejam todos da mesma cor. Por exemplo, uma coloração com a e b vermelhos e c azul é uma coloração admissível, mas uma com os três em azul não seria.

A prova mostra que tal coloração é impossível. Até o número 7824 é possível colorir os números de tal forma que todos os triplos Pitagóricos sejam admissíveis, mas a demonstração mostra que nenhuma de tais colorações pode ser estendida para colorir também o número 7825. A afirmação feita pelo teorema provado é a seguinte:

Teorema —  O conjunto {1, . . . , 7824} pode ser particionado em duas partes, de modo que nenhuma delas contenha um trio pitagórico, embora isso seja possível para o conjunto {1, . . . , 7825}.

Há 2⁷⁸²⁵ colorações para os números até 7825. Estas colorações possíveis foram reduzidas logicamente a pouco menos de um trilhão de casos, e estes foram examinados utilizando um resolvedor de satisfatibilidade booliana. A criação da demonstração levou dois dias de execução no supercomputador Stampede no Texas Advanced Computing Center e gerou 200 terabytes de dados.

Na década de 1980, Ronald Graham ofereceu um prêmio de $100 para a solução do problema, que já foi dado a Marijn Heule. O artigo descrevendo a prova foi publicado no arXiv, em 3 de maio de 2016 e foi aceito para a conferência SAT 2016.