IXThinker·2025-06-02 18:10

陶哲軒以Lean形式化經典教材 GitHub開源

陶哲軒近來醉心形式化數學證明，不僅在YouTube上載教學影片，更發布開源項目，把自己編寫的數學分析經典教材翻譯成Lean語言，從零構建一個數學宇宙。

影片示範

陶哲軒在YouTube開設賬號，上載四段如何用Lean形式化數學證明的影片；其中第三支尤其矚目：他借助GitHub Copilot，挑戰了數學分析中微積分的基礎內容——ε-δ極限。