定下计划明天继续学习lean4数学形式化，教程学会以后，对看过的一些数学书做形式化
|
lean4中文教程https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻译进行中 英文原版见： https://leanprov... |
lean4的简单程序-- 两横线后面是注释-- 计算#eval 12+12 -- 计算，结果是24
-- 类型检查 def f (x :ℕ) := x + 3 #check f -- 类型检... |
lean4教程https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的 https... |
|
简介&安装教程lean是一款数学形式化语言，它可以用编程语言撰写数学证明，便于计算机进行形式验证，因此一定程度上可以避免人工检查数学证明所带来的负担和错误。
类似的语言有coq，isabelle，metama... |
您好，Purasbar 欢迎您的到来~亲爱的用户：欢迎来到lean4吧，Purasbar欢迎您的到来~
请先阅读我们的社区准则： https://zh.purasbar.com/documents/eula/ 以... |
| There are 7 topics, 23 posts and 0 会员(s) in this bar. |
Content converter: |
