Lean 4: Основы формальной верификации и доказательного программирования

Введение в экосистему Lean 4: установка, синтаксис и основы функционального программирования

Добро пожаловать в курс по Lean 4. Если вы читаете эту статью, значит, вас интересует не просто написание кода, который работает, но и создание кода, правильность которого можно доказать математически. Lean 4 — это уникальный инструмент, который объединяет в себе современный язык функционального программирования и интерактивную систему доказательства теорем.

В этой первой статье мы заложим фундамент: разберемся, что такое Lean, настроим рабочее окружение и напишем наши первые программы.

Что такое Lean 4 и зачем он нужен?

Lean 4 — это проект исследовательского подразделения Microsoft Research (в частности, Леонардо де Моуры). Это язык, который стирает грань между программированием и математикой. В большинстве языков (Python, C++, Java) система типов служит для предотвращения базовых ошибок (например, нельзя сложить строку и число). В Lean система типов настолько мощная, что с её помощью можно выразить любую математическую теорему.

!Lean 4 выступает мостом между миром программного кода и миром строгой математической логики.

В основе Lean лежит исчисление конструкций (Calculus of Constructions) и соответствие Карри — Ховарда. Это принцип, который гласит: написание программы определенного типа равносильно доказательству теоремы, соответствующей этому типу.

Ключевые компоненты экосистемы

Перед установкой важно понимать, из чего состоит инструментарий:

Lean 4 — сам компилятор и ядро языка.

Elan — менеджер версий (аналог rustup в Rust или nvm в Node.js). Он позволяет легко переключаться между версиями Lean.

Lake (Lean Make) — система сборки и менеджер пакетов. С его помощью мы будем создавать проекты и управлять зависимостями.

VS Code — рекомендуемый редактор кода с мощным расширением для Lean.

Установка и настройка окружения

Самый надежный способ начать работу — использовать редактор VS Code. Процесс установки максимально упрощен.

Шаг 1: Установка VS Code

Если у вас еще нет Visual Studio Code, скачайте и установите его с официального сайта Microsoft.

Шаг 2: Установка расширения Lean 4

Откройте VS Code.

Перейдите во вкладку расширений (Extensions) или нажмите Ctrl+Shift+X.

Найдите Lean 4 (издатель: leanprover).

Нажмите Install.

Шаг 3: Инициализация Elan

После установки расширения откройте любой файл с расширением .lean или просто создайте новый текстовый файл, сохраните его как test.lean. Расширение автоматически обнаружит отсутствие Lean в системе и предложит установить elan. Следуйте инструкциям во всплывающем окне.

Шаг 4: Создание первого проекта

Lean 4 не предназначен для работы с одиночными файлами в долгосрочной перспективе. Нам нужно создать проект с помощью Lake.

Откройте терминал в VS Code (Ctrl+ ).

Перейдите в папку, где вы храните проекты.

Введите команду:

Откройте созданную папку в VS Code: File -> Open Folder -> hello_lean.

Найдите файл Main.lean или создайте файл в папке HelloLean. Теперь мы готовы писать код.

Основы синтаксиса: Определения и Типы

Lean — это строго типизированный функциональный язык. Это значит, что у каждого выражения есть тип, и этот тип проверяется на этапе компиляции.

Команда #check

Чтобы узнать тип любого выражения, используется команда #check. Она не запускает код, а только анализирует его.

Здесь мы видим запись вида . В математической нотации это записывается так:

Где — это терм (значение), символ читается как «имеет тип», а — это сам тип.

Определение переменных и функций

Для создания новых определений используется ключевое слово def.

Разберем эту строку: * def — ключевое слово для определения. * myNumber — имя нашего определения. * : Nat — явное указание типа (Natural numbers — натуральные числа произвольной точности). * := — оператор присваивания определения. * 42 — тело определения.

Функции

Функции в Lean — это «граждане первого класса». Они определяются так же, как и обычные значения, но имеют аргументы.

Здесь (n : Nat) означает, что функция принимает аргумент n типа Nat. После скобки : Nat указывает на тип возвращаемого значения.

Мы можем проверить тип самой функции:

Стрелка в типе обозначает отображение. Математически это выглядит так:

