| |
点击 |
回复 |
标题 |
作者 |
最后回复 |
| |
76 |
1 |
https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻译进行中
英文原版见：
https://le... |
悄悄打开魔盒 |
6-9 啊啊是谁都对 |
| |
128 |
6 |
-- 两横线后面是注释-- 计算#eval 12+12 -- 计算，结果是24
-- 类型检查
def f (x :ℕ) := x + 3
#check f... |
悄悄打开魔盒 |
5-4 啊啊是谁都对 |
| |
120 |
3 |
https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的
h... |
悄悄打开魔盒 |
5-2 悄悄打开魔盒 |
| |
91 |
4 |
如题 |
啊啊是谁都对 |
5-2 啊啊是谁都对 |
| |
80 |
1 |
lean是一款数学形式化语言，它可以用编程语言撰写数学证明，便于计算机进行形式验证，因此一定程度上可以避免人工检查数学证明所带来的负担和错误。
类似的语言有coq，isabelle，meta... |
悄悄打开魔盒 |
5-2 悄悄打开魔盒 |
| |
39 |
0 |
亲爱的用户：欢迎来到lean4吧，Purasbar欢迎您的到来~
请先阅读我们的社区准则：
https://zh.purasbar.com/documents/eula... |
社区管理员 |
5-2 社区管理员 |
档案 
载入中...