Formally verified polygon intersection - Opus 4.8 oneshots, prev failed

这个项目用 Lean 4 形式化描述 multipolygon intersection 的规格，并验证算法输出的内部点集确实等于两个输入内部点集的交集。README 里最有信息量的地方不是“AI 写了代码”，而是信任边界：人类只需审阅 DataStructures、Defs 和 precondition-check algorithm 相关的 3 个规格文件，约 87 行 Lean，再运行 checker。局限也写得清楚：为便于证明，AI 生成实现可能牺牲性能和实际工程考量，下一步是优化性能和简化证明。