| |
點擊 |
回復 |
標題 |
作者 |
最後回復 |
| |
76 |
1 |
明天继续学习lean4数学形式化，教程学会以后，对看过的一些数学书做形式化 |
悄悄打开魔盒 |
2-14 圆环之理 |
| |
284 |
1 |
https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻译进行中
英文原版见：
https://leanprov... |
悄悄打开魔盒 |
6-9 啊啊是谁都对 |
| |
404 |
6 |
-- 两横线后面是注释-- 计算#eval 12+12 -- 计算，结果是24
-- 类型检查
def f (x :ℕ) := x + 3
#check f -- 类型检... |
悄悄打开魔盒 |
5-4 啊啊是谁都对 |
| |
462 |
3 |
https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的
https... |
悄悄打开魔盒 |
5-2 悄悄打开魔盒 |
| |
347 |
4 |
如题 |
啊啊是谁都对 |
5-2 啊啊是谁都对 |
| |
280 |
1 |
lean是一款数学形式化语言，它可以用编程语言撰写数学证明，便于计算机进行形式验证，因此一定程度上可以避免人工检查数学证明所带来的负担和错误。
类似的语言有coq，isabelle，metama... |
悄悄打开魔盒 |
5-2 悄悄打开魔盒 |
| |
196 |
0 |
亲爱的用户：欢迎来到lean4吧，Purasbar欢迎您的到来~
请先阅读我们的社区准则：
https://zh.purasbar.com/documents/eula/
以... |
社区管理员 |
5-2 社区管理员 |
檔案 
載入中...