lean4吧_Purasbar

25000行代码的素数定理证明，20万行代码的球堆积问题证明，规模越来越大

悄悄打开魔盒 00:52 悄悄打开魔盒 (點擊/回復: 22/1)

明天继续学习lean4数学形式化，教程学会以后，对看过的一些数学书做形式化

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

https://lixiang90.github.io/mathematics_in_lean_CN/index.html
翻译进行中
英文原版见：
https://leanprov...

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

-- 两横线后面是注释-- 计算#eval 12+12 -- 计算，结果是24
-- 类型检查
def f (x :ℕ) := x + 3
#check f -- 类型检...

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

https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的
https...

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

如题

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

lean是一款数学形式化语言，它可以用编程语言撰写数学证明，便于计算机进行形式验证，因此一定程度上可以避免人工检查数学证明所带来的负担和错误。
类似的语言有coq，isabelle，metama...

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

亲爱的用户：欢迎来到lean4吧，Purasbar欢迎您的到来~
请先阅读我们的社区准则：
https://zh.purasbar.com/documents/eula/
以...

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

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