背景

這篇文章記錄了一位擁有數學背景的軟體工程師學習 Lean 定理證明器的初步心得。作者認為形式化數學不僅能減少錯誤，更能將數學寫作從繁瑣的機械驗證中解放，讓人類專注於傳達直覺與創意，並預言未來數學家將與人工智慧協作，由 AI 處理形式化細節，人類則負責建構高層次的證明策略。

社群觀點

針對作者從軟體工程師視角切入 Lean 的嘗試，社群展開了關於工具選擇與理論細節的深入討論。有評論者指出，雖然 Lean 在形式化數學領域蔚為風潮，但若讀者的核心目標是軟體驗證而非純數學，目前 Isabelle 可能是更成熟的選擇。Isabelle 作為經典的定理證明器，其不具備依賴類型的特性對於初學者而言門檻較低，且在軟體工程應用上有更深厚的積累。不過，Lean 社群正積極擴張，未來這種側重數學的傾向可能會有所改變。

在技術細節上，留言者針對作者提到的概念混淆給予了具體澄清。關於「證明」與「定義性相等」的區別，有觀點解釋這取決於函數的定義方式，例如在處理列表合併時，若定義是基於遞迴，則某些屬性可以直接透過展開定義來驗證，而另一些則必須依賴歸納法證明。此外，針對 Prop 與 Decidable 的區別，社群成員指出 Prop 是純粹的數學命題，而 Decidable 則要求必須能寫出一個程式來判定該命題的真偽。這涉及到計算性與非計算性的本質差異，在同倫類型論的視角下，命題被視為「子單元」，其證明過程往往具有證明無關性，即我們只關心命題是否為真，而不關心具體的證明路徑。

最後，討論也觸及了 Curry-Howard 同構在構造主義與經典數學之間的張力。有留言提醒，在處理形式化證明時，必須意識到經典集合論與構造邏輯在處理排中律等問題上的差異。雖然作者對 AI 協作充滿期待，但社群中也有人好奇目前大型語言模型在 Coq 或 Lean 等嚴謹語言上的實際表現，這顯示出儘管願景宏大，但在實踐層面仍有許多待探索的技術邊界。

延伸閱讀

在討論中，社群成員推薦了幾項學習資源：

• Concrete Semantics：Isabelle 的經典教科書，目前已有 Lean 版本的重寫計畫 Logical Verification 2025。
• Homotopy Type Theory：深入理解命題與類型關係的理論基礎。
• Diaconescu-Goodman-Myhill 定理：探討排中律與構造邏輯關係的重要理論參考。