Lean

2024年8月10日 (六) 11:27的版本

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

Lean

简介

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

新闻

• 陶哲轩使用Blueprint在Lean4中形式化多项式Freiman-Ruzsa猜想的证明过程 (2023.12.05)

功能

指南

项目

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

文档

• Theorem Proving in Lean

图书

图集

链接

• Lean官网