lean4吧_Purasbar

設置 | 登錄 | 註冊

明天繼續學習lean4數學形式化，教程學會以後，對看過的一些數學書做形式化

悄悄打开魔盒 2-14 圆环之理 (點擊/回復: 76/1)

https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻譯進行中
英文原版見：
https://leanprov...

悄悄打开魔盒 6-9 啊啊是谁都对 (點擊/回復: 284/1)

-- 兩橫線後面是注釋-- 計算#eval 12+12 -- 計算，結果是24
-- 類型檢查
def f (x :ℕ) := x + 3
#check f -- 類型檢...

悄悄打开魔盒 5-4 啊啊是谁都对 (點擊/回復: 404/6)

https://leanprover-community.github.io/mathematics_in_lean/
這個教程是關於如何用lean4和mathlib4做數學的
https...

悄悄打开魔盒 5-2 悄悄打开魔盒 (點擊/回復: 462/3)

如題

啊啊是谁都对 5-2 啊啊是谁都对 (點擊/回復: 347/4)

lean是一款數學形式化語言，它可以用程式語言撰寫數學證明，便於計算機進行形式驗證，因此一定程度上可以避免人工檢查數學證明所帶來的負擔和錯誤。
類似的語言有coq，isabelle，metama...

悄悄打开魔盒 5-2 悄悄打开魔盒 (點擊/回復: 280/1)

親愛的用戶：歡迎來到lean4吧，Purasbar歡迎您的到來~
請先閱讀我們的社區準則：
https://zh.purasbar.com/documents/eula/
以...

社区管理员 5-2 社区管理员 (點擊/回復: 196/0)

本吧共有主題數7個，帖子數23篇，會員數0位。

內容轉換：