Знание-сила, 2008 № 06 (972)

Совершенно очевидно, что любое нетривиальное математическое доказательство опирается на массу утверждений, доказанных ранее, и прямое сведение к аксиомам обычно крайне трудно. Вообще говоря, в большинстве случаев это и не нужно: для доказательства утверждение сводят к уже доказанным фактам. Ключевой фактор для психологической убедительности такого метода состоит в том, что любой желающий может при желании разобраться до конца; конечно, под «любым желающим» уже давно подразумевается квалифицированный математик, но это не важно.

Важно другое. Современные математические доказательства становятся все сложнее и сложнее; они из явлений индивидуального опыта постепенно становятся явлениями опыта коллективного. Само понятие убедительности начинает терять этот индивидуальный оттенок — «если я захочу, я смогу разобраться до конца» — и все больше приобретает характер «коллективной убедительности». Доказательство становится убедительным не для отдельного математика, а для некоторого научного коллектива. Я могу проверить эту часть доказательства, но она опирается на утверждения, доказательства которых мне неизвестны; они известны другим моим коллегам, и я верю им, что эти доказательства правильны. Смысл коллективной убедительности в том, что для каждой составной части доказательства найдется свой «отвечающий за нее» член коллектива, для которого непосредственно убедительна именно эта часть (а другие участники полагаются на него в данном вопросе).

Непревзойденный пример такого доказательства — теорема о классификации конечных простых групп. Хотя отдельные небольшие кусочки этого доказательства несложно проверить квалифицированному алгебраисту, полностью его до недавнего времени понимали чуть ли не только его авторы. Однако приходилось верить, а иногда и пользоваться этим результатом.

Но и это еще не все. В наше время представления о доказательствах изменились еще и под влиянием вычислительной техники. Теперь мы умеем производить на свет доказательства, которые требуют перебора столь большого числа вариантов, что этот перебор становится недоступным человеку — а компьютеру доступен; либо же требуемые вычисления чересчур сложны, чтобы делать их вручную. Первым примером такого доказательства стало решение знаменитой проблемы четырех красок.

Даже в моей небогатой научной практике было уже два случая, когда в доказательстве математических фактов помогал компьютер. В одном случае мы написали программу, которая проводила вычисления в достаточно хитром кольце (через сведение к кольцу многочленов, конечно, но сведение тоже проводил компьютер). По результатам этих вычислений мы пришли к неким математическим выводам. Другой случай был даже более рафинированным: компьютер перебирал все возможные случаи, и на основе этого полного перебора, опираясь на то, что действительно все варианты были исследованы, мы доказали требуемую нижнюю оценку.

Можно ли считать, что в этих случаях мы получили доказательство? Бог с ними, с другими людьми, я сам, автор, могу быть уверен, что доказал что-то? А если я ошибся, когда писал программу? Программисты знают: вопрос не в том, есть ли в программе баги, а в том, когда они обнаружатся. А специалисты по верификации знают, что доказать корректность компьютерной программы зачастую гораздо сложнее, чем убедиться в корректности математического доказательства. Здесь не надо путать корректность алгоритма (как математического объекта) с корректностью самого кода программы: если проверить алгоритм обычно можно теми же методами, что и обычное доказательство, то анализ кода — очень сложная задача. И чтобы быть уверенным, что моя программа работает правильно, проверять надо именно код, а не идею алгоритма (она-то, конечно, и проверена, и в статьях изложена).

Под влиянием всех этих факторов у некоторых исследователей создается впечатление, что с развитием математики (в частности, с появлением все более и более сложных и длинных доказательств) доказательства теряют свое главное свойство — убедительность. Что же тогда остается от доказательства: ведь убедительность, казалось бы, — единственное, что от него требуется? Кроме того, с усложнением доказательства возрастает его элемент субъективности: математик уже не просто по собственной лености верит и не проверяет — он физически не способен этого сделать. Получается, что хотя все доказательства должны, по определению, быть убедительными, на деле одни из них (более простые) убедительнее других (более сложных). То есть простые доказательства как бы «в большей степени являются доказательствами», чем сложные! Из-за этого некоторые авторы начинают говорить чуть ли не о «болезни» современной математики (о кантовской болезни, продиагностированной Пуанкаре, они уже не вспоминают — видимо, перешла в хроническую фазу и лечению не подлежит).