Lean

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(链接)
 
(未显示1个用户的3个中间版本)
第6行: 第6行:
 
==简介==
 
==简介==
 
Lean 是一种定理验证器(theorem prover)和编程语言,它是基于具有归纳类型(inductive types)的构造微积分(calculus of constructions)。
 
Lean 是一种定理验证器(theorem prover)和编程语言,它是基于具有归纳类型(inductive types)的构造微积分(calculus of constructions)。
 +
 +
==新闻==
 +
*[https://www.163.com/dy/article/IL9DAULT0511ABV6.html 陶哲轩使用Blueprint在Lean4中形式化多项式Freiman-Ruzsa猜想的证明过程] (2023.12.05)
  
 
==功能==
 
==功能==
第18行: 第21行:
 
*[https://github.com/digama0/mm0 Metamath Zero] 包含一些工具和验证器以及以 Metamath Zero 语言为中心的规范组成,支持 [[Haskell]], Lean, [[Rust]], [[C programming language|C]].
 
*[https://github.com/digama0/mm0 Metamath Zero] 包含一些工具和验证器以及以 Metamath Zero 语言为中心的规范组成,支持 [[Haskell]], Lean, [[Rust]], [[C programming language|C]].
 
*[https://github.com/Kha/electrolysis electrolysis] import [[Rust]] to Lean
 
*[https://github.com/Kha/electrolysis electrolysis] import [[Rust]] to Lean
 +
 +
==文档==
 +
*[https://leanprover.github.io/theorem_proving_in_lean/index.html Theorem Proving in Lean]
 +
 +
==图书==
  
 
==图集==
 
==图集==
第26行: 第34行:
 
[[category:formal]]
 
[[category:formal]]
 
[[category:proof assistant]]
 
[[category:proof assistant]]
[[category:lean]]
 
 
[[category:c++]]
 
[[category:c++]]
 
[[category:programming language]]
 
[[category:programming language]]
 +
[[category:Huihoo Foundation]]

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

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

Lean

Lean

目录

[编辑] 简介

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

[编辑] 新闻

[编辑] 功能

[编辑] 指南

[编辑] 项目

[编辑] 文档

[编辑] 图书

[编辑] 图集

[编辑] 链接

分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