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

一張紙，可能比圓規與直尺更會解數學題。

Columbia University 研究團隊在 2026 年 9 月上傳至 arXiv 的預印本 《A Lean Paper About Paper: A Formal Framework for Origami》 中，嘗試做了一件相當少見的事情：把摺紙從直覺式幾何活動，轉換成可以由電腦逐步檢查的形式化數學系統。

研究使用 Lean 4 與其數學函式庫 Mathlib，重新描述摺紙數學中著名的七種 Huzita 操作，並建立超過 100 個 theorem 與 lemma。更重要的是，作者不是單純把 Huzita 規則當成「公理直接接受」，而是試圖在座標幾何模型下證明這些摺法何時存在、何時唯一，以及哪些特殊情況可能不存在或有多個解。

這使摺紙變成一個很有意思的形式化驗證實驗場：一邊是抽象幾何，一邊是真的可以拿一張紙做出來的物理操作。

摺紙為什麼會比圓規與直尺更強？

傳統幾何中，圓規與無刻度直尺能完成大量構造，但它們有著明確的代數限制。

只使用圓規與直尺時，可構造數字所對應的代數擴張，基本上只能經由反覆開平方取得。因此，如果一個問題最終需要解某些不可約三次方程，就可能超出傳統尺規作圖能力。

摺紙卻不完全受這個限制。

原因在於 Huzita 系統中的某些摺法，不只是畫出一條線或找一個中點，而是要求一條摺痕同時滿足多個反射與落點條件。

其中最關鍵的是通常被稱為 Huzita 6 或 Beloch fold 的操作：給定兩個點與兩條線，尋找一條摺痕，使兩個點分別反射到指定的兩條線上。

這個幾何條件會導出三次方程。

而一旦幾何操作具備解 cubic constraint 的能力，摺紙就能完成一些著名的古典問題，例如 任意角三等分與倍立方問題。

角三等分：古希臘尺規作圖做不到，摺紙可以

任意角三等分是數學史上的經典問題。

19 世紀已證明，一般情況下不能只靠無刻度直尺與圓規把任意角精確分成三等份。

但使用摺紙，多重幾何條件可以在一次摺疊中同時成立，因此能繞過傳統尺規構造的代數限制。

研究團隊將一種源自 Abe 摺法的角三等分構造寫入 Lean，並證明構造得到的幾何關係確實符合三等分條件。

這裡的重點不只是「電腦算出結果」。

Lean 的工作方式更接近：

每一個定義、每一個幾何條件、每一步推論，都必須符合形式系統中的型別與邏輯規則。

如果某一步推論不成立，proof 就無法通過。

因此，這與一般數值模擬有很大差別。模擬可以告訴你「看起來很接近」，形式化證明要求的是「在給定假設下，這個命題可以被邏輯導出」。

一張紙甚至可以構造 ∛2

另一個著名例子是 Delian Problem，也就是倍立方問題。

問題看似簡單：如果一個立方體體積為 1，要如何構造另一個體積剛好為 2 的立方體？

新立方體的邊長必須是：

∛2

但 ∛2 無法透過有限次傳統尺規作圖構造。

論文則以摺紙構造搭配 Lean 證明，展示相關摺法能產生對應 ∛2 的幾何比例。

這也凸顯了摺紙數學真正有趣之處：紙張不是單純把直線換成摺痕，而是增加了反射、同時對齊多個目標等額外幾何操作。

這些額外自由度，直接改變了可解問題的代數範圍。

從摺紙進一步走到 Cardano 三次方程

作者接著定義了一類 Origami-constructible numbers，也就是摺紙可構造數。

他們在 Lean 中將這些數字放進複數域框架，並研究加法、乘法、反元素、平方根與立方根等操作。

研究還形式化了與 Cardano's formula 有關的結果，證明在其設定下，具有摺紙可構造係數的 monic cubic polynomial 可以找到屬於該可構造集合的根。

