数学家Thomas Hales在Terence Tao博客发表客座文章指出：自动形式化——用AI把数学论文翻译成Lean等语言下计算机可验证的证明——今年已从设想变为实用技术。相比之下，历史上依赖人工的验证需要巨大投入：仅Kepler猜想的验证就耗费了约20个人类工作年。
Hales同时提到了所谓的「可靠性之夏」（Summer of Soundness Bugs）：今年7、8月间，Lean系统先后被发现若干可靠性（soundness）缺陷，但均在短期内被迅速修复，显示出形式化社区对基础工具质量的响应速度。
自动形式化被广泛视为AI对数学最确定的价值路径：它不追求让AI「原创定理」，而是承担把人类证明翻译为机器可验证形式的繁重工作。随着大模型对数学语言理解的提升与Lean生态的成熟，数学共同体的验证产能有望获得数量级提升。此前OpenAI曾一日撤回3篇数学手稿，也从反面印证了机器验证环节的必要性。