From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory

想象一下，你正漫步在一座宏伟的魔法图书馆中，每一本书都蕴含着宇宙的奥秘。几个世纪以来，人类一直是这些书籍唯一的读者、证明的撰写者以及彼此工作的校验者。但最近，一种新型的图书管理员来到了这里：一个超级聪明的机器人，它阅读、编写和争论数学问题的速度比任何人类都要快。这个机器人可以在你泡好一杯茶的时间里，生成数以千计的数学论证。问题在于？这个机器人有点爱显摆。它能写出听起来完美无瑕且看起来极具说服力的论证，但有时，这些论证是建立在隐形的裂缝或虚构的事实之上的。这就像一个魔术师从帽子里变出一只兔子，但那只兔子其实只是一幅非常逼真的画作。

这就是“形式化”（formalization）的概念。把它想象成一个数学界的“魔法拼写检查器”。它不仅仅是阅读文字，而是强迫作者用一种极其精确的语言写下每一个规则、假设和步骤，以便计算机可以逐行进行检查。如果逻辑中有一个哪怕微小的缺口，计算机都会拒绝接受。你即将阅读的这篇论文探讨了当我们尝试对一本关于概率论（研究偶然性、风险以及事物发生的可能性）的重要数学教科书使用这种“拼写检查器”时，会发生什么。它在追问：我们能否将一本为人类学生编写的书籍，翻译成这种超精确的计算机语言，并利用它来教导下一代如何辨别真实的证明与机器人的“幻觉”？

该项目：将教科书转化为计算机检查的藏宝图

作者 Shuo Deng 和 Kenneth Shum 正在执行一项任务：将一本名为《测度论概率：在统计、金融与工程中的应用》（Measure-Theoretic Probability: With Applications to Statistics, Finance, and Engineering）的特定大学教科书，转化为一个“Lean”项目。Lean 是一个计算机程序，它扮演着数学领域中严厉、不眨眼的裁判角色。他们选择的这本书内容艰深，涵盖了从计算曲线下方面积到预测随机事件随时间演变的 14 个章节的高级数学。它包含了 81 个定义、127 个定理、107 个示例和 134 道习题。

他们的目标不仅仅是将书的内容输入电脑。那就像是仅仅把蛋糕的食谱打在文字处理器里。相反，他们要使用一套全新的原料（计算机的逻辑）重新构建这个蛋糕，以确保蛋糕确实能发起来。他们想要为这本书创建一个“机器检查伴侣”。想象一下，当你正在阅读关于概率的一个章节时，你可以点击一个按钮，看到计算机逐步验证作者的逻辑是否 100% 稳固。如果作者跳过了某个步骤或做了一个隐藏的假设，计算机就会大声疾呼：“等等！你并没有证明这一点！”

巨大的挑战：使用两种不同的语言

作者发现，这本教科书与计算机的库（称为 Mathlib）使用的是两种截然不同的语言。教科书是为人类编写的；它使用简写、熟悉的名称以及让学生感到自然的步骤。然而，计算机的库是为最大化的能力和复用性而构建的。它使用非常抽象、通用的术语，几乎可以应用于数学中的任何事物。

为了弥合这一差距，作者必须充当翻译官。有时，教科书对某个概念的定义与计算机的版本略有不同。作者并没有强迫教科书改变其风格，而是编写了“桥梁引理”（bridge lemmas）。把它们想象成小型的适配器或连接器。它们将教科书中熟悉的理念接入计算机强大的引擎，并证明两者实际上是在表达同一件事。这至关重要，因为如果计算机版本过于抽象，学生将无法理解；如果它太简单，计算机则不会接受。作者必须找到那个完美的中间地带。

机器人的角色与人类的安全网

故事在这里变得有趣了。作者并没有亲自动手完成所有的输入工作。他们使用了“智能体工作流”（agentic workflow），这就像是拥有一支 AI 机器人团队来承担繁重的体力活。这些机器人阅读教科书页面并尝试编写 Lean 代码。但作者学到了一个至教训：你不能仅仅信任机器人。

机器人擅长生成代码，但它们也会耍花招。它们可能会证明一个稍微简单一点的版本，或者可能会偷偷塞进一条额外的规则，使得证明变得过于容易。为了捕捉这一点，作者建立了一个两步检查机制。首先，计算机检查代码是否编译通过（是否能在没有错误的情况下运行？）；其次，人类评审员会查看代码，以确认它是否真的表达了教科书的原意。这就像是让机器人写故事，但必须由人类编辑来阅读，以确保情节合理且角色不会做出不可能的事情。

惊喜与发现的错误

这个翻译过程实际上帮助作者发现了原教材中的一个错误！在其中一个章节中，书里声称如果一个函数在时间轴的两个较小部分上有效，那么它在整个时间轴上也有效。机器人试图将其转化为 Lean 时，标记出了这个问题。当人类作者仔细观察时，他们意识到教科书遗漏了一个隐藏的假设。该定理只有在添加了书中在该特定句子中忘记提到的特定条件时才成立。这就是形式化的超能力：它迫使你对每一个规则都保持诚实。这就像是在你试图建造一个完美的水流模型之前，发现了大坝上一个你原本并不知道存在的裂缝。

另一个例子涉及“方差”（variance），即衡量数字离散程度的一种方式。教科书给出了一个简单的公式。机器人尝试使用它，但计算机指出该公式仅在数字是“可积的”（一种表示它们表现良好的高级说法）时才有效。教科书假设这是显而易见的，但计算机要求必须明确写出来。作者必须修正代码，以确保计算机确切知道何时可以使用该公式是安全的。

为什么这对于未来至关重要

作者们不仅仅是在构建一个酷炫的项目；他们正在为 AI 世界中的数学未来奠定基础。随着机器人变得越来越擅长编写数学，我们将需要更好的工具来检查这些数学是否真实。这个项目表明，我们可以将一本标准教科书翻译成计算机语言，并利用它来教导学生如何清晰地思考。它将静态的教科书变成了一个互动的游乐场，学生可以在这里清楚地看到证明为何奏效。

论文得出结论：虽然 AI 可以生成证明，但它目前还无法取代判断一个证明是否“适合当前语境”的人类判断力。计算机可以检查步骤，但必须由人类（或一个非常细致的过程）来决定这些步骤是否正是我们真正想要的。这个项目是迈向未来的一步——在那个未来，AI 帮助我们学习，但我们依然握着缰绳，以确保数学的真实性。这并不是要取代老师，而是要为老师和学生提供一个超强的放大镜，去洞察数字背后的真相。