Математики Ливерпульского университета, Великобритания, задались вопросом – если компьютер создал доказательство математической задачи, слишком большое для изучения, как судить, насколько оно верное?
Вопрос, поднятый британскими математиками Алексеем Лисицей и Борисом Коневым, не является сугубо теоретическим – они создали компьютерную программу для решения малой части известной задачи несоответствия Эрдеша.
Уточним, что в ходе решения той или иной задачи математики порой исписывают целые тома доказательствами. Стремление переложить эту работу на компьютеры выглядит совершенно логичным.
Однако, теперь перед исследователями возникла проблема – результат работы программы, которую Конев и Лисица создали для решения несоответствия Эрдеша, занимает 13 Гб, что на 2 гигабайта больше полного объёма информации Википедии.
Перед математиками возникла дилемма: либо принять на веру доказательства, созданные машиной, либо отказаться от их использования, ограничивая тем самым возможности человечества.
Тем временем, исследователи Университетского колледжа Лондона доказали, что человеческий мозг воспринимает математические формулы точно так же, как и произведения искусства.