Машина, которая доказывает

☀️ Автоматическое доказательство теорем: когда логика становится кодом
Мы уже знаем, что математическое доказательство — это механическая процедура: берем аксиомы, применяем правила вывода, получаем теоремы. Но может ли эту работу выполнять компьютер?
Математическое ядро:
В 1950-х годах математики начали создавать программы, которые автоматически ищут доказательства. Это направление называется автоматическое доказательство теорем (Automated Theorem Proving, ATP).
Как это работает?
1. Формализация: Теорема и аксиомы записываются на формальном языке (обычно логика первого порядка).
2. Поиск: Алгоритм (например, метод резолюций) систематически применяет правила вывода, пытаясь построить цепочку от аксиом к теореме.
3. Проверка: Если цепочка найдена — доказательство готово. Если нет — программа может работать бесконечно (вспомните проблему остановки!).
Современные системы (Coq, Lean, Isabelle) пошли дальше: они не только ищут доказательства, но и проверяют их с абсолютной точностью. Каждое утверждение в доказательстве проверяется компьютером.
Зачем это нужно?
В 1976 году Кеннет Аппель и Вольфганг Хакен доказали теорему о четырех красках с помощью компьютера. Это был первый случай, когда доказательство было слишком длинным для проверки человеком. Сегодня системы вроде Lean используются для верификации сложных математических результатов и даже программного кода в авиации и криптографии.