Math Logic на собеседовании

2024 год: алгоритм DeepMind AlphaProof решает задачи IMO в формальной системе Lean. 2026: каждый коммит в Rust компилятор - это микро-доказательство теоремы о памяти. Логика перестала быть кабинетной дисциплиной - она в каждом npm install (SAT solver), в каждом type checker (Curry-Howard), в каждой proof-of-stake транзакции (formal verification).

• AlphaProof (DeepMind 2024) - серебро IMO через Lean 4 + LLM + RL
• Rust borrow checker - линейная логика на уровне компилятора, безопасность памяти по построению
• AWS S2N TLS - формально верифицированный криптокод (SAW + Cryptol), баги пойманы до продакшна
• Lean Copilot (Stanford 2024) - LLM-подсказки тактик для формальных доказательств в Mathlib

Техники доказательства: набор инструментов на собес

На техническом интервью часто звучит фраза «докажите корректность». Без набора стандартных техник любая содержательная задача превращается в перебор частных случаев. Базовый арсенал: **прямое доказательство** (из посылок к выводу), **от противного** (предположим обратное и придём к лжи), **математическая индукция** (база и шаг), **контрапозиция** ($A \to B$ эквивалентно $\neg B \to \neg A$), **конструктивное доказательство** (явно построим объект), **принцип Дирихле** (pigeonhole).

**Классика интервью.** Иррациональность $\sqrt{2}$ - доказательство от противного: предположение $\sqrt{2} = p/q$ в несократимой форме приводит к чётности и $p$, и $q$. Бесконечность простых (Евклид) - конструкция: для любого конечного набора $\{p_1, \ldots, p_n\}$ число $p_1 \cdot p_2 \cdots p_n + 1$ даёт новый простой делитель. Канторов диагональный аргумент - конструкция строки, отличающейся от каждой в перечислении.

Выбор техники определяется структурой задачи. Утверждение «не существует X со свойством Y» естественно идёт через противоречие. Утверждение «для всех $n$ верно P(n)» - кандидат на индукцию. «Существует объект с особым свойством» - конструкция. Опытный решающий за минуту прикидывает 2-3 техники и выбирает самую короткую.

**ML-применение.** Корректность mergesort и BFS доказывается индукцией по длине входа или глубине обхода. Pigeonhole стоит за анализом хеш-коллизий: при $n$ возможных значениях хеша и $n+1$ ключе коллизия гарантирована. Доказательство NP-трудности задачи - это редукция плюс рассуждение от противного: если бы существовал полиномиальный алгоритм, то существовал бы и для SAT. Lean 4 выражает все эти техники как тактики: `intro`, `apply`, `induction`, `contradiction`, `exact`.

Парадоксы и границы: где логика ломается

Парадоксы - это не курьёзы, а инструменты разметки границ формальных систем. **Парадокс Рассела** (1901): рассмотрим множество $R = \{x : x \notin x\}$ - множество всех множеств, не содержащих себя. Вопрос: $R \in R$? Если да - противоречит определению. Если нет - удовлетворяет определению, значит должно быть в $R$. Наивная теория множеств Кантора-Фреге несовместна.

**Реакция: ZFC.** Цермело (1908) и Френкель (1922) переписали аксиомы: схема выделения позволяет образовывать $\{x \in A : \phi(x)\}$ только из существующего множества $A$. Аксиома регулярности запрещает $x \in x$. Так парадокс Рассела был исключён ценой потери «множества всех множеств».

**Теорема Кантора:** $|P(X)| > |X|$ для любого множества. Доказательство - канторова диагональ: предположим биекцию $f: X \to P(X)$, рассмотрим $D = \{x \in X : x \notin f(x)\}$. Если $D = f(d)$, то $d \in D \iff d \notin D$. Следствие: иерархия бесконечностей $\aleph_0, \aleph_1, \aleph_2, \ldots$ и невозможность множества всех множеств.

