Доказательства: методы

1976. Иллинойс. Аппель и Хакен после пяти лет работы запускают IBM мейнфрейм. 1936 часов процессорного времени. 400 страниц кейсов. Первое доказательство теоремы о четырёх цветах, которое человек физически не может проверить руками. Математика никогда не будет прежней - и именно три метода из этого урока лежат в основе каждого шага той машинной верификации.

• **Lean4 и mathlib**: более 100 000 машинно-верифицированных теорем. За каждой - вариант прямого доказательства или индукции, записанный в синтаксис proof assistant
• **Нижние границы алгоритмов:** доказательство «сортировка сравнениями требует не менее n*log(n)» - классическое «от противного» через дерево решений. Это почему QuickSort нельзя ускорить принципиально
• **Безопасность:** доказательство, что RSA не взламывается за полиномиальное время - тоже от противного: если взломать, то разложить на множители, но это NP-hard

Предварительные знания

• Предикатная логика

Прямое доказательство: цепочка следствий

Прямое доказательство - это логический конвейер: берём гипотезу P, прогоняем через цепочку известных фактов, на выходе получаем Q. Никакой магии - только применение определений, лемм, алгебраических тождеств. Именно так работает 90% доказательств корректности алгоритмов в production-коде: предусловие передаётся через инварианты к постусловию.

**Структура прямого доказательства:** 1. Допускаем, что **P** истинно (гипотеза) 2. Применяем определения, леммы, алгебрические преобразования 3. Приходим к утверждению **Q** Форма: P -> A1 -> A2 -> ... -> Q

В анализе алгоритмов прямые доказательства - повсюду. Жадный алгоритм: «выбор на шаге k не хуже оптимального» -> «итоговое решение не хуже оптимального». Каждая стрелка в этой цепочке - прямое доказательство одного небольшого факта. Именно так Дейкстра доказывал корректность своего алгоритма - и именно так это делается в формальных спецификациях вроде TLA+.

**Как начать прямое доказательство:** запишите гипотезу в явном виде через определения. Доказываете «n чётное -> ...» - сразу пишите n = 2k. Это «разворачивание» определения - первый шаг почти каждого прямого доказательства. Пропустили этот шаг - дальше идти некуда.

Доказательство от противного: reductio ad absurdum

Евклид доказал иррациональность корня из двух этим методом ещё в IV веке до н.э. Тот же приём - в доказательстве нижней границы сортировки O(n log n), в невозможности решить проблему остановки, в P vs NP аргументах. Логический айкидо: принять, что противник прав, и показать, что это ведёт к абсурду.

**Структура доказательства от противного:** 1. Предполагаем **не-Q** (отрицание того, что хотим доказать) 2. Проводим рассуждения, используя и P, и не-Q 3. Получаем противоречие (например, «X и не-X») 4. Делаем вывод: не-Q ложно -> Q истинно QED

В computer science «от противного» - стандартный инструмент для нижних границ и невозможности. Доказательство того, что сортировка сравнениями требует не менее n*log(n) операций - именно противоречие через дерево решений: если алгоритм делает меньше, дерево слишком мало и не может различить все n! порядков. DeepMind AlphaProof решал задачи IMO 2024 через автоматический поиск именно таких противоречий.

**Частая ошибка:** путать «от противного» с «контрапозитивом». - **От противного** - предполагаем не-Q и ищем противоречие (с P или само с собой) - **Контрапозитив** - доказываем «не-Q -> не-P» напрямую (без поиска противоречия) Оба метода доказывают «P -> Q», но структура рассуждений разная.

**Когда выбирать доказательство от противного:** если нужно доказать «не существует», «невозможно», «не более» - «от противного» часто элегантнее прямого. Предполагаете существование или возможность, приходите к нелепице. Wiles доказал теорему Ферма в 1995 году - 129 страниц, 7 лет в тайне, одна ошибка, год патча. Математическое доказательство - единственная вещь, которая не имеет права быть «почти верной».

Контрапозитив: доказываем обратное

Контрапозитив - элегантный трюк: «P -> Q» логически эквивалентно «не-Q -> не-P». Это не «от противного» - нет никакого предположения и поиска нелепицы. Просто прямое доказательство другого утверждения, которое случайно эквивалентно исходному. Когда гипотеза P неудобна, а отрицание заключения не-Q даёт хорошую отправную точку - переворачиваем стрелку.

**Контрапозитив:** P -> Q эквивалентно не-Q -> не-P Эти две импликации логически тождественны (проверяется таблицей истинности). Доказав одну, автоматически доказывается другая. **Стратегия:** если гипотеза «P» сложна для работы, а отрицание заключения «не-Q» даёт более удобную отправную точку - используйте контрапозитив.

