Agent 自主生成形式化验证求解器
burny_tech · x · 2026-07-18
Lanyon 生成了一个**端到端形式化验证**的 PDE 求解器，覆盖线性平流、各向同性平流-扩散以及完整/各向异性平流-扩散方程。 - 规模：约 **8,000 行**经验证的仿真代码 + **10,000 行 Lean 4 证明** - 耗时：约 **158 秒**完成 - 结果：对二维到三维的多种方程，都给出了**每一项性质的正确性证明** 作者强调，这是首个针对平流-扩散方程的**端到端形式化验证求解器**，完全由 agent 自主生成。