Lean

Lean е функционален език за програмиране и интерактивен доказател на теореми (proof assistant), разработен първоначално от Леонардо де Моура в Microsoft Research, а впоследствие поддържан от организацията с нестопанска цел Lean FRO.

Най-новата му основна версия, Lean 4, е широко използвана от математическата общност за компютърно формализиране и автоматично верифициране на сложни математически доказателства, предоставяйки т.нар. „машинно проверими сертификати“. Благодарение на математическата строгост на Lean, изследователските лаборатории за изкуствен интелект го използват за валидиране на резултати, генерирани от невронни мрежи, елиминирайки проблема с халюцинациите в научните публикации.