#Lean 4

摺紙其實比圓規直尺更強：研究團隊用 Lean 4 把紙張摺疊變成可機器驗證的數學系統

Columbia University 團隊在最新 arXiv 預印本中，利用 Lean 4 與 Mathlib 將七種 Huzita 摺紙操作正式化，並證明角三等分、倍立方、Haga 定理與三次方程相關構造。研究還打造 Crease Pattern Inspector，能把 2D 摺痕轉成 3D 模型，再輸出成 Lean 表示。更特別的是，Claude Code 與 Gemini 也實際參與部分證明與工具開發，但最終結果仍由形式化證明系統進行檢查。