Где — функция, — множество натуральных чисел (тип аргумента), а вторая — множество натуральных чисел (тип результата).

Вычисление выражений

Если #check проверяет типы, то #eval вычисляет значения. Это аналог print или REPL в других языках.

Обратите внимание: вызов функции не требует скобок вокруг аргументов, как в C++ или Python. Мы пишем addOne 5, а не addOne(5). Скобки используются только для группировки сложных выражений.

Анонимные функции (Лямбда-выражения)

Иногда нам не нужно давать функции имя. Для этого используется ключевое слово fun.

Синтаксис fun x => body создает функцию, которая принимает x и возвращает body. В математике это соответствует лямбда-исчислению:

Где — символ лямбда-абстракции, — переменная, а — тело функции.

Каррирование и частичное применение

В Lean все функции принимают ровно один аргумент. Как же тогда написать функцию сложения двух чисел?

Посмотрим на её тип:

Тип Nat -> Nat -> Nat на самом деле читается как Nat -> (Nat -> Nat). Это означает, что add принимает число x и возвращает новую функцию, которая ждет число y и возвращает результат.

!Визуализация процесса каррирования: функция с несколькими аргументами — это цепочка функций с одним аргументом.

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

Мы передали только первый аргумент и получили новую функцию addFive.

Сопоставление с образцом (Pattern Matching)

Одной из самых мощных возможностей функциональных языков является сопоставление с образцом. Это похоже на switch-case в других языках, но гораздо мощнее.

Рассмотрим логический тип Bool, который имеет два значения: true и false.

Здесь: * match n with — начинаем сопоставление переменной n. * | 0 => true — если n равно 0, возвращаем true. * | _ => false — символ _ означает «любое другое значение». Для всех остальных чисел возвращаем false.

Рекурсия

В функциональном программировании нет циклов for или while. Вместо них используется рекурсия. Lean требует, чтобы все функции были тотальными, то есть завершались для любого входа. Для рекурсии это значит, что Lean должен видеть, что аргумент уменьшается с каждым шагом.

Напишем функцию вычисления факториала. В математике факториал определяется так:

Где — факториал числа, — базовый случай, а — рекурсивный шаг.

В Lean это выглядит так:

Обратите внимание на паттерн k + 1. Если n не ноль, Lean понимает, что n можно представить как k + 1 (где k — предыдущее число). Рекурсивный вызов factorial k происходит с меньшим числом, поэтому Lean гарантирует, что программа не зациклится.

Структуры

Для объединения данных используются структуры. Это аналог struct в C или class (без методов) в Python.

deriving Repr говорит Lean автоматически сгенерировать код для отображения структуры в #eval.

Заключение

Мы сделали первые шаги в экосистеме Lean 4:

Установили инструменты (VS Code, Elan, Lake).

Научились определять значения и функции с помощью def.

Познакомились с типами и командой #check`.

Освоили базовую рекурсию и сопоставление с образцом.

Lean 4 — это язык, где типы играют главную роль. В следующих статьях мы увидим, как эти типы превращаются в логические утверждения, и как написание кода превращается в доказательство теорем.

Логика и доказательства: работа с тактиками, пропозициональное исчисление и кванторы

В предыдущей статье мы научились писать простые функции и вычислять значения. Однако главная сила Lean 4 заключается не в вычислениях, а в доказательствах. Сегодня мы перейдем от написания программ к написанию математических доказательств, используя мощную систему тактик.

Утверждения как Типы

В основе Lean лежит концепция «Утверждения как Типы» (Propositions as Types). Это означает, что любое математическое утверждение (например, «2 + 2 = 4» или «для любого x, x > 0») представляется в языке как тип.

Если утверждение — это тип, то что такое доказательство? Доказательство — это значение (или терм) этого типа. Если нам удается сконструировать значение определенного типа, значит, соответствующее утверждение истинно.

В Lean существует специальный сорт типов, называемый Prop (от англ. Proposition — утверждение).

Здесь myStatement — это не само доказательство, а лишь формулировка утверждения. Чтобы доказать его, мы должны предоставить значение.

Режим тактик

