為什麼不乾脆用 Lean 就好？

背景

本文探討了數學形式化證明工具 Lean 的崛起及其引發的社群現象。作者回顧了從 1960 年代 AUTOMATH 開始的發展史，指出在 Lean 成為主流之前，已有如 Isabelle、HOL Light 與 ACL2 等系統完成了多項深奧的數學證明。作者質疑當前對 Lean 的過度推崇可能導致學術上的封閉與從眾，並強調不應忽視其他邏輯體系的價值。

社群觀點

在 Hacker News 的討論中，社群成員對於 Lean 的流行展現了多樣的解讀。部分評論者認同作者對「群體思維」的警惕，認為即便最終選擇隨大流，深入了解其他替代方案的技術地景仍極具價值，這能避免陷入盲目的技術崇拜。這種觀點強調，在面對「理所當然」的技術選擇時，保持批判性思考是專業素養的體現。

針對 Lean 為何能脫穎而出，討論者指出其成功的關鍵在於實用主義的路線。與過去長期受直覺主義邏輯束縛的系統（如 Coq/Rocq）不同，Lean 的核心社群透過 Mathlib 庫大膽擁抱了古典邏輯，包含排中律與反證法等強大工具。這種做法雖然在哲學層面上可能被認為缺乏對「推測性運動」的包容力，但卻極大地降低了數學家進入形式化領域的門檻，解決了過往系統在處理一般數學問題時常遇到的障礙。

此外，社群也從程式開發的角度提供了不同視角。對於非數學專業的工程師而言，Lean 不僅是一個證明助理，更是一門具備強大函數式編程特性的語言。有開發者分享了將 Lean 應用於日常程式邏輯驗證的經驗，例如證明基礎資料結構的正確性。這顯示出 Lean 的影響力已超越純數學界，開始滲透進軟體工程領域。然而，討論中也出現了關於術語精確性的爭論，提醒讀者在探討邏輯體系時，應嚴格區分「直覺主義邏輯」與一般直覺的差異，這反映了該領域高度嚴謹的學術特質。

延伸閱讀

• Functional Programming in Lean: 一本從函數式編程視角介紹 Lean 的書籍，適合工程師背景的讀者。
• Lean-zip 範例: 展示如何使用 Lean 撰寫並驗證一般程式碼（如 Zip 函數）的實作。