這正是摺紙與圓規直尺能力差異的代數核心之一。

不過作者也很謹慎地指出，目前某些 closure property 仍直接被納入 Origami 定義，而不是全部從最底層的實際摺紙幾何操作推導出來。將這些代數性質完整連回幾何 construction，是未來工作的方向之一。

所以這篇研究並不是宣稱「所有摺紙數學已經完全形式化」，而比較像是在建立一個可以繼續往下蓋的骨架。

Haga 定理：不用尺，也能摺出精確的 1/3

研究另一個很漂亮的案例是 Haga's Theorem。

假設有一張正方形紙，把其中一個角摺到對邊的中點，經由摺痕與紙張邊緣產生的交點，可以得到精確的三等分位置。

在論文處理的基本案例中，研究團隊正式證明其中一個交點位於邊長的 1/3。

這種結果很適合作為形式化數學與真實物理世界之間的橋梁。

你甚至可以真的拿一張紙照著做，而 Lean 則負責回答另一個問題：

為什麼它必然是 1/3，而不是肉眼看起來差不多是 1/3？

Crease Pattern Inspector：從 2D 摺痕一路送進 Lean

論文最有工程味的部分之一，是研究團隊另外打造的 Crease Pattern Inspector。

這是一套互動式工具，讓使用者先建立 2D crease pattern，再查看對應的 3D 摺紙模型。

其 3D 部分使用以 Rust 實作的 bar-and-hinge model，把紙張視為由面、摺線與鉸鏈組成的機械結構。

整個概念流程大致可以想成：

2D 摺痕設計 → Huzita 幾何限制 → 3D bar-and-hinge model → 建立 fold sequence → 轉換成 Lean representation → 進一步進行 proof

Inspector 一開始只允許使用正方形紙張的四個角與四條邊。

當使用者完成合法的 Huzita 摺法後，新摺痕與既有邊線產生的交點才會被解鎖成新的可用 reference point。

這個設計避免使用者直接輸入任意座標，然後宣稱某個點是「摺紙可構造」的。

換句話說，介面本身就在嘗試限制使用者只能沿著合法 construction history 往前走。

但數學上存在的摺痕，不代表那張紙真的能成功摺起來

這也是論文相當重要的一個限制。

如果某條直線滿足反射條件，只代表某個幾何 construction 在數學上存在。

真實紙張還有更多問題：

不同紙層的上下順序是否一致？

摺疊時紙張會不會互相穿透？

多條摺痕同時作用時，模型是否仍然可以保持幾何與拓撲一致？

有限大小的紙張是否真的包含需要使用的所有點與線？

因此作者把問題拆成兩個層次：

Construction validity：某條 crease 是否符合 Huzita 幾何條件。

Physical/configuration validity：有限紙張實際進行狀態轉換時，是否維持合理的面對應、layer ordering 與無衝突結構。

論文目前主要建立的是前者，以及一部分連結後者的基礎設施，並不等於已經完成完整的 rigid origami physics simulator。

這個差異很重要。

否則很容易把「形式上能找到摺痕」誤解成「任何真實紙張都一定能無碰撞地摺成那個形狀」。

AI 也參與了這篇論文，而且作者直接寫在 disclosure 裡

這篇還有另一個很符合 2026 年研究環境的細節。

作者在 AI Statement 中明確表示，他們使用 Claude Code 協助形式化與證明角三等分、Cardano formula 的部分內容，也使用 Gemini 尋找 Haga theorem 所需的 tactic 與 proof method。

Claude Code 同時大量參與 Crease Pattern Inspector 的 backend 與 frontend 開發，也協助把 Inspector 產生的 Haga fold 與 Lean proof 連接起來。

但作者同時指出，Inspector 的構想、基本架構、最終 validation，以及實際建立的模型仍由人工完成；Haga proof 的基本結構也由作者自行設計。

這讓這篇研究變得格外有意思。

它不是簡單的「AI 自己證明數學」。

比較接近：

