Журнал Компьютерра -759   ::   Компьютерра

Многиеизвестные результаты неявно предполагаются, многие вроде бы

очевидные специалисту детали опускаются, и зачастую текст опирается на развитую интуицию профессионалов. Корректность

аргументов в доказательстве оценивается другими математиками, порою в неформальных дискуссиях. В результате развитие

математики превращается в некий социальный процесс в замкнутой среде.

Пока он был более-менее успешным. Ошибки в

математических текстах сравнительно редки, хотя известны примеры неверных утверждений, которые долгое время считались

правильными. Но в последние годы появился ряд таких длинных и сложных доказательств, что мало у кого достанет времени,

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

программы, которые, как известно, могут содержать ошибки. Так почему же предполагается, что их нет и в самих

доказательствах?

Чтобы обойти эти проблемы, программисты и математики еще с пятидесятых годов прошлого века стали

развивать область формальных доказательств. Доказательство кодируется на языке формальной логики, а специальная

программа проверяет его корректность. И кодировка доказательства, и программа его проверки тоже могут содержать ошибки,

но таких программ уже несколько и многократная проверка вселяет уверенность в надежности доказательства.