Пара математиков из Ливерпульского университета (Великобритания), Алексей Лисица и Борис Конев, придумали любопытную проблемку – если компьютер приводит доказательство математической задачи, которое слишком велико для изучения, то как судить, насколько оно верное?
В своей статье в СМИ Лисица и Конев описывают написание и запуск компьютерной программы для решения малой части задачи, известной как задача несоответствия Эрдеша, сообщает phys.org.
Не станем вдаваться в математические дебри, лишь заметим, что математики, решая задачи, порой исписывают целые тома своими нетривиальными доказательствами. Любой, прошедший курс высшей математики, может это подтвердить.
Кажется понятным стремление исследователей переложить на надёжные плечи машин генерацию самых приземлённых частей своего творчества.
Математиков из Британии терзали сомнения, что когда-нибудь, в один из не самых прекрасных дней, компьютер будет работать очень долго, а результат его работы будет очень велик. И вот этот день настал.
Результат работы уникальной программы Конева и Лисицы поражает воображение – файл с текстом доказательства занимает объём в 13 гигабайт! А ведь это на два гигабайта больше, чем полный объём информации всей Википедии, отмечает gearmix.ru.
С настоящего момента перед научным миром возникла диллема: или принимать на веру доказательства, созданные машинами, как факт (хотя мы не в состоянии их проверить), либо отказаться от их использования, ограничивая тем самым наши возможности.
