lean4吧_Purasbar

设置 | 登录 | 注册

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

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

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

悄悄打开魔盒 6-9 啊啊是谁都对 (点击/回复: 424/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 悄悄打开魔盒 (点击/回复: 674/3)

如题

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

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

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

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

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

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

内容转换：