60万行证明1+1=2：当Lean遇到暴力枚举

项目概览：616,873行到底写了什么？

我第一眼看到这个仓库名，以为小数点放错了位置。Proving 1 plus 1 = 2 in 616,873 lines of Lean。61万行证明1+1=2。我点进去，看到39个提交，核心文件叫Principia.lean，配着lakefile.toml、lake-manifest.json和lean-toolchain。这不是一个随手写的脚本，这是一个工程化项目 GH。README的第一段直接给出了数字。101,708个定理，100,714个定义，不用Mathlib，不用任何依赖 README。

同名论文也挂在仓库里，标题一字不差。作者引用了Whitehead和Russell的Principia Mathematica，指出罗素在卷II第86页的✱110.643处给出过类似的证明，还说“上面的命题偶尔有用” README。这句引语让我确认，作者是认真在做这件事，不是随手写个段子。一个证明项目引用了《数学原理》，这本身就是一种态度。

但Hacker News上的反应很冷淡。这个帖子只拿到1个point，0条评论 HN。61万行的证明，在技术社区里安静得像没发生过。我看了几遍评论区，确实没有讨论。也许大多数人看到标题就划走了，或者觉得这事太像行为艺术，不值得评论。但我不太确定，也许只是那天的HN流量太小。

量化与技术细节：手工构建的数系

所有数系都是手工构建的。自然数有三种构造方式，然后是整数、有理数、实数、复数、四元数、八元数、二进制数、模n整数（n从1到500）、两种罗马数字。1+1=2在每个数系里分别证明一次。在模2算术里，命题读作1+1=0，与普通算术的1+1=2并存 README。同一个命题在不同结构下有不同的读法，这让我觉得代数结构比证明本身更有意思。

除了直接证明，作者还在一个嵌入Lean的逻辑中，一条规则接一条规则写出推导过程，模拟最原始的证明。这是形式化的慢功夫，不依赖任何自动推理。更离谱的是0.999...+0.999...=2被证明了，但0.999...+1.999...=2被Lean拒绝，而且拒绝被形式化成一个定理，不是报错 README。这让我重新想了想0.999...这个数在形式化系统里到底意味着什么。

还有一条链式证明。99,999个引理，推出100,000−99,998=1+1 README。这就是暴力穷举的典型形态，每一步都平凡，连起来就是61万行。我不确定这种链式证明有什么数学价值，但至少它测试了Lean的编译极限。61万行跑通了，说明这个证明不是纸面文章，是机器实际检查过的。

反直觉与判断：这是数学还是行为艺术？

更让我意外的是作者主动禁用自动化。no sorry、no rfl、no simp、no decide，除propext、Quot.sound和Classical.choice外不引入任何公理 README。这意味着作者故意不走捷径，把每一步都摊开。我见过很多形式化证明依赖simp或decide来省事，这个项目反其道而行，像用手工工具加工零件，虽然慢，但每一步都看得见。

反直觉的地方在这里。同一个仓库里，1+1=2和模2下的1+1=0同时成立 README。1+1=2不是普适真理，它依赖你选了哪个代数结构。0.999...+1.999...=2被拒绝则说明，形式化系统会主动发现规格里的漏洞，然后生成一个反例定理 README。这些发现比我预想的要深刻，虽然我不确定作者是刻意为之还是偶然撞见，但能把拒绝也写成定理，确实少见。

作者自己的判断是，这个证明的意义不在数学必要性，而在对证明自动化边界做了压力测试 GH。和Mathlib那种庞大依赖不同，这个项目零依赖，60多万行换来自建数系，是一种逆向工程取向 README。HN上没人讨论，我有点不理解，但也许是标题太像段子了。如果这算行为艺术，它至少比多数行为艺术更费电。作者引的那句“上面的命题偶尔有用”，在61万行的背景下，显得有点幽默 HN。

原文：

Proving 1 plus 1 = 2 in 616,873 lines of Lean · 来源：Hacker News

作者：itfan123 值班编辑 · 发布于 2026年10月30日