kouzdra at По поводу пресловутого "доказательства Перельмана которое никто не может проверить":Забавная статья по поводу давно зреющей и наконец созревшей и перезревшей проблемы:
Брайан Дэвис. Куда движется математика?
... В 1970-е годы более сотни специалистов по теории групп образовали своеобразный консорциум, целью которого было представить полную классификацию простых конечных групп... Под общим руководством Даниэля Горенштейна проблема была разбита на «пакеты» задач, которые поручили различным группам математиков всего мира. Через десять лет интенсивной работы удалось составить полную классификацию всех простых конечных групп, состоящую из трех бесконечных счетных семейств и 26 так называемых спорадических групп с особыми свойствами. Существование спорадической группы с самым большим порядком, получившей прозвище «монстр», удалось доказать только при помощи компьютера...
В 1980-е годы случилось нечто не менее интересное, чем сама классификация групп. Сначала произошел внешне позитивный сдвиг: вроде бы удалось найти метод доказательства существования «монстра» без использования компьютера. Было решено объединить усилия различных групп математиков для проведения массированной проработки нащупанного доказательства, но вместо ожидаемого результата было выявлено множество пробелов в ранее принятых доказательствах.
Большую часть дыр удалось залатать, но одна оказалась настолько серьезной, что заявления о том, что получена полная классификация простых конечных групп, были в 1990 году признаны преждевременными. Со временем этот пробел был заполнен доказательством Ашбахера и Смита, и опять тогда казалось, что доказательство вполне корректно.
Интересно, что из двадцати томов этого окончательного доказательства до сих опубликованы лишь неполные пять, и это спустя четверть века после того, как теорема была «доказана». Михаэль Ашбахер, один из самых заинтересованных участников проекта, не исключает, что в один прекрасный день может быть открыта новая простая конечная группа. Если ее характеристики окажутся родственными характеристикам какой-либо из известных групп, это еще не страшно. Однако Ашбахер не исключает и возможности открытия принципиально новой простой конечной группы, и тогда всю работу по их классификации можно начинать заново. Отметим также, что и Жан-Пьер Серр весьма скептически относится к полноте и корректности имеющегося доказательства.
Ашбахер считает доказательство «внешне достаточно крепким». Под этим он подразумевает, что выявленные недостатки пока что удавалось исправлять за счет умеренных объемов дополнительной работы, не затрагивая основной линии доказательства. К сожалению, это не означает, что доказательство корректно.
Сила любого доказательства определяется слабейшим из его звеньев, и тот факт, что до сегодняшнего дня выпадавшие звенья удавалось относительно безболезненно заменять новыми, не гарантирует, что это будет раз за разом удаваться и в дальнейшем. Если представить себе такое доказательство в виде сети, в которой разрыв отдельных нитей не угрожает целостности всей сети, то нельзя исключить, что где-то в этой сети осталась дыра, достаточно большая для того, чтобы муха смогла через нее проползти. Подавляющее большинство мух (в нашем случае — простых конечных групп) поймано, но не обязательно все.
...
Что касается завершения проекта окончательной классификации конечных групп (в смысле публикации исчерпывающего итогового доклада), то оно находится под угрозой срыва в связи с выбытием из строя ведущих участников в силу естественных возрастных причин.
Еще лет десять, и большинство из них уйдет из жизни или из математики, и останется слишком мало ученых, достаточно глубоко понимающих проблему, чтобы завершить классификацию. Но даже если проект увенчается исчерпывающим итоговым докладом, в мире, наверное, не найдется и десяти математиков, которые будут вправе утверждать, что они понимают хотя бы основные линии многотомного доказательства.
Забавно что окончательные выводы автора являются очевидной туфтой именно по итогам сравнения с проводимыми им аналогиями с программированием, которое с подобными проблемами столкнулось гораздо раньше - в программировании как раз сохранение у программы возможности "понимания ее сути" ("обозримости кода") является одним из требований к технологии и в общем за прошедшее время с его выполнением более или менее научились справляться. Судя по мнению автора, математики до этого еще не дозрели и "возможность одному человеку понять доказательство" воспринимают в философском ("интуитивно убедительное доказательство") а не инструментальном (без понимания структуры и логики программы ее дальнейшее развитие крайне затрудняется - потому есть смысл избегать чрезмерной сложности даже ценой некоторых потерь и вкладывать силы и средства в разработку выразительных средств, позволяющих уменьшить сложность).
То есть полудоказательные системы написания кода (те же системы типов) - все-таки отчасти способ автоматизации рутинной работы, в первую очередь - способ структурирования мышления и повышения отчуждаемости кода (типизация гарантирует соответствие программы хотя бы некоторым формальным правилам, которые являются общими для всех разработчиков) и вовсе не ставят целью подмену понимания кода программистом.
Это в основном средство снижения сложности.
* * *
... математика столкнулась с проблемой практически непреодолимой сложности доказательств. Решение важной задачи, которая формулируется в нескольких предложениях, может занимать десятки тысяч страниц, что фактически делает невозможным его полную запись и понимание.
В заключении своей статьи Брайан Дэвис так описывает характер происходящих в математике изменений. «В 1875 году каждый человек, способный к математике, мог за несколько месяцев полностью разобраться в доказательстве большинства известных теорем. К 1975 году ... математики еще могли полностью понять доказательство любой доказанной теоремы. К 2075 году многие области чистой математики будут зависеть от теорем, которые не понимает никто из математиков — ни индивидуально, ни коллективно. ... Обычным делом станет формальная верификация сложных доказательств, но при этом будет много результатов, признание которых будет основано на социальном консенсусе в не меньшей мере, чем на строгом доказательстве».
Подобно инженерам, математики станут говорить не о твердом знании, а о степени уверенности в надежности своих результатов. Это может сблизить математику с другими дисциплинами и, возможно, приведет к снятию философского вопроса об особом онтологическом статусе математических объектов.