Поиск блох попал в повестку дня только тогда, когда блохи совсем уж начали заедать: тот же Вейерштрасс был автором многих «странных» примеров, вроде примера непрерывной нигде не дифференцируемой функции. Один из величайших гениев в истории математики Анри Пуанкаре, кстати, очень не любил такие примеры, называл их «язвой», а кантовскую теорию множеств — естественное продолжение нового уровня строгости — считал «смертельной болезнью математики». Пуанкаре, конечно, простительно, хотя и он не без греха: четыре года был уверен, что доказал свою знаменитую гипотезу, и только потом нашел ошибку.
Не будем дальше излагать здесь историю понятия математического доказательства: к XX веку она плавно перетекает в историю матлогики, и не о ней сейчас речь, хотя история преинтересная, и в другой раз мы обязательно к ней вернемся. История попыток создания логических оснований математики — это даже не детектив, а остросюжетный триллер: Рассел пишет письмо Фреге, из-за которого последнему приходится срочно переписывать уже почти сданную в печать книгу, Гильберт прерывает курс матлогики, узнав о теореме Геделя о неполноте... но хватит, увлекся. Вернемся к нашим математикам, которых нужно убедить в истинности того или иного утверждения. В последнее время понятие доказательности снова начинает меняться...
Карл Вейерштрасс
Анри Пуанкаре
Совершенно очевидно, что любое нетривиальное математическое доказательство опирается на массу утверждений, доказанных ранее, и прямое сведение к аксиомам обычно крайне трудно. Вообще говоря, в большинстве случаев это и не нужно: для доказательства утверждение сводят к уже доказанным фактам. Ключевой фактор для психологической убедительности такого метода состоит в том, что любой желающий может при желании разобраться до конца; конечно, под «любым желающим» уже давно подразумевается квалифицированный математик, но это не важно.
Важно другое. Современные математические доказательства становятся все сложнее и сложнее; они из явлений индивидуального опыта постепенно становятся явлениями опыта коллективного. Само понятие убедительности начинает терять этот индивидуальный оттенок — «если я захочу, я смогу разобраться до конца» — и все больше приобретает характер «коллективной убедительности». Доказательство становится убедительным не для отдельного математика, а для некоторого научного коллектива. Я могу проверить эту часть доказательства, но она опирается на утверждения, доказательства которых мне неизвестны; они известны другим моим коллегам, и я верю им, что эти доказательства правильны. Смысл коллективной убедительности в том, что для каждой составной части доказательства найдется свой «отвечающий за нее» член коллектива, для которого непосредственно убедительна именно эта часть (а другие участники полагаются на него в данном вопросе).
Непревзойденный пример такого доказательства — теорема о классификации конечных простых групп. Хотя отдельные небольшие кусочки этого доказательства несложно проверить квалифицированному алгебраисту, полностью его до недавнего времени понимали чуть ли не только его авторы. Однако приходилось верить, а иногда и пользоваться этим результатом.
Но и это еще не все. В наше время представления о доказательствах изменились еще и под влиянием вычислительной техники. Теперь мы умеем производить на свет доказательства, которые требуют перебора столь большого числа вариантов, что этот перебор становится недоступным человеку — а компьютеру доступен; либо же требуемые вычисления чересчур сложны, чтобы делать их вручную. Первым примером такого доказательства стало решение знаменитой проблемы четырех красок.
Даже в моей небогатой научной практике было уже два случая, когда в доказательстве математических фактов помогал компьютер. В одном случае мы написали программу, которая проводила вычисления в достаточно хитром кольце (через сведение к кольцу многочленов, конечно, но сведение тоже проводил компьютер). По результатам этих вычислений мы пришли к неким математическим выводам. Другой случай был даже более рафинированным: компьютер перебирал все возможные случаи, и на основе этого полного перебора, опираясь на то, что действительно все варианты были исследованы, мы доказали требуемую нижнюю оценку.
Можно ли считать, что в этих случаях мы получили доказательство? Бог с ними, с другими людьми, я сам, автор, могу быть уверен, что доказал что-то? А если я ошибся, когда писал программу? Программисты знают: вопрос не в том, есть ли в программе баги, а в том, когда они обнаружатся. А специалисты по верификации знают, что доказать корректность компьютерной программы зачастую гораздо сложнее, чем убедиться в корректности математического доказательства. Здесь не надо путать корректность алгоритма (как математического объекта) с корректностью самого кода программы: если проверить алгоритм обычно можно теми же методами, что и обычное доказательство, то анализ кода — очень сложная задача. И чтобы быть уверенным, что моя программа работает правильно, проверять надо именно код, а не идею алгоритма (она-то, конечно, и проверена, и в статьях изложена).