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

Это решило старую проблему Рона Грэма. Доказательство было массивным аргументом грубой силы. Не чистая грубая сила, так как это было бы совершенно непрактично, а умное вычисление грубой силы с использованием решателя SAT. 2/

Но я довольно уверен, что это было сказано с юмором, а не (как предполагалось в статье Quanta) как какая-либо критика, поскольку я думаю сейчас, и думал тогда, что такие результаты довольно крутые. 4/

Шутка заключалась бы в предложении, что кто-то мог бы прочитать доказательство этого типа так, как будто это более традиционный вид аргумента, и сложные анализы случаев в традиционных аргументах обычно считаются несколько неэстетичными. 5/

Но, конечно, доказательство такого рода не предназначено для чтения в традиционном смысле и имеет свою собственную привлекательность. Лично я не против идеи использования хороших аргументов для сокращения доказательства до массивных вычислений, а затем выполнения этих вычислений. 6/

Похоже, есть некоторые проблемы, которые нельзя решить реалистично, кроме как с помощью такого подхода, в этом случае я не вижу причин не использовать его, и я доволен достигнутым уровнем понимания. 7/

Сказав это, если кто-то найдет доказательство теоремы четырех цветов (например), которое не требует огромного анализа случаев, я бы это отпраздновал и счел бы это шагом вперед в понимании, поскольку это объяснило бы, почему анализ случаев сработал.

что на данный момент я считаю чем-то, что просто имеет место быть. Точно так же, если кто-то найдет аргумент человеческого масштаба для проблемы Пифагоровых троек, я был бы в восторге. Но я очень сомневаюсь, что такой аргумент существует, и это меня не беспокоит. 9/9