数学家 Scott Armstrong：AI 可代写引理证明，但 arXiv 投稿必须附完整 Lean 形式化

数学家 Scott Armstrong 提出，AI 可将 PDE 等领域的说服性证明提纲扩写为完整证明，但 arXiv 投稿若涉及 100+ 页证明，必须附带完整 Lean 形式化。他强调，逐条手工打磨引理如同“计算器式”工作；其担任编委的期刊可能直接退回未提供形式化的论文，要求补齐后重投。