Show HN：形式化驗證的多邊形交集算法——Opus 4.8 一次搞定，此前失敗
該項目首次實現了形式化驗證的多邊形交集算法，利用 Lean 4 證明助手確保無限點集交集等式的正確性。開發過程藉助 AI 代理（Claude Opus 4.8）自動完成證明和實現，人類只需審查 87 行規格説明。文章介紹了算法背景、驗證挑戰以及 AI 代理能力的演進。
文章情報
要點
- 首個經過形式化驗證的多邊形交集算法實現，使用 Lean 4 證明助手。
- AI 代理（Claude Opus 4.8）能夠自主編寫證明和代碼，人類僅需審查簡短規格。
- 形式化驗證確保了即使面對無限配置的輸入，算法也保證正確。
- Opus 4.8 相比早期版本能處理更大規模的證明策略，並自動規避錯誤中間定理。
為甚麼重要
這條新聞值得關注，因為首個經過形式化驗證的多邊形交集算法實現，使用 Lean 4 證明助手。
技術影響
可能影響模型選型、推理成本、產品能力和評測基準。
在計算幾何領域，多邊形交集是一個基礎但複雜的問題。近日，開發者 schildep 在 GitHub 上發佈了“verified-polygon-intersection”項目，宣稱實現了首個經過形式化驗證的多邊形交集算法。該項目利用 Lean 4 證明助手，從數學上嚴格證明了算法對於任意多邊形配置的正確性。
傳統的軟件測試無法窮舉所有輸入情況，尤其是多邊形頂點可能存在無數種特殊排列。形式化驗證則通過嚴謹的邏輯推理，保證算法滿足規格説明，從而徹底消除不確定性。在本項目中，人類審查者只需閲讀 87 行的規格文件（定義基本幾何概念和交集屬性），其餘數千行代碼和證明均由 AI 代理自動生成。
文章詳細介紹了多邊形交集的數學基礎：將多邊形視為由頂點定義的內部點集，交集即為兩個點集的公共部分。這一看似直觀的概念，在形式化證明中卻需要處理大量隱含的幾何事實。例如，證明定義的內部集與射線方向無關就耗費了上千行 Lean 代碼。
AI 代理的能力演進是本文的另一亮點。開發者最初在年初嘗試使用 Claude Opus 4.5 和 4.6，但發現它們需要用户提供詳盡的證明策略。Opus 4.7 有所改善，能自動完成一些步驟，但仍需人工提示。直到 Opus 4.8，模型能夠在無人干預下，從零開始證明核心定理並生成完整的算法代碼。值得注意的是，Opus 4.8 在遇到可能的錯誤中間定理時，會自主轉向替代策略，甚至並行運行多個子代理試探不同方案。
儘管 AI 代理完成了大部分工作，但開發者強調信任完全來源於 Lean 檢查器，而不是大語言模型。同時，他們也指出當前代碼為了通過驗證而犧牲了部分性能，後續計劃優化算法、簡化證明，並添加 SVG 導入/導出等功能。
該項目不僅展示了形式化驗證在計算幾何中的應用潛力，也反映了 AI 在定理證明領域的快速進步。對於關注軟件可靠性或 AI 能力的讀者來説，這無疑是一個值得關注的開源項目。