Lean 4 形式化验证 3D CSG 只靠 93 行规格
permute · hn · 2026-07-28
用 Lean 4 形式化验证 3D CSG 网格相交
作者声称这是首个形式化验证的 3D constructive solid geometry（CSG）实现，具体是网格相交操作。核心实现写在 Lean 4 里，并用一份只有 93 行的形式化规格说明来约束结果网格的表面定义与三角剖分的可用性条件。
这个项目同时也是一次“尽量不信任 AI 生成代码”的实验：人类只需要读规格说明并运行 Lean checker，而由 agent 自动写出的 6 万多行 Lean 证明无需人工逐行审查。正确性在编译期由 Lean 保障，底层实现和证明都可视为黑盒。作者还提供了一个把验证后的内核编译成 WebAssembly 的浏览器演示。
「编程与Agent」频道最新
- 开源 Google Analytics MCP Server:自然语言查网站数据 — modelcontextprotocol · 2026-10-16
- UPenn 实验：让 Claude 批判自己默认想法,研究灵感产出提升最多 — arjunrajlab · 2026-10-16
- 实测 11 种提示策略催 LLM 创意：直接要「非显而易见」的点子最有效 — arjunrajlab · 2026-10-16
- a16z 播客:AI 让 10 人公司效率翻倍,工程师差距拉大 10 倍 — a16z · 2026-10-16
- Agent 跑任务卡死屏幕，用户每五分钟喊一次「等一下」 — every · 2026-10-16
- 用 3000 条真实发布片喂 Claude:作者做 MCP 告别千篇一律的 AI 生成视频 — Designer_Landscape25 · 2026-10-16