Lean (помощник по проверке)
Помощник по проверке и язык программирования
Наклонять
ПарадигмаФункциональное программирование , Императивное программирование
СемьяПомощник по проверке
РазработчикLean FRO
Впервые появился2013 ; 11 лет назад ( 2013 )
Стабильный релиз
4.11.0 / 1 сентября 2024 г. ; 58 дней назад ( 2024-09-01 )
Предварительный релиз
4.12.0-rc1 / 2 сентября 2024 г. ; 57 дней назад ( 2024-09-02 )
Дисциплина печатиСтатичный , сильный , предполагаемый
Язык реализацииБережливый, C++
ОСКроссплатформенный
ЛицензияЛицензия Apache 2.0
Веб-сайтlean-lang.org
Под влиянием
ML
Coq
Haskell

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 включает стандартную библиотеку battery , которая реализует общие структуры данных , которые могут использоваться как для математических исследований, так и для более традиционной разработки программного обеспечения. [6]

В 2017 году начался поддерживаемый сообществом проект по разработке библиотеки Lean mathlib с целью оцифровать как можно больше чистой математики в одной большой связной библиотеке, вплоть до исследовательского уровня математики. [7] [8] По состоянию на сентябрь 2024 года mathlib формализовал более 165 000 теорем и 85 000 определений в Lean. [9]

Интеграция редакторов

Lean интегрируется с: [10]

Взаимодействие осуществляется через клиентское расширение и сервер протокола языкового сервера .

Он имеет встроенную поддержку символов Unicode , которые можно вводить с помощью последовательностей, подобных LaTeX , например, "\times" для "×". Lean также можно скомпилировать в JavaScript и получить к нему доступ в веб-браузере, а также он имеет обширную поддержку метапрограммирования .

Примеры (Lean 4)

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

индуктивный  Nat  :  Тип |  ноль  :  Nat |  сукц  :  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)

Это простое доказательство для двух предложений и (где есть конъюнкция и импликация ) в Lean с использованием тактического режима: ( П ∧ В ) ⟹ ( В ∧ П ) {\displaystyle (P\клин Q)\подразумевает (Q\клин P)} П {\displaystyle P} В {\displaystyle Q} ∧ {\displaystyle \клин} ⟹ {\displaystyle \подразумевает} 

теорема  and_swap  ( p  q  :  Prop )  :  p  ∧  q  →  q  ∧  p  :=  по  вступлению  h  -- предположим, что p ∧ q с доказательством h, цель q ∧ p  применить  And.intro  -- цель разделена на две подцели, одна q, а другая p  ·  exact  h.right  -- первая подцель в точности правая часть h : p ∧ q  ·  exact  h.left  -- вторая подцель в точности левая часть h : p ∧ q

Это же доказательство в терминологическом режиме:

теорема  and_swap  ( p  q  :  Prop )  :  p  ∧  q  →  q  ∧  p  :=  fun  ⟨ hp ,  hq ⟩  =>  ⟨ hq ,  hp ⟩

Использование

Математика

Lean привлек внимание таких математиков, как Томас Хейлз , [11] Кевин Баззард , [12] и Хезер Макбет. [13] Хейлз использует его для своего проекта Formal Abstracts. [14] Баззард использует его для проекта Xena. [15] Одна из целей проекта Xena — переписать каждую теорему и доказательство в программе бакалавриата по математике в Имперском колледже Лондона на Lean. Макбет использует Lean для обучения студентов основам математического доказательства с мгновенной обратной связью. [16]

В 2021 году группа исследователей использовала Lean для проверки правильности доказательства Питера Шольце в области сжатой математики . Проект привлек внимание формализацией результата на переднем крае математических исследований. [17] В 2023 году Теренс Тао использовал Lean для формализации доказательства гипотезы полиномиального Фреймана-Ружи (PFR), результат был опубликован Тао и его коллегами в том же году. [18]

Искусственный интеллект

В 2022 году OpenAI и Meta AI независимо друг от друга создали модели ИИ для генерации доказательств различных задач олимпиад на уровне средней школы по Lean. [19] Модель Meta AI доступна для публичного использования в среде Lean. [20]