人類定義問題與形式框架 → AI 協助搜尋 tactic、寫程式與部分 proof → Lean kernel 檢查最後產生的形式證明

對 LLM 而言，這是一種非常重要的使用模式。

一般自然語言回答可能會產生 hallucination，但送進 Lean 的 theorem proof 最後只有兩種結果：

通過 type checking，或不通過。

這不代表 AI 產生的所有數學內容自動正確，也不代表形式化 specification 本身不會定義錯問題，但至少它多了一層比純文字回答更嚴格的機器檢查。

為什麼摺紙會成為形式化驗證的好實驗場？

乍看之下，用 Lean 研究摺紙可能很像某種數學家的高級玩具。

但作者選擇 origami，其實有一個很合理的原因。

形式化驗證最大的長期挑戰之一，是如何把抽象 proof 與真實世界連起來。

軟體程式可以完全存在於離散邏輯世界裡，但機器人、自駕車、機械系統與物理結構最後都必須面對連續空間、感測誤差、碰撞與實體限制。

摺紙剛好站在兩者中間。

它有高度精確的數學模型，也能以真正的紙張重現；同時一旦進入多層摺疊、self-intersection 與 rigid foldability，又會立刻碰到計算幾何與物理模型問題。

所以這篇真正有意思的地方，未必只是證明「紙可以三等分角」。

更值得觀察的是這條技術路線：

把使用者操作產生的幾何模型，逐步轉換成可以由 proof assistant 理解與驗證的形式表示。

今天對象是一張紙，未來同類方法可能延伸到機械結構、機器人 motion planning、CAD constraint，甚至某些 safety-critical physical systems。

當然，那仍是比這篇論文遠得多的延伸方向，不能把摺紙 formalization 直接等同於自動駕駛安全驗證。

但它示範了一個非常直觀的小型實驗：如何讓數學模型、互動工具與機器可驗證 proof 開始碰到同一個世界。

目前仍是一篇預印本

需要注意的是，這篇目前是 arXiv 上的 v1 預印本，上傳日期為 2026 年 9 月 14 日。

PDF 中仍可看到 conference acronym、ISBN 與 DOI 的 placeholder，因此不應把它描述成已經正式發表於特定 ACM conference 的 peer-reviewed 論文。

此外，作者自己也把多項工作列為未來方向，包括更複雜摺疊的 topology、多條摺痕交互作用、不同摺疊順序、non-flat folding 與 modular origami。

因此，目前最準確的定位是：

一套把 origami geometry、Lean formalization 與互動式摺痕工具串起來的研究原型與形式化框架。

它距離「完整驗證任何現實摺紙模型」還有很長一段路，但光是把角三等分、倍立方、Haga theorem、Cardano cubic 與 2D/3D crease pipeline 放進同一套研究裡，就已經足夠奇特，也足夠值得關注。

Tech English 專有名詞

Formal Verification｜形式化驗證：使用數學邏輯與形式系統證明某個程式、演算法或模型符合指定條件，而不是只靠測試案例判斷是否正常。

Proof Assistant｜證明輔助器：協助人類撰寫並機器檢查數學證明的軟體。Lean 4 就屬於這類系統。

Huzita–Justin Axioms｜Huzita–Justin 摺紙操作系統：描述單次摺紙中點、線與反射關係的七種基本幾何操作，常用於研究數學摺紙的可構造性。

Origami-Constructible Number｜摺紙可構造數：能透過特定摺紙幾何操作構造出的數字集合，其能力比傳統尺規可構造數更廣，包含與部分三次方程相關的數。

Bar-and-Hinge Model｜桿件與鉸鏈模型：將面視為近似剛性結構、摺痕視為鉸鏈，用來模擬薄片或摺紙結構變形的計算模型。

Cubic Constraint｜三次方程限制條件：其代數關係最高涉及三次項的約束。某些摺紙操作會自然產生這類 constraint，使摺紙能處理傳統尺規作圖無法解決的部分問題。