Lean 4

Lean 4 е интерактивен инструмент за доказване на теореми и пълнофункционален език за програмиране, разработен от Леонардо де Моура в Microsoft Research.

Архитектура и възможности

1. Изчислително ядро (Kernel): Малко, математически валидирано ядро, което гарантира абсолютната синтактична коректност на всяко прието доказателство.
2. Зависими типове (Calculus of Inductive Constructions): Изразяване на математически обекти и свойства директно в типовата система.
3. Mathlib библиотека: Огромна, постоянно нарастваща отворена библиотека от формализирана модерна математика.
4. AI интеграция: Водеща платформа за валидиране на генерирани от изкуствен интелект доказателства без риск от халюцинации.

Lean 4 се утвърди като златен стандарт за формализация в академичната математика и софтуерната верификация.