移動沙發問題的 119 頁證明

假設一份 PR 附著 AI 的回報：「測試已通過。」準備合併前，你還要確認的是：這次跑的測試對應哪個版本、涵蓋了需求裡的哪幾條，以及哪些部分仍沒有被檢查到。回報本身說明了狀態，不等於驗收所需要的依據。

2024 年 11 月，數學家 Jineon Baek 把一份 119 頁的證明投上 arXiv，宣稱解開了移動沙發問題。後續的 Lean 形式化專案，提供了另一層檢查依據。

這條檢查路徑，正好可以用來談一件和 PR 審查一樣具體的事：驗收的依據，要能追溯到被檢查的版本、標準與結果。證據能支持哪些主張，同樣需要交代清楚。

119 頁手算證明交給 Lean 檢查：AI 耗時 4 天形式化，抓出 11 處缺口與 33 處誤植

移動沙發問題問的是：一條寬度為一單位、轉了直角彎的 L 形走廊，能通過這個轉角的連通平面圖形，最大面積是多少。這個問題在 1966 年由數學家 Leo Moser 正式提出，之前已有一些非正式的討論。1968 年，Hammersley 給出一個區間：下界約 2.2074，上界約 2.8284，說明答案落在這個範圍內，但沒有鎖定確切數字。Joseph Gerver 在 1992 年構造出一個由 18 段曲線拼成的圖形，面積約 2.2195，並猜想它就是答案；到了 2018 年，Kallus 與 Romik 用電腦輔助的方法把上界壓到 2.37，但這與 Gerver 構造的面積約 2.2195 仍有距離。構造出一個能通過的圖形，與證明所有能通過的圖形都不會更大，是完全不同的兩件事。Baek 的論文要證明的，正是後者：Gerver 的構造確實達到了最大面積。

這份證明本身完全沒有電腦輔助，數值計算只用科學計算機完成。提出證明與後續形式化，應分開看待兩者的貢獻。Baek 在 2024 年取得密西根大學數學博士，指導教授是 Michael Zieve，目前在延世大學擔任博士後研究員。Gerver 受訪時說：「I'm 75 years old now. I feel lucky to have lived long enough to see someone finally solve the problem.」Zieve 則說：「The fact that Jin was able to do this without computers was impressive.」「Jin is by far the best student I've ever seen with computers.」這些評語分別來自構造提出者與指導教授，記錄的是同儕的直觀感受。但審查一項工作時，同行讚譽和真正支持證明正確性的檢查依據，必須分開看。

論文貼出來之後，陸續有人把它改寫成形式化證明，交給證明輔助工具 Lean 檢查。其中一個公開專案 MovingSofa 的 README 自述：在 Dean Cureton 指揮下，OpenAI Codex 與 Claude Code 這兩個 AI coding agent 花了約四天完成形式化。四天的速度很驚人，但這是在既有論證骨架下進行形式化翻譯，不能直接拿來和原作者構思證明的數年心血比較。README 也記錄，形式化過程發現了論文裡 11 處錯誤或缺口，以及 33 處誤植；這些問題後來都被修正，而且沒有動搖最終的主定理。

這份錯誤與修正紀錄，讓形式化的貢獻有了具體依據。原作者提出了突破性的論證，而後續的形式化工作則把推導邊界補得更加扎實。

機器只能檢查形式推導：定義是否對準原問題、未驗證的假設與留空仍須由人把關

要判斷這份檢查結果究竟能支持什麼，應先確認形式命題是否對準原問題，再看推導依據與檢查涵蓋的範圍。

審閱這份形式化成果時，要先把採用的主張切開：是要確認某個構造可行、確認它的面積，還是確認它達到最大面積？接著請成果提供者指出，每項主張分別對應哪個形式敘述、哪份檢查紀錄，以及依賴哪些前提。對於公理與依賴，也應要求明列採用範圍；如果要進一步主張整個基礎系統一致，就得另外拿出依據。至於形式敘述有沒有對準原問題，可以把「走廊轉角」「連通圖形」「最大面積」逐一列出，看形式語言如何表達。把這些邊界攤開，才能看清採用這項結果時需要承擔哪些判斷。

依 MovingSofa 的 README，形式化過程確實留下了錯誤、缺口與誤植的修正紀錄。若想據此了解形式化補上了什麼，最好的做法是把修正項目對回原論證：原文原本的主張是什麼、修正補了哪個邏輯缺口、修正後的依據放在哪裡。某一處是推導省略過多，還是推導方向有誤，應以相應紀錄為準。審核時宜逐項核對，既不能把錯誤總數一概而論，更不能只憑一句「已驗證」的摘要就略過修正細節。

