Математики просят помощи
Важные проблемы современного состояния математики поднимает декабрьский выпуск журнала Notices of the American Mathematical Society, центральная тема которого посвящена формальным доказательствам.
Как известно, нет ничего надежнее строго доказанной математической теоремы. Она может быть бесполезна, а аксиомы, из которых она выведена, могут не иметь никакого отношения к реальности, однако в абсолютной надежности формального логического вывода никто не сомневается. Этому порой завидуют представители естественных наук, критерий истины в которых не формальная логика, а зачастую не слишком надежный опыт.
Но в последние десятилетия и в привилегированной касте математиков появились сомнения. Что такое строгое математическое доказательство в научной статье или книге? Оно написано человеком и для человека. Хуже того, специалистом и для специалиста. И где гарантии, что в нем нет ошибок? Аргументы в статье излагаются в повествовательной форме, облегчающей их восприятие. Многие известные результаты неявно предполагаются, многие вроде бы очевидные специалисту детали опускаются, и зачастую текст опирается на развитую интуицию профессионалов. Корректность аргументов в доказательстве оценивается другими математиками, порою в неформальных дискуссиях. В результате развитие математики превращается в некий социальный процесс в замкнутой среде.
Пока он был более-менее успешным. Ошибки в математических текстах сравнительно редки, хотя известны примеры неверных утверждений, которые долгое время считались правильными. Но в последние годы появился ряд таких длинных и сложных доказательств, что мало у кого достанет времени, квалификации и энергии, чтобы их как следует проверить. Хуже того, некоторые доказательства опираются на компьютерные программы, которые, как известно, могут содержать ошибки. Так почему же предполагается, что их нет и в самих доказательствах?
Чтобы обойти эти проблемы, программисты и математики еще с пятидесятых годов прошлого века стали развивать область формальных доказательств. Доказательство кодируется на языке формальной логики, а специальная программа проверяет его корректность. И кодировка доказательства, и программа его проверки тоже могут содержать ошибки, но таких программ уже несколько и многократная проверка вселяет уверенность в надежности доказательства. В последние годы программы проверки доказательств стали достаточно мощными, чтобы справляться со сложными теоремами. К сожалению, формальная запись доказательства пока получается примерно в четыре раза длиннее обычной и требует примерно неделю муторной напряженной работы, чтобы формализовать одну страницу. И надо очень любить математику и программирование, чтобы этим заниматься. Тем более что славы проверка известных теорем не приносит. Впрочем, программы совершенствуются, и, возможно, в недалеком будущем запись формального доказательства станет не намного труднее записи обычного. А редакции математических журналов не станут рассматривать статьи без приложения формальных записей сформулированных в них теорем.