В 2023 году Влад Тенев и Тудор Ахим совместно основали стартап Harmonic, цель которого — уменьшить галлюцинации ИИ путем генерации и проверки Lean-кода. [21]

В 2024 году Google DeepMind создал AlphaProof [22] , который доказывает математические утверждения в Lean на уровне серебряного призера Международной математической олимпиады . Это была первая система ИИ, которая достигла достойного медали результата при решении задач математической олимпиады. [23]


Смотрите также

Ссылки

  1. ^ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, André; Sutcliffe, Geoff (ред.). «The Lean 4 Theorem Prover and Programming Language». Автоматизированная дедукция – CADE 28 . Cham: Springer International Publishing: 625–635. doi : 10.1007/978-3-030-79876-5_37 . ISBN 978-3-030-79876-5.
  2. ^ "О". Lean Language . Получено 2024-03-13 .
  3. ^ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff (ред.). Автоматизированная дедукция — CADE 28. Springer International Publishing. стр. 625–635. doi :10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5. S2CID  235800962 . Получено 24 марта 2023 г. .
  4. ^ "Значительные изменения по сравнению с Lean 3". Lean Manual . Получено 24 марта 2023 г. .
  5. ^ "Миссия". Lean FRO . 2023-07-25 . Получено 2024-03-14 .
  6. ^ "batteries". GitHub . Получено 2024-09-22 .
  7. ^ "Создание математической библиотеки будущего". Журнал Quanta . Архивировано из оригинала 2 октября 2020 г.
  8. ^ "Lean community". leanprover-community.github.io . Получено 2023-10-24 .
  9. ^ "Статистика Mathlib". leanprover-community.github.io . Получено 2024-09-22 .
  10. ^ "Установка Lean 4 на Linux". leanprover-community.github.io . Получено 2023-10-24 .
  11. ^ Хейлз, Томас (18 сентября 2018 г.). «Обзор Lean Theorem Prover». Jigger Wit . Архивировано из оригинала 21 ноября 2020 г.
  12. ^ Баззард, Кевин. «Будущее математики?» (PDF) . Получено 6 октября 2020 г.
  13. ^ Макбет, Хезер. «Механика доказательства». hrmacbeth.github.io . Архивировано из оригинала 5 июня 2024 г.
  14. ^ "Формальные аннотации". Github .
  15. ^ «Что такое проект Зена?». Зена . 8 мая 2019 г.
  16. ^ Робертс, Сиобхан (2 июля 2023 г.). «ИИ тоже придет в математику». New York Times . Архивировано из оригинала 1 мая 2024 г.
  17. ^ Хартнетт, Кевин (28 июля 2021 г.). «Proof Assistant Makes Jump to Big-League Math». Журнал Quanta . Архивировано из оригинала 2 января 2022 г.
  18. ^ Сломан, Лейла (2023-12-06). «Команда математиков «А» доказывает критическую связь между сложением и множествами». Журнал Quanta . Получено 2023-12-07 .
  19. ^ "Решение (некоторых) формальных математических олимпиадных задач". OpenAI . 2 февраля 2022 г. Получено 13 марта 2024 г.
  20. ^ "Обучение ИИ передовым математическим рассуждениям". Meta AI . 3 ноября 2022 г. Получено 13 марта 2024 г.
  21. ^ Метц, Кейд (23 сентября 2024 г.). «Является ли математика путем к чат-ботам, которые ничего не выдумывают?». New York Times . Архивировано из оригинала 24 сентября 2024 г.
  22. ^ "ИИ достиг серебряной медали, решив задачи Международной математической олимпиады". Google DeepMind . 2024-05-14 . Получено 2024-07-25 .
  23. ^ Робертс, Сиобхан (25 июля 2024 г.). «Подвиньтесь, математики, вот и AlphaProof». New York Times . Архивировано из оригинала 29 июля 2024 г.
  • Бережливый веб-сайт
  • Сайт сообщества Lean
  • Lean FRO
  • Игра «Натуральные числа» — интерактивное руководство по бережливому мышлению
Взято с "https://en.wikipedia.org/w/index.php?title=Lean_(proof_assistant)&oldid=1254178588"