**Мнемоника:** контрапозитив - «переворачиваем и отрицаем». P->Q становится не-Q->не-P: стрелка меняет направление, оба утверждения отрицаются. Ни «Q->P» (конверс), ни «не-P->не-Q» (инверс) - не эквивалентны исходному. Только контрапозитив.

Математическая индукция: доказательство для всех n

Математическая индукция - инструмент для утверждений вида «для всех n >= n0: P(n)». Проверяем базу P(n0), показываем «если P(k) верно, то P(k+1) тоже верно» - и по принципу домино утверждение истинно для всех n. Lean4 и Coq ежедневно верифицируют тысячи теорем именно через индукцию - только автоматически. Lean4 содержит более 100 тысяч машинно-верифицированных теорем в mathlib. За каждой - вариант этой конструкции.

**Структура доказательства по индукции:** 1. **База:** доказываем P(n0) непосредственно 2. **Шаг:** предполагаем P(k) (индукционная гипотеза) и доказываем P(k+1) 3. **Вывод:** по принципу математической индукции P(n) верно для всех n >= n0 **Сильная индукция:** в шаге предполагаем P(n0), P(n0+1), ..., P(k) и доказываем P(k+1).

**Сильная индукция** используется там, где шагу нужны не только P(k), но и предыдущие результаты. Классический пример: у каждого числа n >= 2 есть простой делитель. Если n простое - сам делитель. Иначе n = a*b где a, b < n, и по индукционной гипотезе у a есть простой делитель, который делит и n. Этот приём лежит в основе доказательства основной теоремы арифметики.

**Частые ошибки при индукции:** - **Пропустить базу** - без неё цепочка домино не начнётся. Пример: «все числа равны» звучит как теорема, которую можно «доказать» неверным шагом, но база провалится. - **Использовать P(k+1) для доказательства P(k+1)** - круговое рассуждение. - **Неверная формулировка инд. гипотезы** - предполагаем не то, что нужно для шага.

**Индукция в алгоритмах:** каждый рекурсивный алгоритм неявно доказывает свою корректность по индукции. База - базовый случай (n=0 или n=1). Шаг - «если рекурсивный вызов для меньшего n корректен, то вся функция корректна». Написав рекурсивный алгоритм, уже мыслишь индуктивно - просто без явной формализации.

Ключевые идеи

• **Прямое доказательство:** P -> A1 -> ... -> Q. Первый шаг - развернуть определение гипотезы. Применяется для большинства позитивных утверждений.
• **От противного:** предположить не-Q, прийти к противоречию. Идеально для доказательств невозможности и нижних границ. Тем же методом Евклид доказал иррациональность корня из 2.
• **Контрапозитив:** P->Q эквивалентно не-Q->не-P. Если с не-Q работать удобнее, чем с P - переворачиваем стрелку.
• **Математическая индукция:** база + шаг (P(k) -> P(k+1)) = доказательство для всех n. Каждый рекурсивный алгоритм неявно использует этот принцип.
• **Lean4/Coq**: те же четыре метода, записанные машиночитаемо. Proof assistants проверяют их механически - 1936 часов CPU Аппеля и Хакена теперь занимают секунды.

Связанные темы

Методы доказательств - сквозной инструмент всей дискретной математики:

• Предикатная логика — Доказательства работают с кванторами: «для всех n» - это для-всех, «существует x» - существует
• Комбинаторика — Формулы перестановок и сочетаний доказываются по индукции или прямым построением биекции
• Теория графов — Корректность алгоритмов обхода графа (BFS, DFS) доказывается через инварианты и индукцию

Вопросы для размышления

• Реализован рекурсивный алгоритм merge sort. Как сформулировать его инвариант и структуру доказательства по индукции?
• Придумайте утверждение о структуре данных (например, о куче или BST), которое удобнее доказывать контрапозитивом, а не прямым методом.
• Почему доказательство «корень из 2 иррационален» нельзя заменить вычислением 10000 знаков после запятой?

Связанные уроки

• dm-03 — Предикатная логика - язык, на котором записываются доказательства
• dm-05 — Комбинаторные тождества доказываются по индукции
• dm-12 — Корректность BFS/DFS через инварианты и структурную индукцию
• ml-04 — Формальные системы - математический фундамент методов доказательств
• prob-01-intro — Аксиомы Колмогорова - пример прямой аксиоматики из трёх строк
• alg-01-big-o