Конечно, радостно, иначе было бы скучно. Только удивляюсь как Гильберт мог думать, что такой метод есть, даже для диофантовых уравнений    . Вот мне например ясно наперёд, что вероятность существования такого метода весьма невелика.

А иначе хаос для меня не есть отсутствие метода, тем более, что в шахматах такой в принципе есть - тот же полный перебор. Хаос вытворяется как раз однозначно и железно детерминированными системами    . Как говорят у нас, и один в трамвае буду кучковаться и толкаться

gennah в свое время уничижал методы компьютерной верификации доказательств тем, что пока комп медленно продвигается под твоим направлением, самому тебе станет все ясно и незачем компу дальше барахтаться. Однако комп барахтается для других заинтересованных, чтобы им показать, что доказательство твоё верное, а то у них нет ни времени, ни желания проверять детали твоей работы. А вот компу поверят на слово, ибо знают, что комп не ошибается по определению и конструкции. Все, что требуется от других, это лишь принять исходные посылки работы компа, дальше он сам дотянет (или не) до цели. Если дотянет - значит цель верная, если не дотянет - значит неверная, ясен пень   

В каком смысле? 

Афтоматизму не бывать, компы лишь орудия труда, вроде гаечного ключа 

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