本文研究了 AI 代理在交互式定理证明系统 Lean 中的行为与人类协作者的差异。作者提出“模拟协作”方法，通过在九个大型人类合作项目（共 470 万定义、6000 多次提交）中同步记录 AI 与人类的操作，聚焦两个核心问题：\n1) AI 更关注表层语法还是深层语义；\n2) AI 在下一步行动的偏好何时与人类产生分歧。\n实验结果显示，随着证明构建的进行，AI 代理表现出三大倾向：\n- 对显式标记的空缺（gap）极度敏感，远超人类；\n- 回避高度连接的证明核心以及复杂或出乎意料的目标；\n- 对出人意料的证明主体表现出兴趣，但随后倾向于将其规整回常规模式。\n这些发现揭示了人机数学协作中的盲点，提示未来可以通过引导 AI 注意语义关联、降低对表层标记的依赖等方式提升协同效率。\n\n点评：本文提供了系统化的实验框架，为理解 AI 与人类在数学证明中的不同思路奠定了基础，也为设计更友好的人机交互工具指明了方向。