Математическая логика
Конструктивная математика и MLTT
В 2023 году DeepMind's AlphaProof решил задачи международной математической олимпиады, используя Lean 4 для верификации доказательств. Конструктивная математика и теория типов Мартина-Лёфа лежат в основе новой волны автоматизированного математического рассуждения.
- Formal Math: Lean Mathlib - 150,000+ верифицированных теорем к 2024 году
- CompCert: C-компилятор с формальным доказательством корректности (Airbus, NASA)
- Proof assistants: Coq используется для верификации ядра операционной системы seL4
- Hardware verification: Intel использует HOL Light для верификации процессоров
- Cryptography: верификация протоколов TLS через конструктивные доказательства
- AI Safety: формальная верификация нейросетевых свойств через зависимые типы
Lean 4 за 0.1 секунды проверяет 300 страниц математики. CompCert - C-компилятор без единого найденного бага оптимизации. seL4 - ядро ОС для дронов NASA. Всё это - конструктивная математика в действии: каждое доказательство является алгоритмом, который компьютер может проверить механически.
**О чём этот урок на самом деле:** конструктивная математика - это не ограничение по сравнению с классической, а другой способ организации знания. Конструктивное доказательство ∃x.P(x) автоматически даёт алгоритм нахождения x. MLTT делает это точным через зависимые типы.
Классика vs конструктивизм
Классически: «Среди иррациональных a,b может существовать рациональное a^b» - доказывается без явного примера, разбором двух случаев про √2^√2. Конструктивно: нужно предъявить конкретные a,b и доказать рациональность. Это принципиально разные вещи. Алгоритм экстракции Coq из конструктивного доказательства даёт запускаемый код.
MLTT: три уровня
MLTT работает на трёх уровнях одновременно: (1) Типы - это предложения логики, (2) Термы - это доказательства, (3) Вычисление - это нормализация. Запись a:A читается: «a доказывает A» или «a является элементом A». Это один и тот же формализм для математики и программирования.
Π-типы и Σ-типы в индустрии
**Σ-тип в TypeScript:** `type Pair<N extends number> = { len: N, data: number[] }` - это имитация Σ(n:Nat).[n числа]. **Π-тип в Rust:** `fn concat<const N: usize, const M: usize>(a: [u8;N], b: [u8;M]) -> [u8;{N+M}]` - зависимая функция с константными параметрами. Полноценные зависимые типы есть только в Agda/Coq/Lean/Idris.
**Конструктивная математика в производстве** От теории до верифицированного промышленного кода • **Coq / Rocq** (CIC = MLTT + инductive types): CompCert (C-компилятор), Fiat Cryptography (код для Chrome). Extraction в OCaml/Haskell. • **Lean 4** (Mathlib + тактики): 100k+ формальных теорем, теорема Кеплера, верификация для Scholze. Самый быстро растущий инструмент. • **Agda** (Чистая MLTT + HoTT): Cubical Agda реализует аксиому унивалентности. Используется для верификации криптографических протоколов. • **Idris 2** (Зависимые типы для разработчиков): Ближе к Haskell синтаксически. Линейные типы (Quantitative Type Theory). Для production-разработки.
Конструктивная математика: каждое доказательство - алгоритм
Lean 4 за 0.1 секунды верифицировал теорему Кеплера о плотнейшей упаковке шаров - 300 страниц математики, 7000 строк доказательств. Это стало возможным благодаря конструктивной математике: **каждое доказательство существования - это алгоритм**, который предъявляет объект явно. Компьютер проверяет алгоритм, а не 300-страничный текст.
Классически: √2 иррационально - доказано от противного. Конструктивно: √2 иррационально - вот алгоритм, который по любой дроби p/q показывает, что |√2 - p/q| > 0. Конструктивное доказательство = верифицируемый алгоритм. Именно это делает Lean/Coq возможными.
**Конструктивная математика - это не ограничение, а усиление.** Конструктивное доказательство ∃x.P(x) автоматически даёт алгоритм нахождения x. Коq может «экстрагировать» из доказательства исполняемый OCaml-код. CompCert получен именно так: доказательство корректности компилятора → запускаемый компилятор.
Почему закон исключённого третьего P∨¬P не является конструктивно допустимой аксиомой?
Конструктивно доказать P∨¬P значит либо доказать P, либо ¬P. Для P = 'π содержит 0123456789' ни одно из них неизвестно, хотя классически одно истинно.
Теория типов Мартина-Лёфа (MLTT)
Per Martin-Löf в 1975 построил теорию, где **типы, множества и пропозиции - одно и то же**. Элемент a:A читается и как «a принадлежит множеству A», и как «a - доказательство утверждения A». Это не метафора - это единая формальная система. На ней стоят Agda, Coq (Calculus of Inductive Constructions), Lean 4.
Тип тождества Id_A(a,b) - это **тип**, элементы которого суть доказательства равенства a=b. refl_a : Id_A(a,a) - рефлексивность. Этот тип может иметь много элементов (много «путей» между a и b) - именно это и открыло дверь в Homotopy Type Theory.
Зачем в MLTT вводится иерархия Type₀:Type₁:Type₂:... вместо единого Type:Type?
Type:Type позволяет построить самореференсный тип U:U, приводящий к логическому противоречию. Иерархия Type₀:Type₁ разрывает самореференцию.
Π-типы и Σ-типы: ∀ и ∃ как программы
Π-тип и Σ-тип - главные строительные блоки MLTT. Они не просто аналоги ∀ и ∃ - они являются ими по изоморфизму Карри-Говарда. Π(x:A).B(x) - это ∀x:A.B(x), и каждый элемент этого типа - алгоритм, преобразующий x:A в элемент B(x). Доказательство ∀ = программа.
| Логика | MLTT | Пример |
|---|---|---|
| ∀x:A. P(x) | Π(x:A).P(x) | map : Π(n:Nat).(A→B)→Vec A n→Vec B n |
| ∃x:A. P(x) | Σ(x:A).P(x) | Σ(n:Nat).isPrime(n) - простое число |
| A → B | Π(x:A).B (B не зависит от x) | Обычная функция f:A→B |
| A × B | Σ(x:A).B (B не зависит от x) | Обычная пара (a,b) |
| a = b | Id_A(a,b) | Тип путей из a в b |
Что является элементом типа Σ(n:Nat).isPrime(n) в MLTT?
Σ-тип реализует конструктивное ∃: нельзя просто утверждать 'простое число существует' - нужно предъявить конкретный n и его доказательство простоты.
HoTT и формальная верификация
Владимир Воеводский (медаль Филдса 2002) заметил: тип тождества Id_A(a,b) ведёт себя как **пространство путей** из точки a в точку b в топологическом пространстве A. Id путей = гомотопии. Это Homotopy Type Theory (2013). Аксиома унивалентности: (A ≃ B) ≃ (A = B) - изоморфные типы равны. Это новое основание математики.
**Lean 4 и Mathlib** - крупнейшая формальная математическая библиотека. Питер Шольце попросил верифицировать ключевую лемму из его конденсированной математики (2020). Команда Lean сделала это за 6 месяцев. Результат: Шольце уверен в доказательстве теоремы, о которой сам говорил, что «не уверен на 100%».
Аксиома унивалентности Воеводского: (A ≃ B) ≃ (A = B). Изоморфные типы **равны**. Это означает: любое доказательство о A автоматически переносится на B, если A ≃ B. В классической математике изоморфизм и равенство - разные понятия. В HoTT они совпадают.
Что утверждает аксиома унивалентности Воеводского?
Унивалентность формализует неформальный принцип математики: изоморфные структуры неразличимы. Теорема о A автоматически переносится на B ≃ A.
dok(A ∧ B) = (dok(A), dok(B)) пара доказательств dok(A ∨ B) = inl(dok(A)) | inr(dok(B)) tagged union dok(A → B) = f: dok(A) → dok(B) функция dok(⊥) = () пустой тип (нет элементов) dok(∀x:A. P(x)) = f: Π(x:A).P(x) функция с зависимым типом dok(∃x:A. P(x)) = (x₀, dok(P(x₀))) конкретный свидетель + доказательство
Упражнения
- Чем конструктивное математическое доказательство отличается от классического? — Конструктивно: ∃x.P(x) требует явного свидетеля x₀ и dok(P(x₀)); BHK: доказательство - алгоритм, dok(A→B) = функция; LEM недоступен без явного разбора случаев; Coq extraction: доказательство → запускаемый код автоматически
- Что такое аксиома унивалентности HoTT и какое следствие она имеет? — Univalence: (A ≃ B) ≃ (A = B) - изоморфные типы равны; Следствие: теоремы автоматически переносятся между изоморфными структурами; Тип тождества Id_A(a,b) = пространство путей из a в b; HoTT - новое основание математики, не требующее аксиомы выбора в классическом виде
Ключевые идеи
- Конструктивизм: каждое ∃x.P(x) требует свидетеля x₀; LEM не аксиома - это алгоритмическая математика
- BHK-интерпретация: dok(A∧B)=пара, dok(A→B)=функция, dok(∃x.P)=(x₀,dok(P(x₀)))
- MLTT: типы=пропозиции=множества; a:A читается и как элемент, и как доказательство
- Иерархия Type₀:Type₁:... избегает парадокса Жирара - аналога парадокса Рассела для типов
- Π(x:A).B(x) = ∀, Σ(x:A).B(x) = ∃; вместе покрывают всю логику предикатов
- HoTT: Id_A(a,b) = пространство путей; Univalence: (A≃B) = (A=B); Lean верифицирует Mathlib
Связанные темы
Конструктивная математика объединяет логику, вычисления и формальную верификацию
- Теория типов (System F, CHI) — MLTT расширяет System F зависимыми типами; Curry-Howard обобщается до логики предикатов
- Теория категорий и логика — Локально декартово замкнутые категории = MLTT; HoTT связывает MLTT с геометрией
- Интуиционистская логика — MLTT - вычислительная интерпретация интуиционистской логики предикатов