Bibliotecas escritas em Lean

Linguagem de programação Lean 4 e provador de teoremas.

Biblioteca de componentes matemáticos enxutos.

Demonstração para elaboração de teoria de tipos de alto desempenho.

Verificação simples de programas Rust via purificação funcional em Lean 2(!).

Construindo os números naturais em Lean..

Trabalho em andamento da porta mathlib para lean 4.

💧 Experimento do Tensor Líquido.

Um raytracer simples escrito em Lean 4.

Arquivos complementares para verificação lógica 2020–2021 na VU Amsterdam.

HoTT em Lean 3.

Coleção de benchmarks de linguagens de programação funcionais e assistentes de prova.

Implementação Lean-independente do link MM-Lean.