數學歸納法，在 Lean 裡不是公設｜How Lean Works 第 9 集

▶ How Lean Works 全系列播放清單：https://www.youtube.com/playlist?list=PLCKW73PRfmKo 數學課本上，歸納法是 Peano 公理的一條。可是在 Lean 裡，你只要宣告「自然數有 zero 和 succ 兩種造法」，Lean 就自動送你一個遞迴器，而它的型別，就是數學歸納法這條規則。這一集用它還上一集欠的帳：零加 n 等於 n，整個證明一條公設都沒用到。 這集你會看到： ・先看 Lean 的遞迴函數「加倍」：為什麼原則上它對每個自然數都算得出答案 ・遞迴器：用列出造法的方式宣告型別，Lean 就自動生出它；同一台機器，吐數字就是遞迴計算，吐證明就是歸納法 ・親手造出「零加 n 等於 n」：kernel 算掉一層，歸納假設補上剩下的；公設帳單是空的 ・之前一直在用的 match，到了 kernel 那一層去哪了：或、假、等號、存在的「怎麼用」，背後全是遞迴器 建議先看第 8 集；不需要會 Lean，畫面上的寫法每一步都會念出來。 之前把等號對上了型別，留下一筆欠帳：零加 n 等於 n。這一集用歸納法還上，而歸納法在 Lean 裡是宣告自然數時送的。下一集：kernel 的規則到齊了，把它整個寫在一頁紙上，拿筆親手跑一次。結尾的小故事：Peano 用拉丁文寫下自然數的公理，以及 Landau 那本序言寫著「請忘記你在學校學過的一切」的書。 章節 00:00 欠帳：零加 n 等於 n 00:37 歸納法的分數線 01:15 課本上它是公理 02:02 Lean 的遞迴：加倍 03:03 遞迴器 04:04 遞迴器怎麼算 05:00 吐證明的遞迴器，就是歸納法 07:16 造出零加 n 等於 n 10:18 一條公設都沒用 10:58 列出造法，就有遞迴器；match 去哪了 13:16 故事：Peano 與 Landau 📖 系列配套電子書《從零開始學 Lean》：想自己動手寫 Lean 的話可以看 Kobo：https://www.kobo.com/tw/zh/ebook/lean-10 Pubu：https://www.pubu.com.tw/ebook/698946 Readmoo：https://readmoo.com/book/210503759000101 上一集：第 8 集 Lean 裡的相等，其實有兩種 https://youtu.be/cwT46dnM-Bg 照片來源（片中有縮放、加框或裁切） ・Latino sine flexione：GreenNeutron（CC BY-SA 4.0 https://creativecommons.org/licenses/by-sa/4.0）｜https://commons.wikimedia.org/wiki/File:Logo_vectoris%C3%A9_du_latin_sans_flexions.png ・Python：™/®Python Software Foundation（GPL http://www.gnu.org/licenses/gpl.html）｜https://commons.wikimedia.org/wiki/File:Python_logo_and_wordmark.svg #Lean #數學 #定理證明 #HowLeanWorks