Lean

Lean
Тип	Proof assistant
Разработчик	Microsoft Research
Написана на	C++
Операционная система	Cross-platform
Языки интерфейса	английский
Первый выпуск	2013; 12 лет назад (2013)
Аппаратная платформа	кроссплатформенность
Последняя версия	v3.4.2 (18 января 2019; 6 лет назад (2019-01-18))
Тестовая версия	v4.0.0-m5 (7 августа 2022; 2 года назад (2022-08-07))
Репозиторий	github.com/leanprover/le…
Читаемые форматы файлов: Lean 3 file format[вд] и Lean 4 file format[вд]
Создаваемые форматы файлов: Lean 3 file format[вд] и Lean 4 file format[вд]
Лицензия	Apache License 2.0
Сайт	leanprover.github.io

Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году^[1].

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

1. ↑ Lean  (неопр.). Дата обращения: 30 сентября 2021. Архивировано 18 октября 2021 года.