**Гипотеза континуума.** Существует ли мощность строго между $|\mathbb{N}| = \aleph_0$ и $|\mathbb{R}| = 2^{\aleph_0}$? Гёдель (1940) показал: гипотеза не противоречит ZFC. Коэн (1963) методом форсинга показал: отрицание тоже не противоречит ZFC. Гипотеза континуума **независима** от стандартной аксиоматики - первый пример «истины», находящейся вне формальной системы.

**ML/CS-применение.** Парадоксы кодируются в системах типов: бестиповое лямбда-исчисление содержит комбинатор $Y$ и парадокс Карри, что делает его несостоятельным как логическая система. Hindley-Milner (Haskell, ML) и dependent types (Lean, Coq) убирают это через типизацию. Парадокс лжеца проявляется в задачах верификации: компилятор не может в общем случае доказать, что оптимизация сохраняет семантику - это упирается в неразрешимость, родственную диагональному аргументу.

Теория вычислимости: чего нельзя посчитать

Тьюринг (1936) формализовал понятие алгоритма через **машину Тьюринга**: лента, головка, конечный набор состояний. **Тезис Чёрча-Тьюринга** утверждает: всё вычислимое в интуитивном смысле вычислимо машиной Тьюринга. Эквивалентные модели - лямбда-исчисление Чёрча, рекурсивные функции Гёделя, машины с регистрами. Это не теорема, а определение: «вычислимость» = «вычислимость машиной Тьюринга».

**Проблема остановки** (Halting Problem). Существует ли алгоритм $H$, принимающий программу $P$ и вход $x$, и решающий, остановится ли $P(x)$? Тьюринг (1936) доказал: такого $H$ не существует. Доказательство - диагонализация: построим $D(P) = $ если $H(P, P) = $ «останавливается», то цикл, иначе остановиться. Тогда $D(D)$ ведёт к противоречию.

**Теорема Райса** (1953): любое содержательное семантическое свойство программ неразрешимо. «Содержательное» - истинно для одних программ и ложно для других. «Семантическое» - зависит от поведения, а не от текста. Следствие: невозможно автоматически решить «эта программа без багов», «эта оптимизация безопасна», «эти две программы эквивалентны». Не из-за слабости современных компьютеров - принципиально.

**Теорема о рекурсии** (Клини, 1938). Любая программа имеет неподвижную точку: для любой вычислимой $f$ существует программа $e$ такая, что $\phi_e = \phi_{f(e)}$. Следствие - программа может получить доступ к собственному коду (квайны). Теорема s-m-n: универсальное свойство параметризации, формальная основа интерпретаторов и виртуализации.

**ML-применение.** Синтез программ в общем виде неразрешим (следствие из Райса), но в ограниченных доменах работает: DeepMind AlphaCode (2022) генерирует решения для соревнований, GitHub Copilot - boilerplate. LLM выступают как **приближённые оракулы** для задач halting-типа: «эта функция завершится?» - модель угадывает с высокой вероятностью на типичных кодах, не давая формальных гарантий. Граница теории и практики: Райс не запрещает работать в 99% случаев - запрещает работать всегда.

Логика в индустрии: от Lean до AlphaProof

Современная индустрия использует логику не как академическую дисциплину, а как ежедневный инструмент. **Теория типов** связывает математическую логику и программирование: Lean 4, Coq, Agda, Idris - языки, где тип программы является логическим утверждением, а программа - его доказательством.

**Соответствие Карри-Говарда.** Изоморфизм между логикой и теорией типов: $A \to B$ как импликация - тип функций из $A$ в $B$. $A \land B$ - пара $(a, b)$. $A \lor B$ - дизъюнктное объединение. $\forall x. P(x)$ - зависимый тип $\Pi x. P(x)$. Программа корректного типа автоматически является доказательством соответствующей теоремы. Lean 4 эксплуатирует это для формализации математики.

