beroalПроблема, наверное, действительно «менее проблематична». Хотя есть и другие точки зрения. Вы, наверное, видели эту (популярную) статью:
http://elementy.ru/lib/431269?page_design=print («Теоремы софиста Горгия и современная математика»). Автор, видимо, пессимист. Так или иначе, проблема существует.
Не видел. Мне уже поздно читать научно-популярные статьи по математике.
Полагаю, вы про раздел «Третья теорема Горгия». Автор себя показывает как раз оптимистом:
Цитата:
Тут же поднялся шум — можно ли такому доказательству верить. Ведь большая часть доказательства проведена компьютером, а не человеком. «А вдруг компьютер ошибся?» — говорили такие недалекие люди.
…
И мне, например, кажется, что использование таких вот больших компьютерных переборов в доказательстве — это как раз не проблема. Почему? А вот по той же причине, которая на примере проблемы четырех красок уже проявилась — что к компьютерным доказательствам доверия гораздо больше, чем к человеческим, а не меньше.
Я говорил то же самое.
Неудобство длинного доказательства в следующем:
- 0) долго проверять;
- 1) трудно понимать.
Пункт 0 решаем, так как компьютер может проверять любые доказательства, которые есть в математике, а не только из теории графов. Загружай Coq или Mizar и валяй. Просто автор статьи об этой возможности не упомянул, может, просто не знал? Осталось только обучить математиков пользоваться этими программами. Это не проблема, потому что я же научился, не будучи математиком.
Я не знаю решение пункта 1. «Понимание» вообще трудно обсуждать. Особенно с некоторыми людьми, которые всегда уверены, что они всё
поняли правильно, а ты всё
понял неправильно. Стараюсь этого избегать.
