文章轉(zhuǎn)載于新智元

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

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

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

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

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

1

經(jīng)典教材被電腦「吃了」

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

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

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

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

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

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

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

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

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

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

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

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

1

寫代碼，也能學數(shù)學

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

比如，Mathlib已經(jīng)定義了標準的自然數(shù)集合?。

但他在第2章中構(gòu)建了不依賴于Mathlib的自然數(shù)理論，并建立了許多關(guān)于這個版本自然數(shù)的基本性質(zhì)，這些性質(zhì)與Mathlib中?的對應(yīng)引理類似。

然后，在第2章結(jié)尾中，他設(shè)置了一些練習，要求讀者建立這兩個版本自然數(shù)之間的同構(gòu)關(guān)系。

從那以后，轉(zhuǎn)而使用Mathlib中的自然數(shù)。

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

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

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

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

部分代碼片段

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

參考資料：

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

點個愛心，再走 吧