作品总结
假如有一天，困扰数学家几代人的难题，被一万个人工智能代理用几天时间攻克，接下来最重要的问题会是什么？
不是“机器怎么这么聪明”，而是：我们凭什么相信它真的证明了？
AI的快速发展把我们带到了这样的场景：OpenAI宣布解决纳维－斯托克斯问题，AI负责寻找答案，Lean负责确认结果。不过，首先需要说明：这段文字中的事件、人数和耗时，目前只能作为你提供的叙述，不能仅凭它就认定为已经得到数学界确认的事实。宣布解决难题、公开完整证明、通过形式化检查，以及获得学界认可，是不同的事情。
但即使暂时放下这则消息，它提出的问题也足够震撼：当机器开始生产人类难以逐步审查的推理，我们需要怎样的信任机制？
凯文·哈特内特的《The Proof in the Code》，暂译《代码中的证明》，讲的就是这个问题。
它表面上是一部数学软件的发展史，实际上讲述的是：人类如何把“我认为这是对的”，变成一种可以公开检查、共同积累、交给机器验证的知识。
一句话概括这本书
这是一部关于Lean及其社区的故事：一个原本用来验证软件的工具，如何逐渐改变数学家证明、协作与发现的方式，并成为人工智能可靠推理的重要基础。
本书究竟在讲什么
故事可以从一堆橙子讲起。
四百多年前，开普勒提出一个看起来很朴素的问题：大小相同的球，怎样堆放最省空间？
水果摊上的金字塔式排列，似乎就是答案。但“看起来显然”与“证明一定如此”，中间隔着几百年的数学努力。
到了1998年，数学家汤姆·黑尔斯与合作者终于给出了证明。问题是，这份证明不仅有数百页数学论证，还依赖大量计算机运算。
审稿人检查多年，最终仍无法完全确认。
想象一下：你花掉人生中最宝贵的一段时间，解决了一个著名难题，但同行既不能指出你错在哪里，也不能最终告诉你，你是对的。
黑尔斯于是决定，不再只是请人检查计算机参与的证明，而是把证明本身写成计算机可以检查的形式。
这里出现了本书最重要的区别：让计算机帮助计算，不等于让计算机验证整个证明。
前者可能只是得到大量结果；后者则需要说明，这些结果为什么足以支持结论，推理链条有没有缺口。
与此同时，软件研究者莱昂纳多·德莫拉也在追求另一种确定性：能不能证明一个程序始终符合它的设计要求，而不只是通过几轮测试，看起来没有问题？
他后来创造了Lean。
但真正热情拥抱Lean的，最初不是他期待的软件工程师，而是一群数学家。他们开始给这个几乎不懂数学的系统，逐条输入定义、定理和证明，建立名为Mathlib的公共数学库。
于是，一部软件史，变成了关于知识基础设施的故事。
本书的八个关键想法
第一个想法：数学证明不仅是逻辑对象，也是社会活动。
我们常把数学想象成绝对确定的领域。但现实中，一项成果能否被接受，需要同行阅读、讨论、纠错，也受到声望、时间和专业分工的影响。
这并不意味着数学只是投票决定真理，而是说，人类接近数学真理的过程，仍然要经过人的判断。
黑尔斯的困境告诉我们：当证明的复杂程度超过现有审查能力，信任机制就必须升级。
第二个想法：形式化最先揭露的，可能不是错误，而是我们习惯忽略的歧义。
凯文·巴扎德曾把一道教了很多年的题目输入Lean：如果实数x满足某个方程，那么x是否等于1？
专业数学家默认，这是在问所有满足条件的x。但初学者可能把它理解成某个具体的x。
Lean不会替作者接受这种默认理解。
巴扎德因此发现：学生答不好，有时不只是学生不懂，也可能是老师没有把问题说清楚。
这条经验远远超出数学。制定合同、设计接口、描述产品需求时，我们也经常把“大家应该明白”误当成了“我已经准确表达”。
第三个想法：证明与程序之间存在深刻联系。
书中介绍了柯里－霍华德对应：在适当的逻辑体系中，命题可以对应类型，证明可以对应满足该类型的程序。
这让数学证明与软件验证共享了一部分技术基础。
不过，这不意味着程序只要能运行，就一定正确；它意味着，我们可以把某些正确性要求写成精确的命题，再构造可以被检查的证明。
第四个想法：真正让工具变得有用的，是工具背后的公共知识库。
Lean可以检查逻辑，却不会凭空拥有整个数学世界。
如果库里没有复数的定义，没有拓扑学的基础，没有相关定理，使用者就得先把这些东西建立起来。
Mathlib的价值，正在于让后来者不用每次都从零开始。
它像一座不断扩建的城市：最耀眼的是高楼，但决定城市能否继续生长的，是道路、管线与地基。
第五个想法：大型协作的关键，是让贡献能够独立检查。
传统数学研究很难无限扩大合作人数。你收到一个陌生人提交的引理，仍然要花时间确认它是否正确。
在形式化项目中，如果双方约定的命题、定义和依赖都准确，Lean可以检查对方提交的证明是否成立。
这降低了合作对个人声望和熟人关系的依赖。
从“液体张量实验”到陶哲轩主持的形式化项目，本书展示了一种新的组织方式：把大问题拆成小任务，让不同背景的人贡献，再用统一的检查机制把它们拼起来。
第六个想法：寻找证明与检查证明，是两种不同的能力。
人工智能可以提出猜想、尝试步骤，也可以大量生成错误的路径。Lean则检查提交的形式证明，是否遵循规定的逻辑规则。
这使两者有机会形成循环：AI尝试，Lean反馈，AI继续改进。
但需要强调，Lean并不能保证AI一定找到答案。可靠的裁判，不等于无所不能的选手。
书中AlphaProof在2024年国际数学奥林匹克题目上的表现，就显示了这种结合的潜力，也显示了它对题目表达、训练数据和领域知识的依赖。
第七个想法：形式验证提供的保证，有明确边界。
这是读这本书时尤其需要保持清醒的地方。
Lean检查的是：形式命题能否在所用的逻辑规则、定义与公理下，由提交的证明推出。
它不会自动确认，你写下的命题就是原本想问的问题。
你若把问题翻译错了，可能得到一份完全正确、却证明了另一件事的代码。
此外，内核实现、运行环境和基础假设，也构成信任链的一部分。
所以，“真理机器”是一个有吸引力的比喻，而不是超越一切条件的神谕。形式化没有消灭人的责任，而是把责任放到了更清楚的位置上。
第八个想法：维护基础设施，比展示突破更重要，也更难获得关注。
本书最有力量的冲突，不是人类与机器的对抗，而是创造软件的人与使用软件的人之间的拉扯。
数学家兴奋地提交新项目，德莫拉却要处理兼容性、性能、错误报告和长期维护。
对使用者来说，是“多加一个功能”；对维护者来说，可能是此后多年都要承担的责任。
后来，社区通过拆分Mathlib、维护社区版本、建立专门组织等方式，逐渐调整这种关系。
这里的教训很现实：不能一边赞美公共工具，一边把维持它运转的劳动视为理所当然。
我最喜欢的三条启发
第一条：先让一个有价值的工作流程成立，再谈改变整个世界。
Lean不是因为一句宏大的愿景，就说服了数学家。它经历了基础定义的积累、复杂对象的形式化，以及对前沿研究成果的验证。
每一次具体成功，都让下一次尝试更可信。
第二条：好的工具不只替你检查答案，也会反过来改善你的理解。
彼得·舒尔策请求验证自己的证明，是因为他担心论证太复杂，自己的声望又可能让别人过于容易相信。
形式化不仅消除了部分疑虑，还迫使他澄清原来没有充分展开的步骤，重新看见证明真正依赖的结构。
把思想讲到能够被严格检查，往往就是重新理解思想的过程。
第三条：开放协作需要的不只是热情，还需要结构。
任务如何拆分，定义如何统一，谁负责审核，贡献者如何获得认可，代码由谁维护——这些都不是行政性的附属问题，而是合作能否持续的核心条件。
书中的成功，并非“把人聚在一起，奇迹自然发生”，而是社区逐渐学会为热情建立可以承重的框架。
如何评价这本书
这本书最出色的地方，是没有把技术革命写成一个天才独自完成壮举的传奇。
你会看到，德莫拉既执着又疲惫；巴扎德热情洋溢，也会惹人不快；马里奥·卡内罗坚持开放贡献，却与核心开发者发生冲突；约翰·科梅林愿意投入新方向，也担忧自己的学术前途。
技术的改变，伴随着职业风险、组织冲突与关系修复。
它也让我们看见，什么工作更容易获得荣誉：提出新定理的人通常站在聚光灯下，整理旧知识、构建公共库、维护工具的人，却未必得到同等认可。
而没有后者，很多新突破根本无从发生。
不过，这是一部面向大众的叙事作品，不宜把所有技术解释都当成严格教材。特别是对构造性数学、自动定理证明器的能力，以及形式验证所提供的“绝对保证”，书中有些表述需要更细致的限定。
读它最好的方式，是一边被故事吸引，一边保留一个问题：这里验证的究竟是什么，保证又来自哪里？
我喜欢的几句话
书中引用罗素的话，可以译为：
“凡事都有某种程度的模糊，直到你试着把它说精确，才会意识到。”
这几乎就是全书的钥匙。
黑尔斯的一句话则更直接：
“计算机证明应该由计算机检查。”
它不是要否定人，而是在要求：审查方法必须跟得上知识生产的方法。
德莫拉反复表达的信念是：
“人生最悲哀的事，是没有一个目的。”
这解释了他为什么在意的不只是Lean是否优雅，而是有没有人真正用它完成重要的工作。
科梅林回应舒尔策时说：
“我非常同意数学是一种人类活动。但我也认为，使用计算机是一种人类活动。”
这句话最温和，也最深刻。使用工具，并不必然意味着放弃人的主体性。
谁应该读这本书
如果你关心人工智能，却厌倦了“机器马上取代所有人”的宣传，这本书值得读。它把讨论拉回具体机制：知识从哪里来，错误如何发现，结果如何检查。
如果你是数学、计算机或理工科学生，它会让你看到，发现、证明、验证与维护，是不同却相互依赖的工作。
如果你是教师、产品经理或软件工程师，它也会提醒你：许多失败不是因为答案不够聪明，而是因为问题没有定义清楚。
如果你只是好奇，人类知识将如何在机器时代继续保持可信，那么你就是这本书的理想读者。
可以搭配阅读的几本书
想进一步理解数学证明为什么既是逻辑问题，也是社会信任问题，可以读唐纳德·麦肯齐的《Mechanizing Proof》。它为这本书中的历史讨论提供了重要背景。
想理解智能与形式系统之间的关系，可以读侯世达的《哥德尔、艾舍尔、巴赫》。它更抽象，却能把问题带到更深的层次。
想对AI的能力与局限建立平衡判断，可以读梅拉妮·米切尔的《Artificial Intelligence: A Guide for Thinking Humans》。
想把“怎样信任机器”延伸到医疗、司法和日常决策，可以读汉娜·弗莱的《Hello World》。
最后，回到开头
即使未来真的出现“一万名AI代理攻克世纪难题”的新闻，也不要只问：机器用了多久，人类输了没有。
更重要的问题是：题目有没有被准确表达？证明能否公开检查？验证依赖哪些假设？其他人能否复核和继续使用这个成果？
《代码中的证明》真正令人振奋的，不是它许诺机器永远不会出错，而是它展示了一条路线：
允许创造性的系统大胆尝试，同时让重要结论接受严格检查。
人负责提出值得追问的问题，机器帮助探索庞大的可能性空间，形式系统把推理变成可以检查的公共成果。
这本书最终改变的，或许不是我们对“谁更聪明”的判断，而是我们对知识应当如何建立的期待。
当有人说“相信我，我证明了”，未来我们也许可以回答：
不必只相信你。让我们一起检查。
不是“机器怎么这么聪明”，而是：我们凭什么相信它真的证明了？
AI的快速发展把我们带到了这样的场景：OpenAI宣布解决纳维－斯托克斯问题，AI负责寻找答案，Lean负责确认结果。不过，首先需要说明：这段文字中的事件、人数和耗时，目前只能作为你提供的叙述，不能仅凭它就认定为已经得到数学界确认的事实。宣布解决难题、公开完整证明、通过形式化检查，以及获得学界认可，是不同的事情。
但即使暂时放下这则消息，它提出的问题也足够震撼：当机器开始生产人类难以逐步审查的推理，我们需要怎样的信任机制？
凯文·哈特内特的《The Proof in the Code》，暂译《代码中的证明》，讲的就是这个问题。
它表面上是一部数学软件的发展史，实际上讲述的是：人类如何把“我认为这是对的”，变成一种可以公开检查、共同积累、交给机器验证的知识。
一句话概括这本书
这是一部关于Lean及其社区的故事：一个原本用来验证软件的工具，如何逐渐改变数学家证明、协作与发现的方式，并成为人工智能可靠推理的重要基础。
本书究竟在讲什么
故事可以从一堆橙子讲起。
四百多年前，开普勒提出一个看起来很朴素的问题：大小相同的球，怎样堆放最省空间？
水果摊上的金字塔式排列，似乎就是答案。但“看起来显然”与“证明一定如此”，中间隔着几百年的数学努力。
到了1998年，数学家汤姆·黑尔斯与合作者终于给出了证明。问题是，这份证明不仅有数百页数学论证，还依赖大量计算机运算。
审稿人检查多年，最终仍无法完全确认。
想象一下：你花掉人生中最宝贵的一段时间，解决了一个著名难题，但同行既不能指出你错在哪里，也不能最终告诉你，你是对的。
黑尔斯于是决定，不再只是请人检查计算机参与的证明，而是把证明本身写成计算机可以检查的形式。
这里出现了本书最重要的区别：让计算机帮助计算，不等于让计算机验证整个证明。
前者可能只是得到大量结果；后者则需要说明，这些结果为什么足以支持结论，推理链条有没有缺口。
与此同时，软件研究者莱昂纳多·德莫拉也在追求另一种确定性：能不能证明一个程序始终符合它的设计要求，而不只是通过几轮测试，看起来没有问题？
他后来创造了Lean。
但真正热情拥抱Lean的，最初不是他期待的软件工程师，而是一群数学家。他们开始给这个几乎不懂数学的系统，逐条输入定义、定理和证明，建立名为Mathlib的公共数学库。
于是，一部软件史，变成了关于知识基础设施的故事。
本书的八个关键想法
第一个想法：数学证明不仅是逻辑对象，也是社会活动。
我们常把数学想象成绝对确定的领域。但现实中，一项成果能否被接受，需要同行阅读、讨论、纠错，也受到声望、时间和专业分工的影响。
这并不意味着数学只是投票决定真理，而是说，人类接近数学真理的过程，仍然要经过人的判断。
黑尔斯的困境告诉我们：当证明的复杂程度超过现有审查能力，信任机制就必须升级。
第二个想法：形式化最先揭露的，可能不是错误，而是我们习惯忽略的歧义。
凯文·巴扎德曾把一道教了很多年的题目输入Lean：如果实数x满足某个方程，那么x是否等于1？
专业数学家默认，这是在问所有满足条件的x。但初学者可能把它理解成某个具体的x。
Lean不会替作者接受这种默认理解。
巴扎德因此发现：学生答不好，有时不只是学生不懂，也可能是老师没有把问题说清楚。
这条经验远远超出数学。制定合同、设计接口、描述产品需求时，我们也经常把“大家应该明白”误当成了“我已经准确表达”。
第三个想法：证明与程序之间存在深刻联系。
书中介绍了柯里－霍华德对应：在适当的逻辑体系中，命题可以对应类型，证明可以对应满足该类型的程序。
这让数学证明与软件验证共享了一部分技术基础。
不过，这不意味着程序只要能运行，就一定正确；它意味着，我们可以把某些正确性要求写成精确的命题，再构造可以被检查的证明。
第四个想法：真正让工具变得有用的，是工具背后的公共知识库。
Lean可以检查逻辑，却不会凭空拥有整个数学世界。
如果库里没有复数的定义，没有拓扑学的基础，没有相关定理，使用者就得先把这些东西建立起来。
Mathlib的价值，正在于让后来者不用每次都从零开始。
它像一座不断扩建的城市：最耀眼的是高楼，但决定城市能否继续生长的，是道路、管线与地基。
第五个想法：大型协作的关键，是让贡献能够独立检查。
传统数学研究很难无限扩大合作人数。你收到一个陌生人提交的引理，仍然要花时间确认它是否正确。
在形式化项目中，如果双方约定的命题、定义和依赖都准确，Lean可以检查对方提交的证明是否成立。
这降低了合作对个人声望和熟人关系的依赖。
从“液体张量实验”到陶哲轩主持的形式化项目，本书展示了一种新的组织方式：把大问题拆成小任务，让不同背景的人贡献，再用统一的检查机制把它们拼起来。
第六个想法：寻找证明与检查证明，是两种不同的能力。
人工智能可以提出猜想、尝试步骤，也可以大量生成错误的路径。Lean则检查提交的形式证明，是否遵循规定的逻辑规则。
这使两者有机会形成循环：AI尝试，Lean反馈，AI继续改进。
但需要强调，Lean并不能保证AI一定找到答案。可靠的裁判，不等于无所不能的选手。
书中AlphaProof在2024年国际数学奥林匹克题目上的表现，就显示了这种结合的潜力，也显示了它对题目表达、训练数据和领域知识的依赖。
第七个想法：形式验证提供的保证，有明确边界。
这是读这本书时尤其需要保持清醒的地方。
Lean检查的是：形式命题能否在所用的逻辑规则、定义与公理下，由提交的证明推出。
它不会自动确认，你写下的命题就是原本想问的问题。
你若把问题翻译错了，可能得到一份完全正确、却证明了另一件事的代码。
此外，内核实现、运行环境和基础假设，也构成信任链的一部分。
所以，“真理机器”是一个有吸引力的比喻，而不是超越一切条件的神谕。形式化没有消灭人的责任，而是把责任放到了更清楚的位置上。
第八个想法：维护基础设施，比展示突破更重要，也更难获得关注。
本书最有力量的冲突，不是人类与机器的对抗，而是创造软件的人与使用软件的人之间的拉扯。
数学家兴奋地提交新项目，德莫拉却要处理兼容性、性能、错误报告和长期维护。
对使用者来说，是“多加一个功能”；对维护者来说，可能是此后多年都要承担的责任。
后来，社区通过拆分Mathlib、维护社区版本、建立专门组织等方式，逐渐调整这种关系。
这里的教训很现实：不能一边赞美公共工具，一边把维持它运转的劳动视为理所当然。
我最喜欢的三条启发
第一条：先让一个有价值的工作流程成立，再谈改变整个世界。
Lean不是因为一句宏大的愿景，就说服了数学家。它经历了基础定义的积累、复杂对象的形式化，以及对前沿研究成果的验证。
每一次具体成功，都让下一次尝试更可信。
第二条：好的工具不只替你检查答案，也会反过来改善你的理解。
彼得·舒尔策请求验证自己的证明，是因为他担心论证太复杂，自己的声望又可能让别人过于容易相信。
形式化不仅消除了部分疑虑，还迫使他澄清原来没有充分展开的步骤，重新看见证明真正依赖的结构。
把思想讲到能够被严格检查，往往就是重新理解思想的过程。
第三条：开放协作需要的不只是热情，还需要结构。
任务如何拆分，定义如何统一，谁负责审核，贡献者如何获得认可，代码由谁维护——这些都不是行政性的附属问题，而是合作能否持续的核心条件。
书中的成功，并非“把人聚在一起，奇迹自然发生”，而是社区逐渐学会为热情建立可以承重的框架。
如何评价这本书
这本书最出色的地方，是没有把技术革命写成一个天才独自完成壮举的传奇。
你会看到，德莫拉既执着又疲惫；巴扎德热情洋溢，也会惹人不快；马里奥·卡内罗坚持开放贡献，却与核心开发者发生冲突；约翰·科梅林愿意投入新方向，也担忧自己的学术前途。
技术的改变，伴随着职业风险、组织冲突与关系修复。
它也让我们看见，什么工作更容易获得荣誉：提出新定理的人通常站在聚光灯下，整理旧知识、构建公共库、维护工具的人，却未必得到同等认可。
而没有后者，很多新突破根本无从发生。
不过，这是一部面向大众的叙事作品，不宜把所有技术解释都当成严格教材。特别是对构造性数学、自动定理证明器的能力，以及形式验证所提供的“绝对保证”，书中有些表述需要更细致的限定。
读它最好的方式，是一边被故事吸引，一边保留一个问题：这里验证的究竟是什么，保证又来自哪里？
我喜欢的几句话
书中引用罗素的话，可以译为：
“凡事都有某种程度的模糊，直到你试着把它说精确，才会意识到。”
这几乎就是全书的钥匙。
黑尔斯的一句话则更直接：
“计算机证明应该由计算机检查。”
它不是要否定人，而是在要求：审查方法必须跟得上知识生产的方法。
德莫拉反复表达的信念是：
“人生最悲哀的事，是没有一个目的。”
这解释了他为什么在意的不只是Lean是否优雅，而是有没有人真正用它完成重要的工作。
科梅林回应舒尔策时说：
“我非常同意数学是一种人类活动。但我也认为，使用计算机是一种人类活动。”
这句话最温和，也最深刻。使用工具，并不必然意味着放弃人的主体性。
谁应该读这本书
如果你关心人工智能，却厌倦了“机器马上取代所有人”的宣传，这本书值得读。它把讨论拉回具体机制：知识从哪里来，错误如何发现，结果如何检查。
如果你是数学、计算机或理工科学生，它会让你看到，发现、证明、验证与维护，是不同却相互依赖的工作。
如果你是教师、产品经理或软件工程师，它也会提醒你：许多失败不是因为答案不够聪明，而是因为问题没有定义清楚。
如果你只是好奇，人类知识将如何在机器时代继续保持可信，那么你就是这本书的理想读者。
可以搭配阅读的几本书
想进一步理解数学证明为什么既是逻辑问题，也是社会信任问题，可以读唐纳德·麦肯齐的《Mechanizing Proof》。它为这本书中的历史讨论提供了重要背景。
想理解智能与形式系统之间的关系，可以读侯世达的《哥德尔、艾舍尔、巴赫》。它更抽象，却能把问题带到更深的层次。
想对AI的能力与局限建立平衡判断，可以读梅拉妮·米切尔的《Artificial Intelligence: A Guide for Thinking Humans》。
想把“怎样信任机器”延伸到医疗、司法和日常决策，可以读汉娜·弗莱的《Hello World》。
最后，回到开头
即使未来真的出现“一万名AI代理攻克世纪难题”的新闻，也不要只问：机器用了多久，人类输了没有。
更重要的问题是：题目有没有被准确表达？证明能否公开检查？验证依赖哪些假设？其他人能否复核和继续使用这个成果？
《代码中的证明》真正令人振奋的，不是它许诺机器永远不会出错，而是它展示了一条路线：
允许创造性的系统大胆尝试，同时让重要结论接受严格检查。
人负责提出值得追问的问题，机器帮助探索庞大的可能性空间，形式系统把推理变成可以检查的公共成果。
这本书最终改变的，或许不是我们对“谁更聪明”的判断，而是我们对知识应当如何建立的期待。
当有人说“相信我，我证明了”，未来我们也许可以回答：
不必只相信你。让我们一起检查。
客服咨询
400 093 7005
周一至周日：09:00AM-21:00PM
微信扫码关注
小程序扫码注册
0条评论