Lean Interactive Theorem Prover

Lean е интерактивна система за доказване на математически теореми и функционален език за програмиране, разработен от Microsoft Research. Той предоставя формално валидирана среда, в която сложни математически доказателства се преобразуват в компютърно проверим код, служейки като безпогрешен арбитър срещу халюцинациите на изкуствения интелект.