Математики Борис Конев и Алексей Лисица, работающие в Ливерпульском университете, при помощи компьютера получили доказательство одной математической проблемы. Примечательно, что текст доказательства, выданный после шести часов работы программы, занимает 13 гигабайт, что превосходит объем англоязычной Википедии.

Проблема, над которой работали ученые, была сформулирована в 1930-е годы знаменитым венгерским математиком Палом Эрдёшем. Она известна под названием «задача Эрдёша о разбросе вдоль арифметических прогрессий». Он рассматривал бесконечные последовательности, состоящие из 1 и -1. Эрдёш предположил, что в такой последовательности можно выделить подпоследовательности, состоящие из чисел, порядковые номера которых образуют арифметическую прогрессию (то есть стоящих, например, на втором, четвертом, шестом и т.д. месте или же на третьем, шестом, девятом…), причем для любого натурального числа С найдется такая подпоследовательность, сумма чисел которой по модулю будет больше С. Доказательство, полученное учеными, касается случаев, когда С равно двум.

Получение доказательств математических теорем при помощи компьютера уже не новость. Еще в 1976 году американские математики прибегли к его помощи и решили знаменитую проблему четырех красок. Доказательство тогда заняло сотни страниц, но его всё-таки можно было проверить вручную. Несколько шокирующая новизна нынешнего результата состоит именно в том, что вряд ли его правильность способен проверить человек. Однако к такому развитию событий следовало бы быть готовыми. Для доказательства математических теорем в будущем будут всё чаще применяться компьютеры, а получаемые доказательства по объему вполне могут быть необозримыми для людей.