Лин (помощник по доказательству)
 | |
| Парадигма | Функциональное программирование , Императивное программирование |
|---|---|
| Разработчик | Бережливое ФРО |
| Впервые появился | 2013 год |
| Стабильная версия | 4.7.0
/ 3 апреля 2024 г |
| Предварительный выпуск | 4.8.0-rc1
/ 2 мая 2024 г |
| Дисциплина набора текста | Статический , сильный , предполагаемый |
| Язык реализации | Наклонять , С++ |
| ТЫ | Кросс-платформенный |
| Лицензия | Лицензия Апач 2.0 |
| Веб-сайт | лен-ланг |
| Под влиянием | |
| МЛ Кок Хаскелл | |
Lean — это помощник доказательства и функциональный язык программирования . [1] В его основе лежит расчет конструкций индуктивного типа . Это проект с открытым исходным кодом, размещенный на GitHub . Он был разработан в первую очередь Леонардо де Моурой , когда он работал в Microsoft Research , а теперь и в Amazon Web Services , и за свою историю в него внесли значительный вклад другие соавторы и сотрудники. В настоящее время разработку поддерживает некоммерческая организация Lean Focused Research Organization (FRO) .
История [ править ]
Lean был запущен Леонардо де Моурой из Microsoft Research в 2013 году. [2] Первоначальные версии языка, позже известные как Lean 1 и 2, были экспериментальными и содержали такие функции, как поддержка теории гомотопических типов , основанной на основах, от которых позже отказались.
Lean 3 (впервые выпущенная 20 января 2017 г.) была первой умеренно стабильной версией Lean. Он был реализован в основном на C++, а некоторые функции были написаны на самом Lean. После версии 3.4.2 срок службы Lean 3 был официально прекращен, а разработка Lean 4 началась. В этот промежуточный период члены сообщества Lean разработали и выпустили неофициальные версии до 3.51.1.
В 2021 году был выпущен Lean 4, который представлял собой повторную реализацию средства доказательства теорем Lean, способного создавать код C , который затем компилируется, что позволяет разработать эффективную автоматизацию для конкретной предметной области. [3] Lean 4 также содержит систему макросов и улучшенные процедуры синтеза классов типов и управления памятью по сравнению с предыдущей версией. Еще одним преимуществом по сравнению с Lean 3 является возможность не затрагивать код C++ для изменения внешнего интерфейса и других ключевых частей базовой системы, поскольку теперь все они реализованы в Lean и доступны конечному пользователю для переопределения при необходимости. [ нужна ссылка ]
Lean 4 не имеет обратной совместимости с Lean 3. [4]
В 2023 году была создана Lean FRO с целью улучшения масштабируемости и удобства использования языка, а также реализации автоматизации доказательства . [5]
Обзор [ править ]
Библиотеки [ править ]
Официальный пакет Lean включает стандартную библиотеку std4 , которая реализует общие структуры данных , которые можно использовать как для математических исследований, так и для более традиционной разработки программного обеспечения. [6]
В 2017 году начался поддерживаемый сообществом проект по разработке математической библиотеки бережливой библиотеки с целью оцифровать как больше чистой математики в одной большой сплоченной библиотеке, вплоть до математики исследовательского уровня. можно [7] [8] По состоянию на ноябрь 2023 года mathlib формализовал более 127 000 теорем и 70 000 определений в Lean. [9]
Интеграция редакторов [ править ]
Lean интегрируется с: [10]
Взаимодействие осуществляется через клиентское расширение и сервер протокола языкового сервера .
Он имеет встроенную поддержку символов Unicode , которые можно вводить с использованием последовательностей, подобных LaTeX , например «\times» вместо «×». Lean также может быть скомпилирован в JavaScript и доступен в веб-браузере, а также имеет обширную поддержку метапрограммирования .
Примеры (бережливое производство 4) [ править ]
Натуральные числа можно определить как индуктивный тип . Это определение основано на аксиомах Пеано и гласит, что каждое натуральное число либо равно нулю, либо является потомком некоторого другого натурального числа.
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
Сложение натуральных чисел можно определить рекурсивно , используя сопоставление с образцом .
def Nat.add : Nat → Nat → Nat
| n, Nat.zero => n -- n + 0 = n
| n, Nat.succ m => Nat.succ (Nat.add n m) -- n + succ(m) = succ(n + m)
Это простое доказательство в бережливом режиме с использованием тактического режима:
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
intro h -- assume p ∧ q with proof h, the goal is q ∧ p
apply And.intro -- the goal is split into two subgoals, one is q and the other is p
· exact h.right -- the first subgoal is exactly the right part of h : p ∧ q
· exact h.left -- the second subgoal is exactly the left part of h : p ∧ q
Это же доказательство в терминальном режиме:
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
fun ⟨hp, hq⟩ => ⟨hq, hp⟩
Использование [ править ]
Математика [ править ]
Бережливое производство привлекло внимание таких математиков, как Томас Хейлз. [11] и Кевин Баззард . [12] Хейлз использует его для своего проекта Formal Abstracts. [13] Баззард использует его для проекта Зена. [14] Одна из целей проекта «Зена» — переписать каждую теорему и доказательство в учебной программе по математике для студентов Имперского колледжа Лондона в Lean.
В 2021 году группа исследователей использовала Lean для проверки правильности доказательства Питера Шольце в области сокращенной математики . Проект привлек внимание благодаря формализации результатов на переднем крае математических исследований. [15] В 2023 году Теренс Тао использовал Lean, чтобы формализовать доказательство полиномиальной гипотезы Фреймана-Рузсы (PFR), результат, опубликованный Тао и его сотрудниками в том же году. [16]
Искусственный интеллект [ править ]
В 2022 году OpenAI создала нейронных сетей средство доказательства теорем для Lean на основе , которое использовало языковую модель для генерации доказательств различных олимпиадных задач на уровне средней школы. [17]
Позже в том же году Meta AI создала модель ИИ, которая решила 10 Международной математической олимпиады задач ; эта модель доступна для публичного использования в среде Lean. [18]
См. также [ править ]
Ссылки [ править ]
- ^ https://pp.ipd.kit.edu/uploads/publikationen/demoura21lean4.pdf
- ^ "О" . Бережливый язык . Проверено 13 марта 2024 г.
- ^ Моура, Леонардо де; Ульрих, Себастьян (2021). Платцер, Андре; Сатклифф, Джефф (ред.). Автоматизированный вычет -- CADE 28 . Международное издательство Спрингер. стр. 625–635. дои : 10.1007/978-3-030-79876-5_37 . ISBN 978-3-030-79876-5 . S2CID 235800962 . Проверено 24 марта 2023 г.
- ^ «Значительные изменения по сравнению с Lean 3» . Бережливое руководство . Проверено 24 марта 2023 г.
- ^ «Миссия» . Наклониться ФРО . 25 июля 2023 г. Проверено 14 марта 2024 г.
- ^ "стд4" . Гитхаб . Проверено 13 марта 2024 г.
- ^ «Создание математической библиотеки будущего» . Журнал Кванта . Архивировано из оригинала 2 октября 2020 года.
- ^ «Бережливое сообщество» . LeanProver-community.github.io . Проверено 24 октября 2023 г.
- ^ «Статистика Mathlib» . LeanProver-community.github.io . Проверено 1 ноября 2023 г.
- ^ «Установка Lean 4 в Linux» . LeanProver-community.github.io . Проверено 24 октября 2023 г.
- ^ Хейлз, Томас (18 сентября 2018 г.). «Обзор средства доказательства теорем бережливого производства» . Джиггер Вит . Архивировано из оригинала 21 ноября 2020 года.
- ^ Баззард, Кевин. «Будущее математики?» (PDF) . Проверено 6 октября 2020 г.
- ^ «Формальные рефераты» . Гитхаб .
- ^ «Что такое проект Зена?» . Зена . 8 мая 2019 г.
- ^ Хартнетт, Кевин (28 июля 2021 г.). «Помощник по доказательству переходит в высшую математику» . Журнал Кванта . Архивировано из оригинала 2 января 2022 года.
- ^ Сломан, Лейла (06 декабря 2023 г.). « Команда математики доказывает критическую связь между сложением и множествами» . Журнал Кванта . Проверено 7 декабря 2023 г.
- ^ «Решение (некоторых) формальных олимпиадных задач по математике» . ОпенАИ . 2 февраля 2022 г. . Проверено 13 марта 2024 г.
- ^ «Обучение ИИ продвинутым математическим рассуждениям» . Мета ИИ . 3 ноября 2022 г. . Проверено 13 марта 2024 г.
Внешние ссылки [ править ]
- Бережливый веб-сайт
- Веб-сайт сообщества бережливого производства
- Бережливое ФРО
- Игра «Натуральные числа» — интерактивное руководство по изучению бережливого производства.
Инструменты разработки Microsoft |
|---|
- Языки программирования, созданные в 2013 году.
- Помощники по доказательствам
- Зависимо типизированные языки
- Образовательное математическое программное обеспечение
- Функциональные языки
- Бесплатное программное обеспечение с открытым исходным кодом
- Бесплатное программное обеспечение, написанное на C++.
- бесплатное программное обеспечение Майкрософт
- Языки программирования Майкрософт
- Microsoft Исследования
- Программное обеспечение, использующее лицензию Apache
- Бесплатное математическое программное обеспечение
- Программные системы для доказательства теорем