设置 | 登录 | 注册

定下計劃

明天繼續學習lean4數學形式化,教程學會以後,對看過的一些數學書做形式化
悄悄打开魔盒 2-14 圆环之理 (点击/回复: 218/1)

lean4中文教程

https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻譯進行中
英文原版見:
https://leanprov...
悄悄打开魔盒 6-9 啊啊是谁都对 (点击/回复: 424/1)

lean4的簡單程序

-- 兩橫線後面是註釋-- 計算#eval 12+12 -- 計算,結果是24
-- 類型檢查
def f (x :ℕ) :=  x + 3
#check f -- 類型檢...
悄悄打开魔盒 5-4 啊啊是谁都对 (点击/回复: 659/6)

lean4教程

https://leanprover-community.github.io/mathematics_in_lean/
這個教程是關於如何用lean4和mathlib4做數學的
https...
悄悄打开魔盒 5-2 悄悄打开魔盒 (点击/回复: 673/3)

聽上去lean4可以用來做數學證明題

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

簡介&安裝教程

lean是一款數學形式化語言,它可以用編程語言撰寫數學證明,便於計算機進行形式驗證,因此一定程度上可以避免人工檢查數學證明所帶來的負擔和錯誤。
類似的語言有coq,isabelle,metama...
悄悄打开魔盒 5-2 悄悄打开魔盒 (点击/回复: 396/1)

您好,Purasbar 歡迎您的到來~

親愛的用戶:歡迎來到lean4吧,Purasbar歡迎您的到來~
請先閱讀我們的社區準則:
https://zh.purasbar.com/documents/eula/
以...
社区管理员 5-2 社区管理员 (点击/回复: 302/0)
本吧共有主题数7个,帖子数23篇,会员0位。

内容转换:

发表帖子
标题:
内容:
用户名: 您目前是匿名发表。
验证码:
看不清?换一张
©2010-2025 Purasbar Ver3.0 [手机版] [桌面版]
除非另有声明,本站采用知识共享署名-相同方式共享 3.0 Unported许可协议进行许可。