93 行規範取代 1000+ 行程式：Lean 4 打造可驗證的 3D CSG 運算核心
為何重要
這代表了軟體工程信任架構的演變：開發者從「信賴人類撰寫的複雜程式碼」轉移到「信賴狹義的規格定義」，將鏈條最難的驗證環節交給形式驗證工具（Lean 4）處理。對產業的意義在於揭示 LLM 的高產能潛力不全然是商業化問題，而是工程過程中的「信任盲點」；此類案例證明形式驗證技術可作為開發者與 AI 生產力工具之間的安全橋樑。
作者在 Lean 4 中實現了無人檢視的程式碼，將複雜的 AI 生成證明外包並極簡化人類審查流程，只要核對 93 行形式化規格，即可確保 3D 網格交集運算的正確性。
- 專案採用零信任 AI 模式：人類審查者僅需閱讀 93 行規格與執行 Lean 檢查器，無需閱讀撰寫超過 1000 行的 AI 實作程式碼。
- AI 自動生成超過 60,000 行 Lean 證明（CSG/Proof/），這些證明與實作皆視為黑箱，僅規格需經可信賴的人類審查。
- 效能的代價：為了最小化人類審查 effort，實作在處理兩隻 70k 三角形斯坦福兔子模型時需耗時 24 秒。