这篇由 Katherine M. Collins 领衔、共 17 位作者合作完成、于 2026 年 6 月 2 日提交至 arXiv 的论文《Characterizing initial human-AI proof formalization workflows》（arXiv:2606.04273v1，归类于 cs.AI），关注的并不是 AI 在数学证明上的能力上限，而是人类在真实工作流中如何开始使用这类工具。作者在摘要中首先回顾了一个长期存在的问题：数百年来，数学家依靠手写证明来支撑自己的论证，但让证明的有效性能够被自动检验，一直是难点。近年来 AI 系统在代码生成与高层次数学推理上的进步，被认为有望改变人们形式化证明乃至验证证明的方式。与大量专注于基准测试当前前沿水平的工作不同，这篇论文转向研究人对工具的实际使用。
研究采用混合方法，分析 AI 对形式化工作流的初期影响，具体拆成三个问题：人们声称自己希望得到什么；他们眼中实现这些愿景的障碍是什么；以及在实践中他们究竟如何使用并调整 AI。通过一项定性问卷，作者发现受访者的偏好相当多样，但总体上都希望 AI 在形式化过程中提供辅助，同时保留人类对证明发现过程的高层控制权——也就是说，人们想要的是“可控的协作”，而不是把证明探索完全交给机器。
为了考察在上述限制条件下人们实际如何与 AI 协作，研究团队开展了受控的用户实验。参与者在有无 AI 工具辅助两种条件下，将非形式化的数学问题及其证明形式化，题目覆盖不同难度与不同数学领域。结果显示，尽管当时工具在自动形式化方面仍存在明显局限，参与者在被允许使用 AI 工具时，形式化准确率普遍高于独自完成的情况。此外，大多数参与者会灵活地同时使用多种不同的 AI 工具，而非依赖单一系统。
论文最后总结，这项工作揭示了 AI 融入形式化工作流的早期阶段，其中人类与 AI 的参与呈现出密切交织的互动关系。整体来看，该研究的贡献不在于宣布 AI 已经能够独立完成形式化，而在于以实证方式刻画了当前阶段人机协作的真实形态：工具仍有不足，但已经能在受控实验环境中提升人的表现，而使用者也在主动摸索如何组合与调适这些工具。论文以 arXiv 预印本形式发布，DOI 为 10.48550/arXiv.2606.04273，全文提供 PDF、实验性 HTML 以及 TeX 源码等访问方式。