数学界是否被困在Lean中？

Are We Stuck with Lean?

▲ 153jjgreen65 HN 评论区
数学界是否被困在Lean中？

三年前，Lean 似乎只是众多证明助手中的一个选择，但如今它已占据主导地位。我提出疑问：是否有组织愿意支持 Lean 的替代品？Metamath 因其基于集合论和 Metamath Zero 的高正确性保障而成为有力竞争者。尽管 Lean 拥有 Mathlib 等强大生态，但其内核性能问题和类型论哲学争议仍存。随着 AI 生成形式化数学能力的提升，构建其他证明助手的库已不再遥不可及。我们不应因惯性而放弃探索更可靠、基于集合论的替代方案，这对整个数学社区至关重要。

我们被困在 Lean 中，就像当年被困在 Internet Explorer 中一样。
阅读原文 →HN 评论区RSS

HN 评论区

65
  1. dwheeler

    Metamath 贡献者在此！每个证明工具有其优缺点，但很高兴看到 Metamath 被提及 :-)。

    Metamath 的一个酷点是公理并非内置。诚然，最常用的系统基于经典逻辑和 ZFC 集合论 https://us.metamath.org/mpeuni/mmset.html……但你不必非用这个系统不可。有一个维护良好的数据库使用直觉逻辑：https://us.metamath.org/ileuni/mmil.html；还有一个基于所谓的“新基础”（New Foundations，一种多排序系统）：https://us.metamath.org/nfeuni/mmnf.html；以及基于 HOL 的：https://us.metamath.org/holuni/mmhol.html；如果你想的话，甚至可以自己创建一个。

    在 Metamath 中，证明绝不隐藏任何东西。没有那种“显而易见”的手挥式省略。证明中的每一步都必须由某个公理或先前已证的定理严格且直接地证明，绝无例外。这也意味着虽然寻找证明可能很难，但验证证明却很快。我刚刚运行了一次证明验证，在 6.35 秒内验证了超过 47,000 个定理。在 Metamath Proof Explorer / set.mm 数据库（即那个使用经典逻辑和 ZFC 的库）中，我们常规地对每个提议的更改运行由不同人编写的多个证明器。因此，内核不仅很小，而且由多个不同的程序实现，这使得我们接受无效证明的可能性极低。

    这是我几年前制作的总结 Metamath 的视频：https://www.youtube.com/watch?v=8WH4Rd4UKGE

  2. seanhunter

    我觉得很奇怪，那些不用 Lean 的人为什么不直接去使用替代方案，而不是试图让所有正在使用 Lean 的人改用别的东西。这感觉就像全世界所有的 emacs 用户试图强迫所有 vim 用户改用 emacs 一样。

    直面现实很重要：并非所有数学家都会在同一套工具上进行协作（尽管表面上看这似乎是个很棒的成果）。人是不同的，需求也不同，人们在不同环境下生产力也不同。特别是，那些希望在标准框架（包括 zfc）内形式化结果的人，作为一个群体，永远不会太在意 Lean4 不允许他们在 zfc 之外形式化结果这件事。

  3. Syzygies

    https://github.com/Syzygies/Compare

    在从 Haskell 切换到 Lean 以开启我数学研究的新阶段之前，我花了太长时间比较了数十种语言，其中只有一部分属于上述项目。对我而言，Lean 胜出，甚至无需考虑或使用依赖类型（至少目前是这样）。它仅仅是一种比我见过的任何语言都更好的编程语言。

    这对那些对证明感兴趣的人来说是一个关键优势。人们使用与编写证明相同的语言来编写 tactic。

    https://github.com/Syzygies/Compare/blob/main/source/lean/Na...

    我未来确实对证明感兴趣，这让 Lean 对我更有优势。我更喜欢以视觉形式进行符号推理。我预见未来我们会绘制并查看 AI 生成的绘图，而任何源自印刷术的符号都将像楔形文字一样显得过时。上图是表示“自然数游戏”（The Natural Number Game）中第一个 Lean 证明的一种可能语言。向我展示这个的数学家中，大约十分之一的人能比理解 Lean 符号更快地掌握它。而另外九个人则把可视化编程语言想象成 PowerPoint 幻灯片或儿童图形语言，看不出其意义。

  4. touisteur

    最近没怎么看到关于 SPARK 和 why3 结合前沿大语言模型（LLMs）的讨论。看起来，从实际实现出发逐步证明属性（从消除运行时错误到部分功能证明，如果成本允许再到完整功能证明），而只将 Lean 的精力集中在 why3（及其众多的 SMT 证明器）放弃的地方，似乎更容易？

    此外，由于 SPARK 中的验证非常模块化，这似乎也高度适合代理（agent）化。

  5. 7373737373

    Metamath 的 Python 验证器——其可信内核——只有不到 700 行 Python 代码：https://github.com/david-a-wheeler/mmverify.py/blob/master/m...

    Metamath Zero 的 Haskell 实现是 700 行，C 实现是 1000 行（总共 1800 行）https://github.com/digama0/mm0

    其他证明系统如何比较？

    一些 Bug 数量统计：https://tristan.st/blog/in_search_of_falsehood

同日更多故事

2026-07-30