Lean

您可以在Wikipedia上了解到此条目的英文信息 Lean Thanks, Wikipedia.

Lean

简介

Lean 是一种定理验证器（theorem prover）和编程语言，它是基于具有归纳类型（inductive types）的构造微积分（calculus of constructions）。

项目

• Projects using Lean
• Lean mathlib
• Metamath Zero 包含一些工具和验证器以及以 Metamath Zero 语言为中心的规范组成，支持 Haskell, Lean, Rust, C.
• electrolysis import Rust to Lean

链接

• Lean官网
• Lean 4 @ GitHub