metamath/set.mm

[](https://github.com/metamath/set.mm/actions?query=workflow%3Averifiers) # Metamath set.mm 仓库 这是一个经过严格验证的 [Metamath](https://us.metamath.org/) 数据库集合，它规定了数学公理以及 从这些公理推导出的定理的形式化证明。 ## 什么是 Metamath？ Metamath 是一种计算机语言及其配套的计算机程序，用于 存档、验证和研究数学证明。 与其他一些系统不同，Metamath 没有将特定的公理集 构建到系统中。相反，Metamath 语言简单且稳健， 几乎完全不存在硬编码的语法。 在 Metamath 中，您可以在数据库 （一组文本文件）中表达公理、定理及其证明。 为了证明一个定理，每个证明步骤*必须*使用公理或 先前已证明的定理来进行证明；因此，没有任何东西是隐藏的。 我们相信 Metamath 提供了尽可能简单的框架， 允许以绝对的严谨性表达几乎所有的数学内容。 生成的数据库提供了人类可读的公理和定理陈述。 我们在本仓库中压缩了证明，因此它们的证明占用相对 较少的空间，但工具可以轻松地将其解压缩，以提供 每个证明步骤的人类可读序列。 Metamath 验证速度极快；某些验证器可以在几秒钟内 重新验证可用的最大数据库。 有关更多信息，请参阅 [Metamath 主页](https://us.metamath.org/)、 [Metamath 证明浏览器主页](https://us.metamath.org/mpeuni/mmset.html)、 [Metamath 书籍](https://us.metamath.org#book) 或 视频“Metamath 证明浏览器：现代《数学原理》”(https://www.youtube.com/watch?v=8WH4Rd4UKGE)。 ## 此集合包含哪些数据库？ 包含的数据库及其生成展示的链接， 按（大致）递减的大小顺序排列如下： * “[set.mm](./set.mm)”，又称“Metamath 证明浏览器 (MPE)” - 使用经典逻辑和 带有选择公理的 Zermelo–Fraenkel 集合论 (ZFC)。 这是世界上最大的经过形式化验证的数学集合之一 （例如，它已完成 [形式化 100 个定理](https://www.cs.ru.nl/~freek/100/) 挑战列表中的许多挑战定理）； [此视频展示了 set.mm 截至 2020-04-29 的增长情况](https://www.youtube.com/watch?v=LVGSeDjWzUo)。 [[生成的展示](https://us.metamath.org/mpeuni/mmset.html)] * “[iset.mm](./iset.mm)”，又称“直觉主义逻辑浏览器” - 使用直觉主义集合论。 特别地，它不假设排中律在 所有情况下都必然成立。 [[生成的展示](https://us.metamath.org/ileuni/mmil.html)] * “[nf.mm](./nf.mm)”，又称“新基础浏览器” - 使用 Quine 的新基础 (NF) 集合论公理构建数学， 这是对最初在 Whitehead 和 Russell 的《数学原理》中提出的 “类型层级”集合论的直接衍生。 [[生成的展示](https://us.metamath.org/nfeuni/mmnf.html)] * “[ql.mm](./ql.mm)”，又称“量子逻辑浏览器” - 从 在 Hilbert 空间浏览器中证明的正交模格性质开始， 并带您进入量子逻辑。 [[生成的展示](https://us.metamath.org/qleuni/mmql.html)] * “[hol.mm](./hol.mm)”，又称“高阶逻辑浏览器” - 从 高阶逻辑（HOL，也称为简单类型论）开始，并推导出 ZFC 公理的等价物，从而连接这两种方法。 [[生成的展示](https://us.metamath.org/holuni/mmhol.html)] * “[peano.mm](./peano.mm)” - Peano 算术。 * “[big-unifier.mm](./big-unifier.mm)” - 用于 Metamath 验证器的统一和替换测试， 其中小的输入表达式会扩展到数千个符号。 它是 William McCune 为 OTTER 定理证明器编写的“big-unifier.in”的翻译版本。 * “[miu.mm](./miu.mm)” - 基于 Hofstadter 的工作， 用作演示的一个简单形式系统。 * “[demo0.mm](./demo0.mm)” - 在 Metamath 书籍第 2 章中 用作演示的一个简单形式系统。 也欢迎查看这个 [其他 Metamath 数据库列表](./other-databases.md)。 ## 数据库是如何验证的？ 我们努力提供*极高的*信心，以确保 这些数据库中的证明是完全正确的， 特别是对于 set.mm 和 iset.mm 数据库（ 正在积极开发的主要数据库）。 任何数据库的更改（“提交”）在被接受之前， 都会首先使用 GitHub actions 进行自动验证。 对 set.mm 和 iset.mm 的每一次更改都由许多独立的验证器进行验证， 包括也会检查标记的 metamath-exe，以及 检查定义可靠性的 mmj2。 所有其他数据库的证明在每次提交时都由 一个验证器 (metamath-exe) 进行验证。 有关更多信息，请参阅 [VERIFIERS.md](./verifiers.md)。 ## 致谢与纪念 我们向*所有*对这项工作做出贡献的人表示诚挚的感谢。 整个 collection 献给 [Norman "Norm" Dwight Megill 博士 (1950-2021)](https://www.legacy.com/us/obituaries/bostonglobe/name/norman-megill-obituary?id=31842140) 的记忆， 他是 Metamath 系统的创造者，也是致力于数字化和 形式化验证数学的共同梦想的国际社区的培育者。 他的思想和设计对世界各地的 形式化数学产生了深远的影响。我们非常怀念他。

标签：Metamath, 后端开发, 形式化验证, 数学, 逻辑学, 集合论