Sekitar sepuluh tahun yang lalu Marijn Heule, Oliver Kullmann dan Victor Marek membuktikan bahwa jika Anda mewarnai bilangan bulat positif dari 1 hingga 7825, maka Anda harus dapat menemukan x, y dan z semuanya dengan warna yang sama dengan x^2+y^2=z^2 -- yaitu, triple Pythagoras monokromatik. 1/

Ini memecahkan masalah lama Ron Graham. Buktinya adalah argumen brute-force yang besar. Bukan brute force murni, karena itu sama sekali tidak layak, tetapi perhitungan brute-force yang cerdas menggunakan pemecah SAT. 2/

Tapi saya cukup yakin itu dimaksudkan secara lucu dan bukan (seperti yang disarankan dalam artikel Quanta) sebagai kritik apa pun, karena saya berpikir sekarang, dan berpikir saat itu, bahwa hasil semacam ini cukup keren. 4/

Lelucon itu akan menjadi saran bahwa seseorang mungkin membaca bukti jenis ini seolah-olah itu adalah jenis argumen yang lebih konvensional, dan analisis kasus yang rumit dalam argumen konvensional umumnya dianggap agak jelek. 5/

Tetapi tentu saja bukti semacam ini tidak dirancang untuk dibaca dengan cara konvensional, dan memiliki daya tariknya sendiri. Secara pribadi, saya baik-baik saja dengan gagasan menggunakan argumen yang bagus untuk mengurangi bukti menjadi komputasi besar-besaran dan kemudian melakukan perhitungan. 6/

Tampaknya ada beberapa masalah yang tidak dapat diselesaikan secara realistis kecuali dengan pendekatan semacam ini, dalam hal ini saya tidak melihat alasan untuk tidak menggunakannya, dan saya senang dengan tingkat pemahaman yang dihasilkan. 7/

Meskipun demikian, jika seseorang menemukan bukti teorema empat warna (misalnya) yang tidak memerlukan analisis kasus yang besar, saya akan merayakannya dan menganggapnya sebagai kemajuan dalam pemahaman, karena itu akan menjelaskan mengapa analisis kasus berhasil, 8/

yang untuk saat ini saya anggap sebagai sesuatu yang kebetulan terjadi. Demikian juga, jika seseorang menemukan argumen skala manusia untuk masalah Pythagoras-triples maka saya akan senang. Tapi saya sangat meragukan bahwa argumen seperti itu ada, dan itu tidak mengganggu saya. 9/9