機(jī)器之心報(bào)道

編輯：陳陳、杜偉

不得不感慨，陶哲軒真閑不住啊！

昨天，他還在驚嘆于谷歌 DeepMind AlphaEvolve 對(duì)解決人類數(shù)學(xué)問題（比如和差集問題）起到的加速作用。更早的時(shí)候，他還開通了油管賬號(hào)，當(dāng)起了視頻博主。

今天，陶哲軒又宣布為自己的實(shí)分析本科教材《Analysis I》創(chuàng)建了一個(gè)「Lean」配套項(xiàng)目，將教材中的各種定義、定理和練習(xí)轉(zhuǎn)換成 Lean 版本，為學(xué)生提供了另一種學(xué)習(xí)方式。Lean 既是一個(gè)交互式定理證明器，也是一種編寫形式化證明的語言，近些年來在數(shù)學(xué)家群體中越來越受到歡迎。

同時(shí)，陶哲軒希望該項(xiàng)目可以逐步過渡到標(biāo)準(zhǔn)的 Lean 庫 Mathlib。Mathlib 既是 Lean 定理證明器的官方開源數(shù)學(xué)庫，也是目前世界上規(guī)模最大、最活躍的形式化數(shù)學(xué)項(xiàng)目之一。

陶哲軒表示，大約 20 年前，他寫了一本名為《Analysis I》的實(shí)分析教材，旨在補(bǔ)充市面上眾多優(yōu)秀的實(shí)分析教材。該書側(cè)重于基礎(chǔ)問題，例如自然數(shù)、整數(shù)、有理數(shù)和實(shí)數(shù)的構(gòu)造，并提供足夠的集合論和邏輯知識(shí)，使學(xué)生能夠進(jìn)行高度嚴(yán)謹(jǐn)?shù)淖C明。

雖然在本書撰寫時(shí)，Coq 或 Agda 等一些證明助手已經(jīng)相當(dāng)成熟，但形式化驗(yàn)證當(dāng)時(shí)還不在陶哲軒的考慮范圍內(nèi)。隨著現(xiàn)在具備了一些這方面的經(jīng)驗(yàn)，他意識(shí)到這本書的內(nèi)容實(shí)際上與這些證明助手非常兼容；特別地，之前用來構(gòu)建標(biāo)準(zhǔn)數(shù)系等的「樸素類型理論」，與 Lean 的依賴類型理論（其中 Lean 對(duì)商類型的支持非常出色）非常契合。

因此，陶哲軒決定創(chuàng)建《Analysis I》的 Lean 配套項(xiàng)目，將書中的許多定義、定理和練習(xí)轉(zhuǎn)換成 Lean 版本。特別地，它提供一種完成書中練習(xí)的替代方法，只需在 Lean 代碼中填寫對(duì)應(yīng)的「待完成」（sorries）部分即可。

不過，陶哲軒不打算提供本書練習(xí)的「官方」答案。相反，他歡迎所有人自由創(chuàng)建這個(gè)項(xiàng)目的副本，并完成答題。

GitHub 地址：https://github.com/teorth/analysis

項(xiàng)目介紹

《Analysis I》共有 11 個(gè)章節(jié)，目前已被形式化的章節(jié)如下：

書籍地址：https://tiu-edu.uz/media/books/2024/05/28/1664976801.pdf

看來，陶哲軒要完成對(duì)全書的形式化，還有很多工作要做。

讀者不用擔(dān)心原書籍和形式化后的內(nèi)容對(duì)應(yīng)不上，所有章節(jié)都遵循原始書籍，根據(jù)章節(jié)序號(hào)就能找到。

需要特別說明的是，本次形式化未對(duì)運(yùn)行效率進(jìn)行優(yōu)化，因?yàn)槟承┣闆r下轉(zhuǎn)譯可能不符合 Lean 的慣用規(guī)范。或許，在完成全書的工作后，陶哲軒會(huì)探索這方面的內(nèi)容。

