半自主形式化的Vlasov-Maxwell-Landau平衡
人工智能
2026-04-02 v2 偏微分方程分析
逻辑
摘要
我们提出了对Vlasov-Maxwell-Landau（VML）系统平衡特征描述的完整Lean 4形式化，该系统描述带电等离子体的运动。该项目演示了完整的AI辅助数学研究循环：AI推理模型（Gemini DeepThink）从猜想生成证明，代理编码工具（Claude Code）从自然语言提示将其翻译为Lean代码，专用证明器（Aristotle）关闭111个引理，Lean内核验证结果。一位数学家在10天内监督该过程，仅需200美元，编写了零行代码。整个开发过程均为公开：存储库中存档了所有229个人类提示和213个git提交。我们报告了关于AI失败模式的详细经验——假设 creep、定义对齐错误、代理回避行为——以及成功经验：抽象/具体证明划分、对抗性自我审查以及对关键定义和定理陈述的人类审查的关键作用。值得注意的是，在 corresponding math paper 最终草稿完成之前，该形式化工作已完成。
引用
@article{arxiv.2603.15929,
title = {Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium},
author = {Vasily Ilin},
journal= {arXiv preprint arXiv:2603.15929},
year = {2026}
}
备注
11 figures