Science 报道：Lean 证明证书并非万无一失，自动形式化严谨性或被高估

Science 报道指出，AI 生成的数百页数学新证明常附 Lean 证明检查器证书，但 Lean 形式化与自动形式化流程仍存在裂缝。报道认为，这些机器验证提供的保证可能不如表面可靠，形式化验证社区需要正视自动证明的严谨性局限。