**AlphaProof** (DeepMind, июль 2024) объединяет три компонента: предобученная LLM генерирует кандидатов доказательств в синтаксисе Lean, формальный верификатор Lean 4 проверяет корректность, обучение с подкреплением подстраивает стратегию выбора тактик. Результат - 4 из 6 задач IMO 2024, серебряная медаль. Принципиальная разница с обычной LLM-генерацией: каждый шаг проверен формально, нет «галлюцинаций» в доказательстве.

**Криптопротоколы.** Project Everest (Microsoft Research + INRIA) формально верифицировал реализацию TLS 1.3 на F*. AWS использует SAW (Software Analysis Workbench) и Cryptol для верификации криптокода в s2n - opensource TLS-библиотеке Amazon. Tezos, Cardano применяют формальные методы к смарт-контрактам через Lean/Coq. Ethereum-инструменты Certora и K Framework доказывают свойства Solidity-кода через SMT.

Распространённое заблуждение: «теоремы Гёделя означают, что мы не можем доверять математике». На самом деле Гёдель (1931) доказал: в любой достаточно мощной формальной системе есть истинные, но недоказуемые утверждения. Это не означает «математика сломана» - это означает «список теорем не имеет конца, всегда есть что доказывать дальше». Каждая новая теорема Lean - это новый кирпич в открытом здании.

**ML-применение.** Lean Copilot (Stanford, 2024) - подсказки тактик через LLM-модель, обученную на Mathlib. ProofNet и MiniF2F - бенчмарки автоматического доказательства. Вычислительные системы алгебры (Mathematica, SageMath) генерируют кандидатов, которые затем формально верифицируются в Lean. Граница: для большинства research-математики автоматический поиск пока не работает, но ассистенты доказательств уже стандарт в безопасности и криптографии.

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

• Шесть техник доказательства (прямое, от противного, индукция, контрапозиция, конструкция, pigeonhole) - базовый инструментарий: индукция в корректности алгоритмов, pigeonhole в хеш-коллизиях, противоречие в NP-трудности
• Парадоксы Рассела, Берри, лжеца разметили границы наивной теории множеств: ZFC - результат, гипотеза континуума независима от ZFC (Гёдель + Коэн)
• Halting problem (Тьюринг 1936) и теорема Райса: любое содержательное семантическое свойство программ неразрешимо. ML-системы - приближённые оракулы, не формальные решатели
• Логика в индустрии: Curry-Howard (Lean, Coq, Rust borrow checker), AlphaProof для IMO, формальная верификация TLS и смарт-контрактов. Гёдель не сломал математику - показал её бесконечность

Куда дальше

Math Logic ведёт в:

• Формальная верификация и AI — ml-13 углубляет применение этих техник в SAT/SMT и верификации нейросетей
• Дискретная математика — dm-01 даёт фундамент индукции, комбинаторики и графов, на которых стоят proof techniques
• Теория обучения PAC — lt-01-pac-intro переносит идею «доказуемых границ» из логики в статистическое обучение

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

• Теорема Райса гарантирует, что нет универсальной программы для проверки корректности кода. Однако линтеры, type checker и компиляторы Rust в продакшне ловят миллионы багов в день. Как сочетаются принципиальная неразрешимость и практическая полезность?
• AlphaProof в 2024 получил серебро IMO, генерируя доказательства в Lean. Что меняется для роли математика, когда формальная верификация становится дешевле, чем рецензирование статьи?
• Гипотеза континуума независима от ZFC: её можно принять или отвергнуть, и обе системы непротиворечивы. Что это говорит о природе математической истины - открываем ли её или конструируем?

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

• ml-13 — Формальная верификация и SAT/SMT построены поверх этих базовых техник доказательства
• dm-01 — Дискретная математика - основа индукции, pigeonhole и комбинаторных доказательств
• lt-01-pac-intro — PAC-обучение тоже про доказуемые границы: от логических теорем к вероятностным
• it-01 — Колмогоровская сложность даёт информационно-теоретический аналог неразрешимости
• ml-01-intro