AI 时代反问题的形式化：可能、陷阱与邀请
原标题：Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation
AI 摘要
论文介绍 AutoIP——一个用 AI 智能体自动形式化的 Lean 4 库，涵盖经典线性正则化理论及其依赖的泛函分析。作者指出，机器验证的证明只保证形式陈述本身成立，真正需要人工审查的是形式陈述是否忠实表达原意，并发现教科书定理的假设比声称的更严格。作者邀请反问题社区扩展该库，认为形式化成本骤降将改变应用数学的工作方式。
正文节选
Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation Abstract Proof assistants such as Lean 4 check mathematical proofs down to the axioms, and AI agents have recently made writing such proofs cheap. We describe AutoIP, a Lean 4 library in which classical linear regularization theory, together with the functional analysis it rests on, has been autoformalized by AI agents. A machine-checked proof certifies only the formal statement it proves, so the remaining