設置 | 登錄 | 註冊

目前共有2篇帖子。

简介&安装教程

1樓 悄悄打开魔盒 2024-5-2 11:21
lean是一款数学形式化语言,它可以用编程语言撰写数学证明,便于计算机进行形式验证,因此一定程度上可以避免人工检查数学证明所带来的负担和错误。

类似的语言有coq,isabelle,metamath等


lean4是lean的第四个版本,和lean3相比有很大改进。


除了lean官方的核心程序以外,lean社区还维护一个称为mathlib的库,它包含人类发展出的大多数数学领域的基本定义,公理,定理等。目前mathlib也已经更新到和lean4适配的mathlib4. 


lean4安装方法:

1. 安装VS Code

2. 在VS Code中安装扩展程序lean4

3. 创建新文件,语言选lean4,此时会自动下载安装lean4

4. 左边的输入窗口输入#eval 18 + 19,右边的信息窗口如果显示37,则说明安装完成


要导入数学定理库(例如mathlib4),参考https://github.com/leanprovercommunity/mathlib4/wiki/Using-mathlib4-as-a-dependency

2樓 悄悄打开魔盒 2024-5-2 11:23

內容轉換:

回覆帖子
內容:
用戶名: 您目前是匿名發表。
驗證碼:
看不清?換一張
©2010-2025 Purasbar Ver3.0 [手機版] [桌面版]
除非另有聲明,本站採用知識共享署名-相同方式共享 3.0 Unported許可協議進行許可。