设置 | 登录 | 注册

定下计划

明天继续学习lean4数学形式化,教程学会以后,对看过的一些数学书做形式化
悄悄打开魔盒 2-14 圆环之理 (点击/回复: 204/1)

lean4中文教程

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

lean4的简单程序

-- 两横线后面是注释-- 计算#eval 12+12 -- 计算,结果是24
-- 类型检查
def f (x :ℕ) :=  x + 3
#check f -- 类型检...
悄悄打开魔盒 5-4 啊啊是谁都对 (点击/回复: 639/6)

lean4教程

https://leanprover-community.github.io/mathematics_in_lean/
这个教程是关于如何用lean4和mathlib4做数学的
https...
悄悄打开魔盒 5-2 悄悄打开魔盒 (点击/回复: 666/3)

听上去lean4可以用来做数学证明题

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

简介&安装教程

lean是一款数学形式化语言,它可以用编程语言撰写数学证明,便于计算机进行形式验证,因此一定程度上可以避免人工检查数学证明所带来的负担和错误。
类似的语言有coq,isabelle,metama...
悄悄打开魔盒 5-2 悄悄打开魔盒 (点击/回复: 392/1)

您好,Purasbar 欢迎您的到来~

亲爱的用户:欢迎来到lean4吧,Purasbar欢迎您的到来~
请先阅读我们的社区准则:
https://zh.purasbar.com/documents/eula/
以...
社区管理员 5-2 社区管理员 (点击/回复: 300/0)
本吧共有主题数7个,帖子数23篇,会员0位。

内容转换:

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