| |
點擊 |
回復 |
標題 |
作者 |
最後回復 |
| |
85 |
1 |
明天繼續學習lean4數學形式化，教程學會以後，對看過的一些數學書做形式化 |
悄悄打开魔盒 |
2-14 圆环之理 |
| |
294 |
1 |
https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻譯進行中
英文原版見：
https://leanprov... |
悄悄打开魔盒 |
6-9 啊啊是谁都对 |
| |
419 |
6 |
-- 兩橫線後面是注釋-- 計算#eval 12+12 -- 計算，結果是24
-- 類型檢查
def f (x :ℕ) := x + 3
#check f -- 類型檢... |
悄悄打开魔盒 |
5-4 啊啊是谁都对 |
| |
471 |
3 |
https://leanprover-community.github.io/mathematics_in_lean/
這個教程是關於如何用lean4和mathlib4做數學的
https... |
悄悄打开魔盒 |
5-2 悄悄打开魔盒 |
| |
363 |
4 |
如題 |
啊啊是谁都对 |
5-2 啊啊是谁都对 |
| |
289 |
1 |
lean是一款數學形式化語言，它可以用程式語言撰寫數學證明，便於計算機進行形式驗證，因此一定程度上可以避免人工檢查數學證明所帶來的負擔和錯誤。
類似的語言有coq，isabelle，metama... |
悄悄打开魔盒 |
5-2 悄悄打开魔盒 |
| |
205 |
0 |
親愛的用戶：歡迎來到lean4吧，Purasbar歡迎您的到來~
請先閱讀我們的社區準則：
https://zh.purasbar.com/documents/eula/
以... |
社区管理员 |
5-2 社区管理员 |
檔案 
載入中...