Близько десяти років тому Марійн Хойл, Олівер Куллманн і Віктор Марек довели, що якщо ви двоколірні додатні цілі числа від 1 до 7825, то ви повинні бути в змозі знайти x, y і z одного кольору з x^2+y^2=z^2 - тобто монохроматичну піфагорову трійку. 1/

Це вирішило стару проблему Рона Грема. Доказом став масовий аргумент грубої сили. Не чиста груба сила, оскільки це було б абсолютно нездійсненно, а розумне обчислення грубої сили з використанням розв'язувача SAT. 2/

Але я майже впевнений, що це було задумано з гумором, а не (як запропоновано в статті Quanta) як якась критика, оскільки я думаю зараз і думав тоді, що такі результати досить круті. 4/

Жартома було б припущення, що доказ такого типу можна читати так, ніби це більш традиційний вид аргументації, а складний аналіз випадків у звичайних аргументах зазвичай вважається дещо негарним. 5/

Але, звичайно, доказ такого роду не призначений для прочитання загальноприйнятим способом, а має свій власний вид привабливості. Особисто мене влаштовує ідея використовувати гарні аргументи, щоб звести доведення до масивного обчислення, а потім виконувати обчислення. 6/

Виявляється, є деякі проблеми, які реально не можуть бути вирішені інакше, ніж за допомогою такого підходу, і в цьому випадку я не бачу причин не використовувати його, і я задоволений отриманим рівнем розуміння. 7/

Тим не менш, якби хтось знайшов доказ чотириколірної теореми (наприклад), який не вимагав би великого аналізу випадку, я б відзначив це і розглядав це як прогрес у розумінні, оскільки це пояснювало, чому аналіз випадку спрацював, 8/

що поки що я розцінюю як щось, що просто випадково так і є. Так само, якби хтось знайшов аргумент людського масштабу для задачі піфагорійських трійок, то я був би в захваті. Але я дуже сумніваюся, що такий аргумент існує, і це мене не турбує. 9/9