形式化还是非形式化?人工智能证明定理之问

摘要

计算机证明数学正处于有趣时期。对于计算机能否自主证明研究级数学定理，作者持不确定态度，但更看好AI成为数学家的有用助手，正如其当前用Lean教授研究级定义和证明的工作。就IMO问题而言，有四种公开尝试：两种用语言模型写英文证明（非形式化），两种用语言模型与Lean混合（形式化）。作者担忧非形式化方法：期刊收到越来越多由LLM生成的看似合理的论文，且有时未披露使用，并列举LLM论文与人类论文的差异，如LLM倾向于迎合。