文章轉載于新智元

最近，陶哲軒迷上了形式化數學證明。

在YouTube上，他開設了賬號，上傳了4段視頻：如何用Lean形式化數學證明。

如今，他開始形式化自己的數學分析入門教材。

陶哲軒發布了新的開源項目，把教材中的各種定義、定理和習題翻譯（或轉述）為Lean語言，給學生提供另一種學習數學途徑。

他還打算將新項目逐步過渡到標準Lean庫Mathlib。

1

經典教材被電腦「吃了」

2006年，陶哲軒出版了一本本科生數學分析教科書，日后成為經典之作——「Analysis I」。

初版之后，該書多次更新。目前中文版到了第3版，而英文版已更新至第4版

這本教材從分析的源頭——數系的結構和集合論開始，然后引向分析基礎，再進入冪級數、多元微分學和傅里葉分析，最后介紹勒貝格積分。

全書幾乎完全是以具體的實直線和歐幾里得空間為背景，保留了足夠的直觀性，完美結合了嚴格性和直觀性。

當時，雖然像Coq和Agda之類的證明助手（proof assistant）已經比較成熟，但陶哲軒并沒有特別關注形式化驗證。

證明助手Agda第一版發布于1999年，而Coq第一版發布于1989年

近二十年后，隨著對形式化驗證的深入了解，陶哲軒意識到，《Analysis I》的內容非常適合用于證明助手工具。

Lean是一種更年輕的編程語言和證明助手

因此，他決定為《Analysis I》推出Lean版本的配套項目，將書中的定義、定理和練習「翻譯」成Lean代碼。

項目地址：https://github.com/teorth/analysis

這樣，讀者無需再在紙上推演，而是填寫Lean代碼中的占位符，完成證明。

目前，書中以下部分已被翻譯成Lean：

1

寫代碼，也能學數學

在形式化過程中，陶哲軒有意識地在某些地方脫離Lean的標準數學庫Mathlib，而在其他地方又依賴于它。

比如，Mathlib已經定義了標準的自然數集合?。

但他在第2章中構建了不依賴于Mathlib的自然數理論，并建立了許多關于這個版本自然數的基本性質，這些性質與Mathlib中?的對應引理類似。

然后，在第2章結尾中，他設置了一些練習，要求讀者建立這兩個版本自然數之間的同構關系。

從那以后，轉而使用Mathlib中的自然數。

整本書中，陶哲軒都采用這種模式——

隨著章節推進，越來越多地依賴Mathlib中的定義和函數，而不再直接引用前面章節中的自定義版本。

也就是說，他犧牲一部分「自包含性」，換取與Mathlib更好的兼容性。

因此，這個Lean項目也可以作為Lean和Mathlib的入門教材，同時也是實分析的學習資料。

部分代碼片段

或許以后，數學本科生也將告別筆與紙，不僅計算要用計算機，證明也要用「電腦」。

參考資料：

https://mathstodon.xyz/@tao/114603605315214772

https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/

https://www.ituring.com.cn/book/1822

https://github.com/teorth/analysis

點個愛心，再走 吧