От Фреге к Lean: эволюция формализации
История перевода математики на язык компьютеров началась с Готлоба Фреге и его Begriffsschrift (1879), а затем Давида Гильберта, который предложил строить геометрию на строгих аксиомах. Однако Курт Гёдель в 1930 году показал ограничения этой программы: достаточно мощная система не может доказать собственную непротиворечивость. Несмотря на это, путь к полной формализации продолжился через системы Automath, Mizar, HOL, Isabelle и Coq.
Современный стандарт — Lean. Это интерактивный proof assistant на базе теории зависимых типов. В отличие от обычных языков, где тип — это просто «число» или «строка», в Lean тип может зависеть от значения (например, «список ровно из 5 элементов»). Утверждение здесь — это тип, а доказательство — объект этого типа. Если код компилируется, доказательство верно.
Кейс упаковки сфер: победа формальной верификации
Ярким примером успеха формализации стала гипотеза Кеплера об упаковке шаров. В 2014 году проект Flyspeck завершил формальную проверку доказательства, начатого Томасом Хейлсом. Это доказало, что компьютер может не только считать, но и проверять сложнейшие математические рассуждения, исключая человеческую ошибку.
Задача Навье — Стокса и роль LLM
Ситуация с задачей Навье — Стокса (одной из задач тысячелетия) инициатива ИИ пока не решила, но изменила подход к исследованию. Большие языковые модели, обученные на Mathlib, активно используются для генерации кода на Lean. Это позволяет ученым быстрее формализовать гипотезы и проверять их корректность, выступая в роли мощного ассистента, а не автономного решателя.
Почему это важно для науки
Формализация устраняет неоднозначность естественного языка. То, что для человека очевидно (например, «если число четное, то его квадрат четный»), для компьютера требует строгого определения через аксиомы и правила вывода. Внедрение Lean и ИИ-ассистентов ускоряет научный процесс, делая доказательства технически проверяемыми и воспроизводимыми.
Источник: Habr ↗