Компьютер вывел математическое доказательство, слишком сложное для человека

Двое математиков русского происхождения из Ливерпуля, Алексей Лисица и Борис Конев, придумали интересную дилемму: что будет, если заставить компьютерную программу решить математическую задачу, но решение будет слишком сложным и длинным, чтобы его проверил человек?

Для примера ученые взяли так называемую Проблему несоответствия Эрдеша, сформулированную знаменитым венгерским математиком Полом Эрдешем (Paul Erdős). Задача построена вокруг поиска закономерности в бесконечном списке всего двух чисел "1" и "-1". Проблема возникает в тот момент, когда отсекается бесконечная последовательность, а затем создается конечная последовательность с использованием определенной константы. Сумма чисел и называется фигурой несоответствия.

Лисица и Конев ввели условия задачи с константой несоответствия "2" в компьютер со специальным программным обеспечение SAT-solvers ("Решатели задач выполнимости булевых формул"), которые предназначены для создания математических доказательств.

Компьютер выдал файл с решением математической проблемы, объем которого превышал на пару гигабайтов объем всей "Википедии". Очевидно, что человеку проверить это решение будет не под силу. И потому ученые задают вопрос всем своим коллегам: готовы ли мы настолько доверять компьютерам, чтобы они самостоятельно решали математические и другие логические задачи?

Подробнее ознакомиться с работой математиков можно, прочитав статью авторов исследования на сайте препринтов arXiv.org: http://arxiv.org/abs/1402.2184.

Роман, первое что приходит в голову, поручить проверить решение нескольким компьютерам ~ 5 - 10,
с разными блок-схемными конструкциями и программами.
Причем, предварительно прошедшими тест на решение известных математических задач.

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

Тесты на решение известных математических задач были бы убедительными.