错误的，Lean 是有一个 trusted kernel 的，用 Lean 完成的证明可以导出到这个 kernel language 另外进行验证
Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory
大微软牛逼啊，他家还搞 dafny 么？印象中微软搞了三四个支持形式验证的语言。
Dafny 和 F★ 都没停止开发
这个是刺果果的硬广，你去看下官方说的 bare bone checker引用了多少行 lean C++ 代码，lean/src/checker at master · leanprover-community/lean · GitHub
这个
一般几万行以内代码都能叫 small kernel
这个是第三方的，他自己的是C++的。
几万行显然不能算 small kernel，几百几千行才算。
https://leanprover.github.io/lean4/doc/faq.html
哪怕 lean4也只说自己有 relatively small kernel，跟 lean3措辞一样的。
Coq 的 trusted kernel 就有 1.8 万行
还是你想说 Coq 也不是微内核？这样的话实际在用的proof assistant就没有微内核的了
实际上 small kernel 不是指具体代码行数小，而是说存在一个只有10来条公理的理想状态的 theory，可以把所有的证明转换到这个 theory 里。除了 NuPRL 系用了100多条公理，(dependent) type theory 的 pa 就没有用这么多的。
用 de Burijn criterion 就和代码实现基本脱钩了，Agda 连个 trusted core checker 都没有了，从 core theory 都是 CIC 来说 Lean 比 Coq 只少不多。从 NuPRL(3) 都能上榜我只能说这个标准真的挺宽松的。
顺带第一篇文章内容有点过时了，ACL2 自从完成了自己验证自己的大部分代码后也算 small kernel 了。第二篇文章是 2019 年写的居然没引用 https://www.semanticscholar.org/paper/A-self-verifying-theorem-prover-Moore-Davis/c4d7291fa179e15f3d7b668cd8593b56d74a4052 我怀疑作者不太了解 ACL2
第一篇认为 NuPRL 不满足，第二篇加了个 RedPRL/NuPRL 认为满足，是不是认为 RedPRL 满足？
最完美的 small kernel 是 HOL light，其它的就麻着胆子用吧，「反正还没发现新的 bug」
说起来定理证明界至今还没统一 proof object 语法吧，搞的交叉验证以及共享证明库都是虚幻，可惜。
2015 年之后的 NuPRL4 和 5 不是开源的，我都严重怀疑第二篇作者都没有自己试过用 NuPRL 就照着别人以前的评测写的， 因为 NuPRL4 之后就用的不是 LCF style approach ，而是根据 MetaPRL 重新写了个可以任意添加和屏蔽 inference rule 的解释器。RedPRL 是开源的，而且的确代码不多，只是有个最基本的 type checker。
NuPRL5 搞了这个 FDL，基本就是把定理 serialize 到一个数据库里，然后分享给 HOL 和 PVS 用，但是曾经只有 Cornell 和其他合作的组织内部在用，我只能通过公开的虚拟机 image 的功能大致猜测一下。
FDL 间接影响了 https://openmath.org 但是后者也没有什么 pa 有实装过。
1 个赞
第二篇是2019年的，作者给专家(可能是每个项目的开发者)发调查报告问出来的😄
GitHub - digama0/mm0: Metamath Zero specification language 这个项目评价如何？
在语法上，我只偏好 PFPL/NuPRL/MetaPRL/Lean4/Coq 那样在 proof object 之上能定制 syntax 的做法
请二位在这里讨论 Lean.
标题随便起的, 不太懂 Lean, 觉得不妥的可以自行修改
可怜的 HOL 和 Isabelle😄
大师推荐下形式证明方面的入门、进阶、高阶书籍？我挺感兴趣的，但是一直涉足不深。工具上，很喜欢 ACL2(Lisp嘛，带劲!)，HOL+Coq+Isabelle(ML家族，也挺带劲！)
一本书可以解决，看完就知道进阶怎么自己找资料
1 个赞
Program = Proof
Software Foundations https://softwarefoundations.cis.upenn.edu/lf-current/index.html
这两本书居然都是免费可读，作者好良心！
两本书的比较：Program = Proof | Lobsters
1 个赞
我的 Gopher 上有 Program = Proof 的 review gopher://gopher.club/1/users/ldbeth/
Program = Proof 虽然用的是 Agda，但实际上在 dependent type 之前的 higher order logic 內容也适用于 HOL，在 HoTT 之前的內容也适用于 Lean。
gopher 协议……这还真是让人挠头……有 http 协议访问的 URL 么？