約10年前、Marijn Heule、Oliver Kullmann、Victor Marekは、1から7825までの正の整数を2色にすると、x^2+y^2=z^2でx、y、zをすべて同じ色で見つけることができるに違いないことを証明しました。 1/

これにより、ロン・グラハムの古い問題が解決されました。その証拠は、大規模な総当たりの議論でした。純粋な総当たりではなく、まったく実現不可能だったため、SATソルバーを使用した巧妙な総当たり計算です。2/

しかし、私はそれがユーモラスな意味であり、(Quantaの記事で示唆されているように)いかなる種類の批判としてもなかったと確信しています。 4/

ジョークは、このタイプの証明をあたかもより伝統的な種類の議論であるかのように読むかもしれないという提案であり、従来の議論における複雑なケース分析は一般にやや醜いと見なされます。 5/

しかし、もちろん、この種の証明は従来の方法で読むように設計されておらず、独自の魅力があります。個人的には、優れた引数を使用して証明を大規模な計算に減らし、計算を行うという考えには問題ありません。 6/

このようなアプローチでなければ現実的に解決できない問題もあるようですが、その場合、使わない理由は見当たりませんし、結果として得られる理解度には満足しています。 7/

とはいえ、もし誰かが(例えば)大規模なケース分析を必要としない4色の定理の証明を見つけたら、私はそれを祝い、ケース分析がうまくいった理由を説明するので、理解の進歩と見なすでしょう、8/

今のところ、私はたまたまそうなったことだと考えています。同様に、誰かがピタゴラスの三重奏問題について人間規模の議論を見つけたら、私は喜ぶでしょう。しかし、私はそのような議論が存在するかどうか非常に疑問であり、それは私を気にしません。 9/9