審閱形式證明時，定義對齊只是第一步；接下來還得檢視證明本體到底驗證了多少、又留下了哪些未解的空缺。

依 Cureton 專案 README，Challenge.lean 這份題目檔留了三個預期的 sorry 佔位符（即尚未證明的空位）。審閱時，必須將題目檔的佔位符與支撐主定理的證明依賴分開核對。專案表示，最優性命題——也就是 Gerver 的構造達到最大面積——已完成形式化；但數值部分只核對到面積至少是 11/5，並未核對 2.2195 這個更精確的數字。主定理與面積近似值的檢查範圍，必須分開看。

採用檢查結果前，我們仍得退一步審視：形式命題是否忠實對應原問題、公理假設是否合理。機器的檢查不能取代人類對問題結構的理解與同儕審查。

工程 PR 的驗收準則：測試通過不等於能合併，檢查依據必須說清版本、需求與未涵蓋範圍

回到開頭那份 PR。移動沙發問題給軟體工程最大的啟發在於：驗收的依據，必須能明確追溯到被檢查的版本、標準與結果。

落實到工程現場，這個要求可以拆成三件事。第一，檢查結果要對應到明確的版本：跑的是哪一次 commit、哪一組環境設定，和回報「測試已通過」的是不是同一次。第二，檢查標準要對準需求本身：必須明確指出測試涵蓋了規格裡的哪幾條，以及哪些邊界情境尚未被檢查。第三，誰在解讀結果要說清楚：reviewer 負責確認證據是否充分，CI 紀錄負責交代執行了哪些檢查；至於需求定義本身有沒有盲點，仍得由人工另外審查。

在工程實務中，最危險的誤區是把「測試通過」直接延伸成「所有情境都沒問題」。驗收時，必須交代測試涵蓋了哪些輸入、環境與需求。至於要投入多深的驗證，關鍵在於衡量判斷出錯時的代價，以及撰寫規格與維護檢查所需的成本，同時保留需求審查、測試與人工判斷各自的位置。

舉個具體場景：如果這次 PR 影響的是計費邏輯或資料庫遷移，團隊要先問，算錯一筆帳或搞壞一批資料，代價能不能承受？如果答案是否定的，就值得多花時間把驗收範圍寫清楚，並考慮引入更嚴格的檢查。相反地，若只是調整內部工具的提示文字，只要確認文字不影響操作判斷，基礎測試就已足夠。驗收的投入程度，應該跟著出錯時的代價走。如果專案考慮引入形式化驗證，同樣應先說清楚希望支持哪些主張、誰負責建模與維護，避免投入的成本遠超過它所防範的風險。

這也是為什麼「多找一個人 review」或「CI 亮綠燈」不能單獨當成答案。如果驗收標準本身對需求的理解就有偏差，換再多人看、跑再多次流程，通過的結果依然支持不了採用的決定。標準要先對準需求，檢查才有意義。

下一次點擊 merge 之前，你可以做的最小動作很簡單：找出一份對應當前版本的檢查紀錄，明確說出它支持了需求裡的哪一條，以及還有哪些邊界未被涵蓋。這份紀錄不必像移動沙發問題那樣繁複，但必須回答同一個核心問題：這次通過，究竟對準了哪一個標準。

延伸閱讀

• AI 寫的測試全過，為什麼功能還是錯的？驗證閉環完整懶人包（2026）：同一個問題在日常 PR 裡的版本——測試本身憑什麼可信，以及讓測試可信的幾層做法。
• Plan、Build、Verify、Ship 是什麼？AI 寫程式變快後，進度要怎麼算？（2026 完整懶人包）：Verify 這一關在整個交付流程裡的位置，以及驗收條件為什麼要在開工前就寫好。

參考資料

• Wikipedia. Moving sofa problem（問題沿革、構造與上下界數值）.

• Quanta Magazine. 移動沙發問題報導（Baek 學經歷與 Gerver、Zieve 受訪引言）.

• Baek, Jineon (2024-11-29). Optimality of Gerver's Sofa. arXiv:2411.19826.

• Cureton, Dean. MovingSofa（專案 README，形式化過程與結果的自述）.

• Lean. Axioms and Computation. Theorem Proving in Lean 4.