Il y a environ dix ans, Marijn Heule, Oliver Kullmann et Victor Marek ont prouvé que si vous coloriez en 2 couleurs les entiers positifs de 1 à 7825, alors vous devez être en mesure de trouver x, y et z tous de la même couleur avec x^2+y^2=z^2 -- c'est-à-dire un triplet pythagoricien monochromatique. 1/

Cela a résolu un ancien problème de Ron Graham. La preuve était un argument massif de force brute. Pas de la pure force brute, car cela aurait été totalement infaisable, mais un calcul de force brute astucieux utilisant un solveur SAT. 2/

Mais je suis assez sûr que c'était censé être humoristique et non (comme suggéré dans l'article de Quanta) comme une sorte de critique, puisque je pense maintenant, et pensais alors, que ce genre de résultats est plutôt cool. 4/

La blague aurait été la suggestion que l'on pourrait lire une preuve de ce type comme s'il s'agissait d'un type d'argument plus conventionnel, et les analyses de cas compliquées dans les arguments conventionnels sont généralement considérées comme quelque peu laides. 5/

Mais bien sûr, une preuve de ce type n'est pas conçue pour être lue de manière conventionnelle et a son propre attrait. Personnellement, l'idée d'utiliser de bons arguments pour réduire une preuve à un calcul massif et ensuite effectuer le calcul me convient très bien. 6/

Il semble y avoir des problèmes qui ne peuvent être résolus de manière réaliste que par ce type d'approche, auquel cas je ne vois aucune raison de ne pas l'utiliser, et je suis satisfait du niveau de compréhension qui en résulte. 7/

Cela dit, si quelqu'un devait trouver une preuve du théorème des quatre couleurs (par exemple) qui ne nécessitait pas une énorme analyse de cas, je célébrerais cela et le considérerais comme un progrès dans la compréhension, car cela expliquerait pourquoi l'analyse de cas avait fonctionné, 8/

ce que je considère pour l'instant comme quelque chose qui se trouve simplement être le cas. De même, si quelqu'un devait trouver un argument à l'échelle humaine pour le problème des triplets pythagoriciens, je serais ravi. Mais je doute fortement qu'un tel argument existe, et cela ne me dérange pas. 9/9