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」频道最新
- SemiAnalysis 开源 300 万美元 AgentX 基准，百万上下文测 AI 编程 — AccBalanced · 2026-08-24
- 面向小企业的 AI WhatsApp 助手，该选什么技术栈？ — aarondiaz92 · 2026-08-24
- RAG 新趋势：双阶段文档处理平衡成本与精度 — llama_index · 2026-08-24
- Fabien 分享 agent.md：改进 LLM 辅助代码质量的工作流 — Thrumpwart · 2026-08-24
- 低显存 Qwen 3.8 27B 用户常用插件与技能讨论 — radlinsky · 2026-08-24
- Stanford 新法：LLM 自我验证，分数暴涨 9.3% — Saboo_Shubham_ · 2026-08-24