用AI辅助形式化证明等离子体平衡方程，10天完成，零代码，成本200美元。
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
- AI生成猜想，工具自动转为Lean代码，专业证明器验证111个引理
- 仅1位数学家监督，耗时10天，总成本200美元，零行代码
- 适合对形式化验证、AI科研协作感兴趣的学者
我们完成了描述带电等离子体运动的Vlasov-Maxwell-Landau（VML）系统平衡特征的完整Lean 4形式化。该研究展示了端到端的AI辅助数学研究流程：AI推理模型（Gemini DeepThink）从猜想生成证明，代理编码工具（Claude Code）将自然语言提示转化为Lean代码，专用证明器（Aristotle）验证了111个引理，最终由Lean内核完成验证。整个过程由一名数学家在10天内监督完成，花费200美元，未编写任何代码。所有229条人工提示与213次git提交均公开存档。报告了详细的AI失败模式（如假设蔓延、定义对齐错误、代理回避行为），以及有效策略：抽象/具体证明分离、对抗性自审，以及关键定义和定理陈述的人工审查。值得注意的是，形式化工作在对应数学论文最终稿完成前即已结束。
原文摘要 · Abstract (English)
We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the full AI-assisted mathematical research loop: an AI reasoning model (Gemini DeepThink) generated the proof from a conjecture, an agentic coding tool (Claude Code) translated it into Lean from natural-language prompts, a specialized prover (Aristotle) closed 111 lemmas, and the Lean kernel verified the result. A single mathematician supervised the process over 10 days at a cost of \$200, writing zero lines of code. The entire development process is public: all 229 human prompts, and 213 git commits are archived in the repository. We report detailed lessons on AI failure modes -- hypothesis creep, definition-alignment bugs, agent avoidance behaviors -- and on what worked: the abstract/concrete proof split, adversarial self-review, and the critical role of human review of key definitions and theorem statements. Notably, the formalization was completed before the final draft of the corresponding math paper was finished.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。