Написание доказательств «вручную» (как мы писали функции через def) может быть сложным и громоздким для больших теорем. Для этого в Lean существует режим тактик. Он активируется ключевым словом by.

Тактики — это инструкции, которые говорят Lean, как шаг за шагом построить доказательство. Это похоже на диалог с компьютером: вы говорите «предположим X», «применим теорему Y», и Lean обновляет текущее состояние доказательства.

!Схематичное изображение рабочего процесса в Lean: слева код, справа интерактивное состояние доказательства.

Рассмотрим простейший пример. Пусть нам нужно доказать, что из утверждения следует утверждение .

Где — квантор всеобщности, — переменная типа утверждение, а — импликация.

Разберем, что здесь происходит:

theorem — ключевое слово, аналогичное def, но указывающее на то, что мы доказываем утверждение.

by — вход в режим тактик.

intro h — тактика, которая переносит посылку импликации в контекст (наши предположения) и называет её h.

exact h — тактика, которая говорит: «то, что нужно доказать, — это в точности гипотеза h».

Пропозициональная логика

Пропозициональная логика (логика высказываний) работает с логическими связками: «и», «или», «не», «если... то». Давайте посмотрим, как доказывать утверждения с этими связками в Lean.

Импликация ()

Импликация читается как «если , то ».

* Чтобы доказать , мы используем тактику intro. Мы предполагаем, что верно, и пытаемся вывести . * Чтобы использовать факт (если он у нас есть в гипотезах) для доказательства , мы используем тактику apply. Если у нас есть гипотеза , и нам нужно доказать , команда apply h изменит нашу цель на (ведь если мы докажем , то будет следовать из ).

Пример транзитивности импликации:

Конъюнкция (Логическое И, )

Конъюнкция означает, что верны оба утверждения.

* Чтобы доказать , нужно доказать И доказать . Тактика constructor разбивает одну цель на две. * Чтобы использовать гипотезу , можно разбить её на две отдельные гипотезы ( и ) с помощью тактики cases h with hp hq.

Пример коммутативности «И»:

Где — логическое И, — импликация.

Дизъюнкция (Логическое ИЛИ, )

Дизъюнкция означает, что верно хотя бы одно из утверждений.

* Чтобы доказать , нужно выбрать, какую часть мы будем доказывать. Тактика apply Or.inl (или left) выбирает левую часть (), а apply Or.inr (или right) — правую (). * Чтобы использовать гипотезу , мы обязаны рассмотреть два случая: когда верно и когда верно . Это делается тактикой cases h.

Пример коммутативности «ИЛИ»:

Отрицание ()

В конструктивной логике Lean отрицание определяется как импликация:

Где — знак отрицания, — тождество по определению, а — утверждение, которое невозможно доказать (ложь).

Это значит, что доказать «не » — это то же самое, что доказать «если верно, то мы приходим к противоречию».

* Чтобы доказать , мы делаем intro h (предполагаем ) и пытаемся вывести False. * Чтобы использовать противоречие (например, у нас есть и ), мы можем применить apply h2 к h1, получив False.

Кванторы

Логика становится намного интереснее, когда мы добавляем кванторы.

Квантор всеобщности ()

Утверждение читается как «для любого типа верно свойство ».

В Lean квантор всеобщности ведет себя почти так же, как импликация (функция). По сути, это функция, которая принимает значение и возвращает доказательство для этого конкретного .

* Доказательство: intro x. Мы вводим произвольный в контекст. * Использование: Если у нас есть теорема h : ∀ x, P x, мы можем применить её к конкретному значению y, написав h y или apply h.

Квантор существования ()

Утверждение читается как «существует такой типа , для которого верно ».

* Чтобы доказать существование, нам нужно предъявить конкретный объект (свидетеля). Для этого используется тактика exists v (или use v), где v — это значение, которое удовлетворяет свойству. * Чтобы использовать факт существования (гипотезу h : ∃ x, P x), мы используем cases h with val h_val. Это дает нам абстрактное значение val и доказательство h_val, что для этого значения свойство верно.

Пример с арифметикой:

Где — множество натуральных чисел, — отношение «больше».

Тактика rw (Rewrite)

