“近几个月来，出现了大量针对各种新旧结果的 AI 生成证明，其中一些已在证明助手语言 Lean 中形式化。然而，验证某个给定的 Lean 仓库是否确实证明了所声称的命题并非易事，尤其对于不熟悉该领域使用的受众而言……"