Automation Without Understanding

这篇短论讨论 AI 参与研究级数学后，数学基础设施要怎样从“读懂完整推导”转向“审计机器可检查的关键声明”。它提出把 AI 产出的核心 claim 暴露为可形式化、可验证对象，并强调人类数学家的解释、反例构造和挑战能力仍然是系统的一部分。文章更像研究议程而非实验论文，局限也在这里：它提出的是验证架构和社会技术分工，还不是一个已经跑完的数学自动化系统。