Lean

Lean – функційна мова програмування, що використовується як асистент доведення теорем. Базується на численні конструкцій.

Lean
Парадигма	Функційне програмування
Дата появи	2013
Розробник	Microsoft Research
Останній реліз	4.1.0 (25 вересня, 2023; 9 місяців тому (2023-09-25))
Тестова версія	v4.2.0-rc1 (26 вересня, 2023; 9 місяців тому (2023-09-26))
Система типізації	Статична, сильна, з виведенням
Під впливом від	ML, Coq, Haskell
Мова реалізації	, Lean
Платформа	кросплатформова програма
Операційна система	кросплатформова програма
Ліцензія	Apache License 2.0
Репозиторій вихідного коду	github.com/leanprover/lean4
Вебсайт	leanprover.github.io

Проєкт Lean заснований у 2013 році Леонардом де Моура, який на той час працював у Microsoft Research. Проєкт має відкритий сирцевий код та поширюється на умовах дозвільної ліцензії Apache.

Система Lean здобула прихильність деяких математиків, зокрема, (автора доведення гіпотези Кеплера) та Кевіна Баззарда. Останній заснував проєкт Xena, на меті якого формалізувати кожну математичну теорему із бакалаврського курсу математики в Імперському коледжі Лондона.

У 2021 році Lean було використано для формалізації доведення нової теореми Петера Шольце в галузі ^[en], у доведенні якої він не був цілком упевнений. Формалізацію було завершено за пів року групою волонтерів під керівництвом Йогана Коммеліна (Johan Commelin). Таким чином було показано, що система Lean може бути корисною у передовій математиці.

Див. також

• Coq

Примітки

1. . Архів оригіналу за 18 жовтня 2021. Процитовано 5 жовтня 2023.
2. Hales, Thomas (18 вересня 2018). A Review of the Lean Theorem Prover. Процитовано 6 жовтня 2020.
3. Buzzard, Kevin. The Future of Mathematics? (PDF). Процитовано 6 жовтня 2020.
4. What is the Xena project?. Xena (англ.). 8 травня 2019.
5. Hartnett, Kevin (28 липня 2021). Proof Assistant Makes Jump to Big-League Math. Quanta Magazine.