Lean

2024年8月10日 (六) 11:28的最后版本

您可以在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官网