Одной из самых часто используемых тактик является rw (rewrite — переписать). Она используется, когда у нас есть равенство , и мы хотим заменить на (или наоборот) в нашей цели или гипотезах.

Если , то: * rw [h] заменит все вхождения на в цели. * rw [←h] (стрелка влево) заменит на .

Заключение

Мы рассмотрели основы логики в Lean 4:

Implication (->): intro для доказательства, apply для использования.

And (/\): constructor для создания, cases для разбора.

Or (\/): left/right для выбора, cases для разбора случаев.

Not (¬): Работает как импликация к False.

Quantifiers: intro для , exists для .

Эти базовые кирпичики позволяют строить доказательства любой сложности. В следующей статье мы углубимся в работу с числами, индукцию и автоматизацию доказательств, чтобы Lean делал рутинную работу за нас.

Индуктивные типы и структуры: моделирование данных и определение свойств программ

Ранее были изучены основы синтаксиса Lean 4, функциональное программирование и базовая логика. Было показано, как доказывать простые утверждения, используя тактики. Однако реальные программы редко работают только с абстрактными утверждениями , где — посылка, а — следствие. Они работают со структурами данных: списками, деревьями, пользователями, транзакциями.

В данной статье разбирается, как моделировать сложные данные с помощью структур и индуктивных типов. Более того, будет показано, что в Lean индуктивные типы используются не только для хранения данных, но и для определения логических свойств (например, «число является четным» или «список отсортирован»).

Структуры: Типы-произведения

Самый простой способ объединить несколько значений в одно целое — использовать структуры. В теории типов это называется типами-произведениями (Product Types), потому что множество возможных значений структуры является декартовым произведением множеств значений её полей.

Определение структуры

Допустим, необходимо представить точку в двумерном пространстве. Для этого нужны две координаты.

