用 Lean 學數學：把證明當程式寫#

本書不是「Lean 使用手冊」，也不是「證明論教科書」，而是一本 用 Lean 4 親手做證明來學數學 的書。

傳統的數學入門書請你「讀懂」證明；本書要求你把每一個證明 寫成 Lean 程式，讓編譯器判斷對錯。這帶來三個革命性的學習效果：

立即回饋：寫錯了，Lean 當場指出哪一步跳太快 —— 那正是你觀念模糊的地方
精確表達：你必須把「顯然」翻譯成實際的邏輯步驟，才能真正理解定義
積木式成長：Lean 的 Mathlib 像一座樂高圖書館，學會使用它，你就能證明大學所有科目的定理

書中每章都對應一門標準大學數學課程：邏輯、集合、數論、代數、分析、拓樸、機率。讀完本書，你不只學會 Lean，更 用一種前所未有的嚴謹方式 重修了這些課。

本書特色#

做中學：每節都有完整的 Lean 4 程式碼，可直接複製到電腦上執行
對照表：每個數學概念同時給出「教科書寫法」與「Lean 寫法」的對照
習題分級：★★☆☆☆（照抄修改）→ ★★★★☆（獨立構思）
與 Mathlib 共舞：不重造輪子，從第一頁就教你看懂 Mathlib 的 API 文件
章章有專案：每章結尾有一個小型「形式化專案」，例如完整證明 \(\sqrt{2}\) 是無理數

目錄#

閱讀方式#

按順序讀：本書是螺旋式的，第 \(n\) 章的證明技巧會在第 \(n+1\) 章被假設已熟悉
打開電腦：每個例子都建議你在 Lean 中實際輸入、故意改錯、觀察錯誤訊息
習題是重點：Lean 的學習 80% 來自寫證明，20% 來自閱讀
與 Mathlib 交朋友：遇到不熟的 lemma，用 exact?、apply? 搜尋即可

需要的背景知識#

高中數學（但不假設你學過證明）
有一點任何語言的程式經驗更好，但不是必須
每章開頭會先介紹數學概念，再介紹 Lean 寫法 —— 數學零基礎也能讀

與另一本書的關係#

本系列另有《Lean 與 AI 數學證明》，講述 Lean 的 歷史、型別論理論與 AI 攻克數學難題 的故事；本書則是 動手做證明學數學 的實作教材。兩者可獨立閱讀，也可搭配食用。