Biblioteker skrevet i Lean

Lean 4 programmeringssprog og teorembeviser.

Lean matematiske komponenter bibliotek.

Demo til en højpræstationstype-teori-uddybning.

Enkel verifikation af Rust-programmer via funktionel oprensning i Lean 2(!).

Opbygning af de naturlige tal i Lean..

Arbejder i gang mathlib port til lean 4.

💧 Liquid Tensor Experiment.

En simpel raytracer skrevet i Lean 4.

Ledsagende filer til logisk verifikation 2020–2021 på VU Amsterdam.

HoTT i Lean 3.

Samling af benchmarks for funktionelle programmeringssprog og korrekturassistenter..

Lean-uafhængig implementering af MM-Lean linket.