lean4吧_Purasbar

设置 | 登录 | 注册

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

悄悄打开魔盒 2-14 圆环之理 (点击/回复: 220/1)

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

悄悄打开魔盒 6-9 啊啊是谁都对 (点击/回复: 426/1)

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

悄悄打开魔盒 5-4 啊啊是谁都对 (点击/回复: 660/6)

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

悄悄打开魔盒 5-2 悄悄打开魔盒 (点击/回复: 675/3)

如題

啊啊是谁都对 5-2 啊啊是谁都对 (点击/回复: 521/4)

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

悄悄打开魔盒 5-2 悄悄打开魔盒 (点击/回复: 396/1)

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

社区管理员 5-2 社区管理员 (点击/回复: 302/0)

本吧共有主题数7个，帖子数23篇，会员数0位。

内容转换：