Что такое доказательство.

Математики доказывают теоремы уже 2500 лет. Первым систематическим собранием доказательств были «Начала» Евклида (~300 до н.э.). Метод: аксиомы плюс правила вывода — теоремы. Каждый шаг проверяем. Цепочка необрываема. Это казалось идеальным фундаментом. Две тысячи лет математики строили на нём. Потом выяснилось, что фундамент неполный.

В 1931 году Курт Гёдель доказал: в любой достаточно мощной формальной системе есть истинные утверждения, которые нельзя доказать средствами этой системы. Математика не может доказать собственную непротиворечивость. Это не недостаток — это фундаментальное свойство.

Но задолго до Гёделя возник другой вопрос: что вообще значит «доказать»?

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

В XX веке математики попытались формализовать эту практику. Гильберт хотел записать всю математику в виде формальной системы — символов и правил манипуляции. Доказательство — последовательность символов, где каждый шаг следует из предыдущих по правилам. Человеческое понимание не нужно. Гёдель разрушил эту мечту. Но идея формального доказательства осталась.

Доказательство — это то, что убеждает разумного человека. Строгое доказательство — то, что убеждает даже неразумного человека. — Марк Кац, математик

В 1976 году Кеннет Аппель и Вольфганг Хакен доказали четырёхцветную теорему: любую карту можно раскрасить четырьмя цветами так, чтобы соседние страны имели разные. Математики пытались доказать это с 1852 года — 124 года. Аппель и Хакен доказали. Но их доказательство содержало проверку 1936 особых случаев, выполненную компьютером. Никакой человек не мог проверить каждый случай вручную1.

Математическое сообщество раскололось. Одни сказали: это доказательство, компьютер надёжен. Другие сказали: это не доказательство, мы не понимаем, почему оно истинно. Нет озарения. Нет инсайта. Только перебор.

Это философский вопрос о природе математического знания. Доказательство — это верификация истинности или понимание причины истинности?

Сегодня компьютерные доказательства стали мощнее. Proof assistants — Lean, Coq, Isabelle — позволяют записать доказательство формально, и компьютер проверяет каждый шаг2. В 2022–2023 годах математики верифицировали в Lean ключевые результаты Питера Шольца о perfectoid spaces — одни из сложнейших современных3.

Парадокс: формальное доказательство надёжнее человеческого. Люди делают ошибки. Компьютер — нет. Но формальное доказательство непонятно человеку напрямую. Его нужно «переводить» обратно в человеческий язык.

Есть и третий тип — вероятностное доказательство. Тест Миллера-Рабина проверяет простоту числа: если тест пройден — число простое с вероятностью больше 1 − 4^−k. Для криптографии достаточно. Для математики — нет4.

Что считать доказательством? Греки требовали понимания. Гильберт требовал формальности. Аппель и Хакен показали, что формальность и понимание могут расходиться. Гёдель показал, что даже формальность имеет предел.

Возможно, доказательство — это не свойство текста. Это отношение между текстом и сообществом, которое его читает. Доказательство — то, что математическое сообщество принимает как достаточное основание для уверенности. Социальный консенсус. Временный. Пересматриваемый.

Это не скептицизм — это честность.