AI 时代反问题的形式化：可能性、陷阱与倡议

研究人员构建了 Lean 库 AutoIP，由 AI 智能体自动形式化了经典线性正则化理论及其泛函分析基础。该库让审阅者只需比对形式化陈述与自然语言表述而无需阅读证明，并通过对陈述的简单自动化测试揭示出某教科书定理假设过严的问题。团队指出形式化风险主要在于陈述而非机器证明，并邀请反问题学术界共同扩展该库。