Словарь
Lean
Язык программирования и система интерактивного доказательства теорем, в которой каждый логический шаг проверяется компьютером. Применяется для формализации математики (в том числе в библиотеке mathlib) и для проверки доказательств, полученных людьми или моделями ИИ; корректность вывода гарантируется только при верно записанной формулировке.