另外，原書中設(shè)置為讀者練習(xí)的章節(jié)內(nèi)容，在本次轉(zhuǎn)譯中以 sorry 占位符形式呈現(xiàn)。陶哲軒表示，他本人暫無計(jì)劃提供習(xí)題解答。

陶哲軒還強(qiáng)調(diào)，盡管項(xiàng)目中的定義、定理及證明編排嚴(yán)格遵循了教材內(nèi)容，但他盡量避免直接引用教材原文，而是在適當(dāng)處標(biāo)注了原書參考文獻(xiàn)。因此，該形式化工程應(yīng)視為原教材的注解式輔助資料，而非替代品。

Lean 版本內(nèi)容截圖

值得強(qiáng)調(diào)的是，本形式化工程在設(shè)計(jì)上刻意采用了與標(biāo)準(zhǔn)數(shù)學(xué)庫 Mathlib 若即若離的策略 —— 部分內(nèi)容保持獨(dú)立，部分則依托 Mathlib 實(shí)現(xiàn)。

例如，盡管 Mathlib 已具備標(biāo)準(zhǔn)自然數(shù)體系，但在第 2 章中，陶哲軒首先以手工方式構(gòu)建了另一種自然數(shù)結(jié)構(gòu) Chapter2.Nat（若在 Chapter2 命名空間下可簡稱為 Nat），并推導(dǎo)出與該結(jié)構(gòu)相關(guān)的基礎(chǔ)結(jié)論。隨后在結(jié)語部分，建立了這種替代自然數(shù)與 Mathlib 自然數(shù)之間的同構(gòu)關(guān)系（更準(zhǔn)確地說，是將其設(shè)為習(xí)題）。自此之后，第 2 章的自然數(shù)體系將被棄用，轉(zhuǎn)而采用 Mathlib 的自然數(shù)定義。

這種先獨(dú)立構(gòu)建再逐步遷移的模式將貫穿全書 —— 隨著章節(jié)推進(jìn)，讀者將越來越依賴 Mathlib 的定義與函數(shù)，而非直接引用前期章節(jié)的對(duì)應(yīng)內(nèi)容。

因此，本配套資料既可視為實(shí)分析的輔助教材，也能作為 Lean 與 Mathlib 的入門指南。

現(xiàn)在，這個(gè) Lean 版數(shù)學(xué)副本已經(jīng)上線，歡迎大家前去挑戰(zhàn)。無論你是數(shù)學(xué)系學(xué)生、Lean 初學(xué)者，還是對(duì)形式化驗(yàn)證感興趣的研究員，這都是一個(gè)親自動(dòng)手、順便提升數(shù)學(xué)內(nèi)功的好機(jī)會(huì)。而陶哲軒本人，也在等待大家的反饋。

網(wǎng)友評(píng)論

有熟悉陶哲軒該教材以及 Lean 的用戶表示非常興奮，希望可以移到自己的代碼庫中。ta 表示自己一直對(duì)數(shù)學(xué)感興趣，而《Analysis I》是第一本真正展示如何以編程式大腦所期望的嚴(yán)謹(jǐn)方式構(gòu)建數(shù)學(xué)的教材。后來也接觸了 Lean，同樣對(duì)其效果非常滿意。

不過，Mathlib 的數(shù)學(xué)概念學(xué)習(xí)起來有點(diǎn)復(fù)雜，所以很高興有人架起了從該教材到該工具的橋梁。

還有人分享了使用 Lean 來教數(shù)學(xué)的體會(huì)，最令人興奮的地方是即時(shí)反饋。如果學(xué)生的證明錯(cuò)了，則根本無法通過編譯。以前，學(xué)生只可以從助教、老師或其他知識(shí)淵博的專家那里獲得反饋，而現(xiàn)在能夠通過 Lean 編譯器快速得到反饋。

ta 希望未來有更多選擇，讓 Lean 編譯器提供更具指導(dǎo)性的反饋，就像 Rust 編譯器提供代碼修改建議一樣。不過這可能需要專門的 LLM 才能實(shí)現(xiàn)。

博客地址：https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/