资源介绍
这是一本关于数学如何被彻底改变的书，讲的是一群数学家用计算机程序来验证数学真理的故事。作者凯文·哈特尼特是知名科学媒体Quanta Magazine的资深撰稿人，长期跟踪报道数学与计算机科学前沿进展，这本书由Quanta Books与Farrar, Straus and Giroux联合出版。故事的主角是一款名为Lean的程序，它最初由Leo de Moura在2013年开发，原本的目标是为软件代码提供百分百正确的保证，确保像Windows或Word这样的程序不含安全漏洞。然而事态的发展出人意料，软件工程师们对这个工具反应冷淡，反倒是一群职业数学家从中看到了巨大的潜力，以近乎狂热的热情开始使用它。原因其实并不复杂，研究型数学的核心是证明，而证明本质上就是一系列严格的逻辑链条，和计算机程序有着异曲同工之妙。当一个证明的逻辑每一步都无懈可击时，最终就会得到一个新的定理。Lean恰好能充当那个确保每一步都正确的检查者，于是数学家们梦想中的工具突然变成了现实。书里讲述了Jeremy Avigad如何将Lean视为实现数十年抱负的契机，Kevin Buzzard如何在职业中期的怀疑中转向这个工具，Patrick Massot如何借助它检验学生的计算，年轻的Johan Commelin如何在热情与担忧之间投入其中，Mario Carneiro则梦想搭建一座数字化的众包数学图书馆。这些人来自不同的背景，各有各的动机，但他们共同的目标是重塑数学家的工作方式、协作方式，甚至改变数学家判定真理本身的标准。这项工作在实践中意味着要把教科书里的数学一条定义、一个定理、一个证明地翻译成计算机可以理解的形式，填满一座未来的数学图书馆。为了让整个数学共同体接受这种全新的工作方法，他们经历了在线论坛上没日没夜的讨论，举办了一场在疫情期间靠自筹资金运作的学术会议，甚至发起了一场持续一年之久的运动，只为吸引一位被誉为半个世纪以来最具天赋的数学家加入。故事在推进的过程中，世界也在变化，人工智能的爆发为这个项目注入了新的紧迫感和可能性。Google DeepMind和Meta等公司的工程师开始意识到，Lean所提供的那种绝对可靠的逻辑保证，正是训练下一代推理系统最理想的基石——有了数学定理级别的严谨，AI就不再那么容易产生幻觉式的错误。数学作为人类推理最纯粹的表达形式，正在与飞速发展的机器智能建立一种全新的关系，而Lean站在这个交汇点上。这本书最迷人之处在于它写的不只是一项技术变革，更是一群理想主义者如何试图说服一个古老而保守的学科接受新的工作方式。如果你对数学的本质、计算机辅助证明、形式化方法，或者人工智能与数学之间的交叉地带感兴趣，这本书会让你读得停不下来。哈特尼特的笔触兼具故事性和知识深度，既能让普通读者理解Lean在做什么，也能让专业读者感受到这场运动背后激动人心的人际张力。它不是一本干巴巴的科普读物，而更像一部记录科学革命前夜的纪实作品，让你看到当一种新的思维方式试图嵌入一个延续了几千年的传统时，会碰撞出怎样的火花。