Lean
инструмент интерактивного доказательства теорем / Материал из Википедии — свободной encyclopedia
Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году[1].
Краткие факты Тип, Разработчик ...
Lean | |
---|---|
Тип | Proof assistant |
Разработчик | Microsoft Research |
Написана на | C++ |
Операционная система | Cross-platform |
Языки интерфейса | английский |
Первый выпуск | 2013; 11 лет назад (2013) |
Аппаратная платформа | кроссплатформенность |
Последняя версия | v3.4.2 (18 января 2019; 5 лет назад (2019-01-18)) |
Тестовая версия | v4.0.0-m5 (7 августа 2022; 22 месяца назад (2022-08-07)) |
Репозиторий |
github.com/leanprover/le… github.com/leanprover/le… |
Лицензия | Apache License 2.0 |
Сайт | leanprover.github.io |
Закрыть
Lean имеет интерфейс, который отличает его от других интерактивных средств доказательства теорем. Lean может быть скомпилирован на JavaScript и доступен в веб-браузере. Он имеет встроенную поддержку символов Юникода. (Они могут быть набраны с использованием последовательностей, подобных применяемым в системе LaTeX, таких как "\times" для "×".) Lean также имеет обширную поддержку метапрограммирования.