Problème des triplets booléens de Pythagore

Le problème consiste à savoir s'il est possible de colorier chacun des entiers positifs en rouge ou en bleu, de sorte qu'aucun triplet de Pythagore d'entiers a, b, c, satisfaisant ${\displaystyle a^{2}+b^{2}=c^{2}}$ soient tous de la même couleur.

Par exemple, dans le triplet de Pythagore 3, 4 et 5 ( ${\displaystyle 3^{2}+4^{2}=5^{2}}$ ), si 3 et 4 sont colorés en rouge, alors 5 doit être coloré en bleu.

Marijn Heule, Oliver Kullmann et Victor W. Marek ont montré qu'une telle coloration n'est possible que jusqu'au nombre 7824. L'énoncé réel du théorème prouvé est

Il existe 2⁷⁸²⁵ ≈ 3.63×10²³⁵⁵ combinaisons de couleurs possibles pour les nombres jusqu'à 7825 . Ces colorations possibles ont été logiquement et algorithmiquement réduites à environ un billion de cas (toujours très complexes), et celles-ci ont été examinées à l'aide d'un solveur booléen de satisfiabilité. La création de la preuve a nécessité environ 4 années CPU de calcul sur une période de deux jours sur le supercalculateur Stampede du Texas Advanced Computing Center et a généré une preuve propositionnelle de 200 téraoctets, qui a été compressée à 68 gigaoctets.

L'article décrivant la preuve a été publié lors de la conférence SAT 2016[2], où il a remporté le prix du meilleur article[3]. La figure ci-dessous montre une famille possible de colorations pour l'ensemble {1,...,7824} sans triplet de Pythagore monochromatique, et les carrés blancs peuvent être colorés en rouge ou en bleu tout en satisfaisant à cette condition.

Dans les années 1980 , Ronald Graham a offert un prix de 100 $ pour la solution du problème, qui a maintenant été décerné à Marijn Heule[1].

Depuis 2018, le problème est toujours ouvert pour plus de 2 couleurs, c'est-à-dire s'il existe une k-coloration ( k ≥ 3) des entiers positifs telle qu'aucun triplet de Pythagore n'est de la même couleur[4].

• Liste des longues preuves mathématiques