内容来源：https://www.sciencenews.org/article/the-proof-in-the-code-ai-math-book

内容总结：

AI数学证明新突破：从“代码验证器”到“数学真理机器”

2024年，国际数学奥林匹克竞赛迎来了一位特殊“选手”——谷歌DeepMind研发的AI程序AlphaProof。尽管作为非官方参与者，它最终以42分中取得28分的成绩达到了银牌分数线，引发广泛关注。这一成就标志着人工智能在自动化数学推理领域迈出了关键一步。

AlphaProof的成功，离不开一个名为“Lean”的证明辅助程序。该程序最初由时任微软研究院工程师的莱奥·德穆拉于2013年开发，用于检查软件代码。然而，其精确的逻辑验证能力很快吸引了数学界的目光。在《代码中的证明》一书中，记者凯文·哈特尼特详细记录了Lean如何从一个代码工具演变为数学研究的重要助手。

Lean的核心价值在于能够将数学证明转化为可验证的代码逻辑。正如哈特尼特所比喻：“证明中的逻辑漏洞就像软件代码中的错误。”通过Lean，数学家可以将长达数百页、需要数月审核的证明转化为计算机可逐行检验的形式，从而确保证明的严谨性，并加速新数学事实的确立。

然而，推广之路并非一帆风顺。早期，Lean的数学概念库极为有限，而丰富概念库又需要大量数学家主动参与编码，形成了“先有鸡还是先有蛋”的困境。伦敦帝国理工学院教授凯文·巴扎德等先驱者付出了巨大努力：例如，将算术几何的前沿理论“完美胚空间”转化为Lean代码，就耗费了数月时间，写下数千行代码。

这些努力逐渐结出硕果。到2025年，已有数万学术与技术界用户基于Lean开展项目。它不仅是数学家的验证工具，更成为训练AlphaProof等AI数学模型所需的“高级数学知识库”。对于德穆拉而言，Lean的初衷是构建确保软件代码绝对正确的“真理机器”；而对数学家来说，它正使数学证明变得更加严密、有序和精确。

《代码中的证明》一书通过众多人物与轶事，生动展现了数学家与计算机科学家如何携手突破边界，共同推动数学研究进入人机协作的新篇章。尽管技术细节可能对普通读者构成挑战，但书中描绘的这场静默革命，正深刻改变着人类探索数学真理的方式。

中文翻译：

代码中的证明
凯文·哈特尼特
Quanta出版社，30美元

2024年，国际数学奥林匹克竞赛迎来了一位特殊的“参赛者”。谷歌DeepMind将其新训练的人工智能程序AlphaProof投入当年竞赛试题的解答中——尽管只是非正式参与。在这场为期两日、汇聚全球顶尖数学学子的赛事中，参赛者需破解六道高难度数学题。AlphaProof以42分满分中取得28分的成绩，不仅登上新闻头条，更达到了银奖级别的分数线。

AlphaProof是一个数学定理求解系统，专为证明数学命题而设计。就在四年前，训练人工智能系统实现数学推理自动化仍被视为重大挑战。但谷歌DeepMind等团队希望，他们的努力能让人工智能掌握更广泛的推理能力，未来或将应用于解决现实世界问题，并借助逻辑使AI工具摆脱“幻觉”——即虚构信息的困扰。

这类程序的成功，很大程度上归功于证明辅助程序Lean。2013年，时任微软研究院软件工程师的莱奥·德穆拉推出了Lean，初衷是将其作为检查软件代码的工具。但如今，数学家与AI研究者已成为Lean最热烈的拥护者。在凯文·哈特尼特的新书《代码中的证明》中，这位记者追溯了这段演进历程。

哈特尼特记录了德穆拉如何坚持开发一款短期内毫无商业价值的软件，以及一小群数学家如何以执着决心说服整个领域接纳这一程序。全书贯穿了来自世界各地的众多人物，他们在Lean中看到了验证数学真理的新途径，并为提升Lean的易用性贡献了或大或小的力量。这些故事共同编织出一段鼓舞人心的协作篇章。

在开篇章节中，哈特尼特穿插解释了数学与编程的相似性，阐明了Lean为何能如此自然地融入数学研究。“二者皆以精确的语法书写，呈现为一系列逻辑步骤，环环相扣，”他写道，“证明中的逻辑漏洞如同软件代码中的错误。”代码逻辑正确，程序方能运行；证明书写无误，新的数学定理方能诞生。

Lean问世后不久，卡内基梅隆大学的杰里米·阿维加德便开始尝试用它撰写数学证明。Lean与其他证明辅助程序（亦称交互式定理证明器）能够验证人类撰写的新数学证明——这些证明有时长达数百页，人工审核需耗时数月。这类程序虽无法独立提出新证明，但通过协助确保证明无误，它们能帮助数学家更快地确立新的数学事实，供后续证明使用。然而，早期的证明辅助软件仍显笨拙，要求数学家以全然不同的方式书写数学。

为使用证明辅助工具，数学家必须将问题从自然语言转化为代码，并为基本数学概念编写定义库与定理库。例如，伦敦帝国理工学院数学教授凯文·巴扎德在编写习题集以指导学生使用Lean时，很快遇到了意想不到的障碍。“Lean要求他证明2不等于1，”哈特尼特写道，“这个命题在人类日常对话中显然成立，无需任何解释。”但Lean却要求在使用前先证明这个不等式。

