论文：Lean验证不能保证自然语言证明正确

Bastounis、Circelli 和 Hansen 在 arXiv 论文 arXiv:2610.08144 中论证，AI 把自然语言证明自动形式化（autoformalisation）后即使通过 Lean 机械验证，也不能保证原始自然语言论证正确，原因在于翻译难以做到语义忠实。作者称，这一过程可能无法为原始自然语言论证提供任何可信度。 该结论针对的是 AI 自动形式化翻译这一环节，而非 Lean 验证器本身的可靠性。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。