8500行C代码配1.5万行Lean，物理方程验证引关注
kylekabasares · x · 2026-07-21
开发者展示了将AI与物理算法结合的严谨实践：针对电动力学中的麦克斯韦方程组，Lanyon不仅用约8500行经过形式化验证的C代码实现了保持双曲性的波传播算法，还使用Lean语言编写了约1.5万行代码进行验证，证明了包括收敛性、L2稳定性在内的156个正确性定理，且精度严格下探至浮点数级别。
「研究」频道最新
- 斯坦福数据中心化 AI 研讨会开放报名，海报截止延期 — jure · 2026-10-26
- 「氛围验证」研究：近 60% 的形式化证明证明的不是作者本意 — basedjensen · 2026-10-26
- 浏览器助手 Ito 读懂浏览意图，自动把标签页编排成 Flows — andrewkuznet · 2026-10-26
- 康奈尔研究称大脑按线性序列处理语言,挑战乔姆斯基层级语法;印度语言成反例讨论点 — anirbanbandyo · 2026-10-26
- Hi3D V1.0 开源发布：训练资产翻四倍，切片成功率 90% — kimmonismus · 2026-10-26
- Ortet 首次健康评测：34 个开源模型跑 50 项任务，综合排名不够用 — elmanmansimov · 2026-10-26