Vlasov-Maxwell-Landau平衡的半自主形式化

我们完成了对Vlasov-Maxwell-Landau（VML）系统（描述带电等离子体的运动）中平衡刻画的完整Lean 4形式化。该项目展示了完整的AI辅助数学研究闭环：AI推理模型（Gemini DeepThink）从一个猜想出发生成证明，智能体编程工具（Claude Code）依据自然语言提示将其翻译为Lean，专用证明器（Aristotle）关闭了111个引理，最后由Lean内核验证结果。一位数学家用10天时间监督了这一过程，成本为200美元，未写一行代码。整个开发过程完全公开：全部229条人类提示和213次git提交均存档于代码仓库中。我们详细报告了关于AI失败模式的教训——假设蔓延、定义对齐错误、智能体回避行为——以及行之有效的做法：抽象/具体证明拆分、对抗性自审，以及对关键定义和定理陈述进行人工审查这一关键环节。值得注意的是，形式化的完成时间早于相应数学论文终稿的完成。