很长一段时间里，Lean的数学库内容匮乏，难以满足数学家需求。而若没有更多数学家使用该程序，便无法编码更多数学知识。哈特尼特分享了部分数学家推广Lean的艰辛历程。例如，2018年，巴扎德等人着手将“完美胚空间”理论转化为Lean代码。这项算术几何学的前沿成果耗费了他们数月时间，编写了数万行代码。努力终见成效：到2025年，“学术界与技术界已有数万用户基于Lean开展日益宏大的项目”，哈特尼特写道。这其中包括AI研究者——他们在Lean中发现了训练AlphaProof等数学求解AI模型所需的大量高等数学库。

德穆拉与数学家们共同渴望构建一台“真理机器”——“一种能百分百确保逻辑链条正确的计算机程序”。对德穆拉而言，他追求的“真理”是确知如Microsoft Word等计算机程序的代码正确无误；而对数学家来说，真理机器能使数学证明的发现过程更严谨、有序且精确。

在梳理这段历史时，《代码中的证明》时常在时间线间跳跃，引入人物与轶事却未总是明晰其意义。这或许会让读者感到困惑，但对于数学爱好者而言，本书为Lean的故事及其在数学史新篇章中的地位，增添了引人入胜的质感。

您可通过Bookshop.org购买《代码中的证明》。Science News是Bookshop.org的合作伙伴，通过本文链接购买将为其带来佣金收入。

英文来源：

The Proof in the Code
Kevin Hartnett
Quanta Books, $30
In 2024, the International Mathematical Olympiad had an unusual entrant. Google Deepmind had set AlphaProof, a newly trained AI program on that year’s competition questions, although as an unofficial participant. In the contest, top math students from across the world solve six advanced math problems over two days. AlphaProof made headlines and the silver-medal level cutoff by scoring 28 points out of 42.
AlphaProof is a mathematical theorem solver, a system for proving mathematical statements. Just four years prior, training AI systems to automate mathematical reasoning had been a grand challenge. But Google Deepmind and other groups hoped that their efforts would equip AI systems with broader reasoning skills that could someday be applied to real world problems, using logic to potentially free AI tools of hallucinations, instances of made-up information.
Many of these programs owe their success to the proof assistant program Lean. Leo de Moura launched Lean as a tool for checking software code in 2013 when he was a software engineer at Microsoft Research. But today, mathematicians and AI researchers are Lean’s biggest cheerleaders. In his new book The Proof in the Code, journalist Kevin Hartnett traces that evolution.
Hartnett chronicles de Moura’s persistence in developing software that had no immediate commercial benefit and the dogged determination of a small group of mathematicians who persuaded their field to embrace the program. Throughout the book, Hartnett introduces a host of characters from around the world who saw in Lean a new way to assess mathematical truths and played roles big and small in making Lean more user-friendly. Taken together, this makes for an inspiring story of collaboration.
In the initial chapters, Hartnett sprinkles in explanations about the similarities between math and coding that demonstrate how Lean’s use could so naturally be transplanted to research math. “Both are written in exact syntax as a series of logical steps, each one leading to the next,” Hartnett writes. “A gap in the logic of a proof is like a bug in software code.” A program runs when the code has the correct logic. A new math theorem is the result of a correctly written proof.
Almost immediately after Lean’s launch, Jeremy Avigad of Carnegie Mellon University began setting it up to write math proofs. Lean and other proof assistant programs, also known as interactive theorem provers, can verify new human-written mathematical proofs, which sometimes span hundreds of pages and can take months to review. The programs can’t come up with new proofs, but by helping to ensure that proofs are error-free, they can allow mathematicians to establish new mathematical facts faster for use in newer proofs. Still, proof assistants were clunky pieces of software that required writing math in an entirely different way.
To work with proof assistants, mathematicians had to translate problems from plain language into code and create libraries of coded definitions and theorems of basic math concepts. For instance, when Kevin Buzzard, a math professor at Imperial College London, was writing up problem sets to teach his undergraduate students to work with Lean, he quickly ran into an unexpected hurdle. “Lean asked him to prove that 2 is not equal to 1,” Harnett writes. “It’s a statement so clearly true that human beings, in normal conversation, wouldn’t waste a moment justifying it.” But Lean required him to prove inequality before using it.
For a long time, there just wasn’t enough math in Lean’s libraries for it to be useful to mathematicians. And more math couldn’t be coded without more mathematicians using the program. Hartnett shares what it took for some mathematicians to popularize Lean. For instance, in 2018, Buzzard and others set about translating perfectoid spaces into Lean. Coding this sparkly new innovation in arithmetic geometry took them months of work and many thousands of lines of code. And these efforts worked. By 2025, “tens of thousands of users across academia and technology were launching increasingly ambitious projects on top of Lean,” Hartnett writes. This included AI researchers, who had found in Lean in an extensive library of advanced math required to train math-solving AI models such as AlphaProof.
Both de Moura and the mathematicians wanted to build a truth machine, “a computer program that can provide a complete, 100 percent guarantee that a chain of logic is correct,” Hartnett writes. While for de Moura, the truth he was after was to know for sure that the code for computer programs, like Microsoft Word, was correct and bug-free, for mathematicians, a truth machine could make mathematical proof discoveries more rigorous, organized and exact.
In tracing this history, The Proof in the Code jumps between timelines, introducing characters and anecdotes without always clearly stating their importance. This can be confusing for readers, but for the mathematically curious, the book adds an engrossing texture to the story of Lean and its place in a new, recent chapter in the story of math.
Buy The Proof in the Code from Bookshop.org. Science News is a Bookshop.org affiliate and will earn a commission on purchases made from links in this article.