В 2014 году человечество вплотную подошло к ключевой точке своего развития. Мало того, что созданные нами машины обыгрывают лучших представителей человечества в шахматы, а роботы-хирурги с успехом заменяют человека при выполнении рутинных операций, так и ещё в одной сфере деятельности компьютеры обошли нас.

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

В своей статье, учёные описывают написание и запуск компьютерной программы для решения малой части задачи, известной как задача несоответствия Эрдеша.

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

Результат работы программы Лисицы и Конева поражает воображение – файл с текстом доказательства занимает объём в 13 гигабайт, т.е. 13,000,000,000 Байт!

Это на два гигабайта больше, чем полный объём информации в Википедии.

Теперь перед научным миром стоит дилемма: либо принимать на веру доказательства, созданные машинами, как факт (хотя мы не в состоянии их проверить), либо отказаться от их использования, ограничивая тем самым наши возможности.