Здесь: * structure — ключевое слово для объявления. * Point — имя нового типа. * x и y — поля структуры с типом Float. * deriving Repr — просит Lean автоматически создать код для текстового представления (чтобы можно было видеть результат в #eval).

Создание и использование

Можно создать экземпляр структуры и обращаться к её полям через точку:

Также можно обновлять значения (функционально, создавая новую копию):

Индуктивные типы: Сердце Lean

Если структуры позволяют хранить «И то, И это» (координату X и координату Y), то индуктивные типы позволяют выразить «ИЛИ то, ИЛИ это». Но их возможности гораздо шире простых перечислений.

Индуктивный тип определяется указанием всех способов (конструкторов), с помощью которых можно создать элемент этого типа.

Перечисления (Enumerations)

Простейший вид индуктивного типа — это перечисление.

Тип Weekday имеет ровно 7 значений. Можно писать функции, используя сопоставление с образцом (match):

Параметризованные типы и рекурсия

Индуктивные типы становятся по-настоящему мощными, когда они могут хранить данные и ссылаться сами на себя. Классический пример — натуральные числа.

В математике натуральные числа строятся по аксиомам Пеано:

— это натуральное число (где — начальный элемент).

Если — натуральное число, то (следующее за ним) — тоже натуральное число (где — текущее число, а — функция следования).

В Lean это записывается так:

Здесь zero — это базовый случай, а succ (successor) — индуктивный шаг, который принимает одно число и возвращает следующее.

Аналогично определяются списки. Список элементов типа (где — произвольный тип данных) — это либо пустой список, либо элемент, присоединенный к другому списку.

!nil : List α | cons (head : α) (tail : List α) : List α

* nil — пустой список. * cons — конструктор, добавляющий элемент в начало (аналог :: или [x] + list).

Например, список [1, 2] в развернутом виде выглядит как: cons 1 (cons 2 nil)

Индуктивные предикаты: Логика через типы

Самая удивительная особенность Lean заключается в том, что используется тот же механизм inductive для определения логических свойств. Вспомним принцип «Утверждения как Типы». Если можно определить тип данных, можно определить и тип доказательства.

Рассмотрим свойство «быть чётным числом». Его можно определить индуктивно:

Разберем это определение:

Even — это не тип данных (как Nat), а функция, возвращающая утверждение (Prop). Она принимает число и возвращает утверждение о нем.

zero — это аксиома: «0 является четным».

add_two — это правило вывода: «Если четное (имеется доказательство ), то тоже четное» (где — число, — гипотеза, — число, увеличенное на 2).

Если нужно доказать, что 4 — четное число, конструируется значение этого типа:

Тактика induction

При работе с индуктивными типами (числами, списками) обычной тактики cases (разбор случаев) часто недостаточно. cases позволяет разобрать число на и (где — ноль, а — следующее число), но не дает индуктивной гипотезы.

Для доказательства свойств рекурсивных структур используется тактика induction.

Рассмотрим пример. Докажем ассоциативность сложения списков (оператор ++).

где — квантор всеобщности (для всех), — списки элементов типа , — операция конкатенации (объединения) списков, — равенство.

Что здесь произошло?

induction as разбило доказательство на два случая: когда список пуст (nil) и когда он не пуст (cons).

В случае cons был получен доступ к ih (индуктивной гипотезе). Она говорит, что равенство уже верно для хвоста списка (tail).

Тактика simp упрощает выражение, используя определение функции ++.

rw [ih] (rewrite) использует гипотезу индукции, чтобы завершить доказательство.

Почему это важно для верификации?

Индуктивные типы позволяют моделировать:

Синтаксис языков программирования (выражения, операторы).

Структуры данных (красно-черные деревья, очереди).

Семантику выполнения (как программа меняет состояние шаг за шагом).

Определяя свойства индуктивно (как Even), можно формально доказывать корректность алгоритмов. Например, можно определить индуктивный предикат Sorted (отсортирован) и доказать, что функция sort превращает любой список в список, удовлетворяющий предикату Sorted.

Заключение

Были рассмотрены два фундаментальных способа организации данных в Lean: * Структуры для объединения данных (логическое И). * Индуктивные типы для перечислений и рекурсивных структур (логическое ИЛИ + рекурсия).

Также стало известно, что свойства программ тоже могут быть индуктивными типами, а для доказательства теорем о них используется мощная тактика induction.

В следующей части курса эти знания будут применены на практике для верификации простой программы и доказательства её корректности относительно спецификации.

Верификация алгоритмов: математическая индукция, рекурсия и доказательство корректности функций

В предыдущих статьях мы изучили синтаксис Lean 4, основы логики и структуру индуктивных типов. Теперь мы подошли к самому интересному этапу: использованию этих инструментов для доказательства того, что наши программы работают правильно.

В обычном программировании мы пишем тесты. Тесты проверяют работу функции на некоторых входных данных (например, для чисел 0, 1, 10 и 100). Но тесты не могут гарантировать, что функция работает верно для всех возможных значений. Формальная верификация позволяет доказать корректность алгоритма для любого допустимого входа, используя мощь математической индукции.

Связь рекурсии и индукции

Существует глубокая фундаментальная связь между рекурсией в программировании и индукцией в математике.

Рекурсия — это способ определения* функции: мы разбиваем сложную задачу на более простые подзадачи, пока не дойдем до базового случая. Индукция — это способ доказательства* свойств: мы доказываем утверждение для базового случая, а затем показываем, что если утверждение верно для простой задачи, то оно верно и для более сложной.

!Визуализация принципа: рекурсия разбирает задачу до основания, а индукция строит доказательство от основания вверх.

В Lean 4, когда мы определяем рекурсивную функцию по индуктивному типу (например, Nat или List), мы почти всегда будем использовать тактику induction для доказательства свойств этой функции.

Пример 1: Сумма чисел (Формула Гаусса)

Рассмотрим классическую задачу. Напишем функцию, которая вычисляет сумму всех натуральных чисел от до .

Определение функции

Эта функция рекурсивна. * Если , сумма равна 0. * Если , мы прибавляем текущее число к сумме предыдущих.

Формулировка теоремы

Карл Фридрих Гаусс еще в школе заметил, что сумму чисел можно вычислить по формуле:

Где — знак суммы, — переменная суммирования, а — верхняя граница.

В Lean деление натуральных чисел (Nat) целочисленное и отбрасывает остаток, что может усложнить доказательство. Чтобы избежать дробей, перепишем формулу в виде умножения:

Где — операция умножения, — наша рекурсивная функция.

Доказательство

Попробуем доказать это утверждение в Lean.

Разбор ключевых моментов:

induction n with ... — разбивает задачу на два случая: ноль и последователь.

ih — это наше самое мощное оружие. Это предположение, что для k формула уже доказана. Наша задача — свести выражение для k+1 к выражению, содержащему k, и заменить его.

rw (rewrite) — используется для подстановки определений и гипотезы индукции.

Структурная индукция: работа со списками

Индукция работает не только для чисел. Она применима к любым индуктивным типам данных. Это называется структурной индукцией.

Рассмотрим функцию разворота списка reverse.

Здесь :: — конструктор добавления элемента в начало, а ++ — конкатенация списков.

Мы хотим доказать свойство инволютивности: если развернуть список дважды, мы получим исходный список.

Где — квантор всеобщности, — произвольный список типа .

Попытка доказательства и необходимость лемм

Здесь мы застреваем. У нас есть reverse (reverse xs ++ [x]). Функция reverse определена для конструктора :: (элемент в начале), но здесь у нас ++ [x] (элемент в конце). Lean не знает, как reverse взаимодействует с ++.

Нам нужна лемма — вспомогательная теорема.

Лемма о развороте конкатенации

Нам нужно доказать, что разворот суммы списков — это сумма разворотов в обратном порядке:

Теперь, имея эту лемму, мы можем завершить главное доказательство.

Завершение доказательства

Вернемся к reverse_reverse:

Стратегия доказательства корректности

При верификации функций в Lean полезно придерживаться следующего алгоритма:

Определите функцию. Убедитесь, что она завершается (Lean требует тотальности функций).

Сформулируйте свойство. Запишите теорему, используя логические связки и равенства.

Попробуйте индукцию. Используйте induction по основному аргументу, который уменьшается в рекурсии.

Упрощайте (simp). Используйте simp для вычисления базовых случаев и раскрытия определений.

Ищите заторы. Если simp и rw [ih] не решают задачу, посмотрите на выражение. Возможно, вам нужна лемма о том, как ваша функция взаимодействует с другими операторами (как reverse и ++).

Докажите лемму. Выделите её в отдельную теорему и докажите (часто тоже индукцией).

Тотальность функций

Важно отметить, что Lean позволяет доказывать свойства только для функций, которые гарантированно завершаются. Если бы функция могла уйти в бесконечный цикл, логика Lean стала бы противоречивой (можно было бы доказать ложь).

К счастью, для структурной рекурсии (когда мы отнимаем 1 от числа или откусываем голову у списка) Lean автоматически доказывает завершаемость.

Заключение

Мы научились использовать математическую индукцию для верификации программ. Мы увидели, что: * Индукция в доказательствах зеркально отражает рекурсию в коде. * Индуктивная гипотеза (ih) позволяет использовать решение для меньшей задачи. * Часто для доказательства требуются вспомогательные леммы, описывающие свойства операций.

Теперь вы обладаете инструментарием для того, чтобы не просто писать код, но и математически гарантировать его безошибочность. В следующих статьях мы рассмотрим более сложные тактики автоматизации, которые позволят сократить наши доказательства с десятков строк до одной-двух команд.

Продвинутые техники: автоматизация доказательств, метапрограммирование и формализация математических теорем

Мы прошли долгий путь от установки Lean 4 до доказательства корректности рекурсивных функций с помощью индукции. До сих пор мы писали доказательства «вручную», шаг за шагом объясняя Lean, какую тактику применить. Это полезно для обучения, но в реальных проектах доказательства могут занимать тысячи строк.

В этой статье мы перейдем на следующий уровень. Мы узнаем, как заставить компьютер писать доказательства за нас, как расширять язык Lean под свои нужды и как формализовывать «чистую» математику.

Автоматизация доказательств

Главная цель Lean — не заставить человека страдать над рутиной, а позволить ему сосредоточиться на сложных идеях. Для этого существуют мощные тактики автоматизации.

Упроститель (simp)

Тактика simp (simplifier) — это «рабочая лошадка» Lean. Она использует базу знаний лемм, помеченных атрибутом @[simp], чтобы переписывать выражение до тех пор, пока оно не станет максимально простым.

!Визуализация процесса упрощения выражения: тактика находит известные шаблоны и заменяет их на упрощенные версии.

Рассмотрим пример. Допустим, нам нужно доказать:

Где и — натуральные числа, — сложение, — ноль.

Вручную мы бы использовали коммутативность и свойства нуля. Но simp знает эти свойства.

Здесь мы подсказали simp, что нужно использовать коммутативность сложения (Nat.add_comm). Свойство он знает по умолчанию.

Линейная арифметика (linarith)

Часто возникают задачи с неравенствами, которые очевидны для школьника, но требуют десятков шагов в формальной логике. Например:

Где — числа, — строго меньше, — меньше или равно, — логическое И, — импликация.

Тактика linarith (linear arithmetic) автоматически решает системы линейных равенств и неравенств.

linarith ищет противоречия в системе линейных ограничений. Если отрицание цели противоречит гипотезам, значит, цель верна.

Алгебраические кольца (ring)

Для доказательства равенств с умножением, сложением и возведением в степень (в коммутативных кольцах) используется тактика ring.

Попробуем доказать формулу сокращенного умножения:

Где — числа, скобки обозначают приоритет операций, а квадрат — умножение числа на само себя.

Без тактики ring нам пришлось бы многократно применять дистрибутивность () и ассоциативность, что заняло бы 20-30 строк кода.

Метапрограммирование: Lean на Lean

Уникальная особенность Lean 4 заключается в том, что это расширяемый язык. Большая часть самого Lean написана на Lean. Это означает, что вы можете писать свои собственные тактики, используя тот же синтаксис.

Макросы

Самый простой способ автоматизации — создание макросов. Макрос — это шаблон, который разворачивается в другой код перед компиляцией.

Допустим, мы часто встречаем паттерн: ввести гипотезу и сразу упростить цель.

Написание своих тактик

Вы можете писать функции на Lean, которые манипулируют состоянием доказательства. Это называется метапрограммированием. Если вы заметили, что в вашем проекте часто повторяется одна и та же логическая структура доказательства, вы можете написать скрипт (тактику), который делает это за вас.

Это делает Lean не просто языком для проверки доказательств, а языком для программирования доказательств.

Формализация математики и Mathlib

До сих пор мы говорили о верификации программ. Но Lean широко используется математиками для формализации «чистой» математики (топологии, алгебры, анализа).

Библиотека Mathlib

Mathlib — это гигантская библиотека математических теорем, доказанных сообществом Lean. В ней содержатся десятки тысяч утверждений: от свойств простых чисел до сложных теорем функционального анализа.

Когда вы подключаете Mathlib, вы получаете доступ к огромному количеству готовых структур.

Пример: Группы

В математике группа — это множество с операцией, которая ассоциативна, имеет нейтральный элемент и обратный элемент.

Где — операция группы, — элементы группы, — квантор всеобщности.

В Lean мы можем определить структуру группы и доказывать теоремы для любой группы сразу.

Здесь [Group G] говорит Lean: «Пусть G — это произвольный тип, который является группой». Lean автоматически находит подходящие аксиомы.

Зачем нужна формализация?

Абсолютная точность. В обычных математических статьях часто пишут «очевидно, что...» или «аналогично...». В Lean каждый шаг должен быть проверен ядром. Ошибки невозможны.

Помощь в исследованиях. Современная математика стала настолько сложной, что рецензенты могут годами проверять доказательства (как было с доказательством гипотезы Кеплера). Компьютер делает это мгновенно после написания кода.

Обучение. Lean заставляет четко понимать каждое определение. Вы не можете использовать понятие, если не понимаете его формальной сути.

Заключение курса

Мы прошли путь от основ синтаксиса до продвинутых техник.

* Мы узнали, что типы — это утверждения, а программы — это доказательства. * Мы освоили индукцию как главный инструмент работы с рекурсивными данными. * Мы увидели, как автоматизация (simp, linarith, ring) берет на себя рутину.

Lean 4 — это инструмент будущего. Граница между программистом и математиком стирается. Верифицированный код гарантирует отсутствие багов, а формализованная математика гарантирует истинность теорем. Теперь этот инструмент в ваших руках.