Lean 4

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

Той разчита на зависима теория на типовете (Calculus of Inductive Constructions), осигурявайки математическа непогрешимост при формалната верификация на математически теории и критични софтуерни системи. Lean 4 е златният стандарт за синтез между езикови модели и машинно проверими доказателства.