标签
本文对五个广泛使用的Lean定理证明基准进行了审计，发现了398个机械可验证的问题，例如反例、空洞定理和不健全的公理。它提出了一个故障分类法、自动化检查器和发布标准，以提高评估的可靠性和可信度。
谷歌新论文提出LEAP框架，一种智能体框架，使通用大语言模型能够通过规划证明并检查每一步来解决形式化数学问题，在Lean IMO基准测试上将性能从低于10%提升至70%，并解决了所有2025年的Putnam问题。