Các thư viện được viết bằng Lean

Ngôn ngữ lập trình Lean 4 và chứng minh định lý.

Thư viện thành phần toán học tinh gọn.

Bản trình diễn để xây dựng lý thuyết loại hiệu suất cao.

Xác minh đơn giản các chương trình Rust thông qua thanh lọc chức năng trong Lean 2(!).

Xây dựng các số tự nhiên trong Lean..

Đang tiến hành cổng mathlib cho lean 4.

💧 Thí nghiệm Tenor lỏng.

Một raytracer đơn giản được viết bằng Lean 4.

Các tệp đồng hành cho Xác minh hợp lý 2020–2021 tại VU Amsterdam.

HoTT trong Lean 3.

Bộ sưu tập các điểm chuẩn của ngôn ngữ lập trình chức năng và trợ lý bằng chứng..

Triển khai độc lập tinh gọn của liên kết MM-Lean.