形式化验证研究者长文反思：形式化变廉价之后

Kaiyu Yang 自 2018 年起研究机器学习用于形式化定理证明，曾开发 CoqGym、LeanDojo 并参与 Goedel-Prover。他发布一篇 25 分钟长文，探讨 AI 与形式化验证结合的当前热潮，并反思一个更深层的问题：当形式化的成本变得足够低廉时，这一技术能够解决哪些真正有价值的问题。

2026-09-25 ~ 2026-09-25 · 2 条相关

• 深耕形式化验证 8 年，Kaiyu Yang 反思形式化变廉价后能解决什么 — KaiyuYang4 · 2026-09-25
• 深耕形式化验证多年的研究者反思:当形式化变廉价会发生什么 — IanArawjo · 2026-09-25