Vlasov-Maxwell-Landau平衡の半自律的な形式化

arXiv cs.AI / 2026/3/18

📰 ニュースDeveloper Stack & InfrastructureTools & Practical UsageModels & Research

共有:

要点

Gemini DeepThink、Claude Code、Aristotle、そして Lean カーネルを含む AI 支援の推論ループを用いて、Vlasov-Maxwell-Landau平衡の完全な Lean 4 の形式化が達成されました。
このプロセスは、単独の数学者の監督のもと、10日間にわたり実施され、費用は200ドルで、手作業で書かれたコードは一行もありませんでした。
この開発は公開されており、229件の人間のプロンプトと213件のGitコミットを記録し、AIの故障モードと抽象的証明と具体的証明の分離、敵対的自己レビューなどの成功戦略を詳述しています。
対応する数学論文の最終稿より前に形式化が完成しており、AI支援による数学研究の迅速で再現性のあるワークフローを示しています。

要約: 私たちは、Vlasov-Maxwell-Landau（VML）系における均衡の特徴付けの完全な Lean 4 形式化を提示します。VML 系は荷電プラズマの運動を記述します。プロジェクトは、AI 支援による完全な数学研究ループを示します。AI 推論モデル（Gemini DeepThink）が予想から証明を生成し、エージェント型コーディングツール（Claude Code）が自然言語のプロンプトから Lean へ翻訳し、専門的な証明支援器（Aristotle）が111個の補題を閉じ、Lean カーネルが結果を検証しました。1 人の数学者がこの過程を10日間監督し、費用は200ドルで、コードは一行も書きませんでした。
開発全体の過程は公開されています：すべての229個の人間のプロンプトと213個の Git コミットがリポジトリにアーカイブされています。我々は AI の故障モードに関する詳細な教訓 — 仮説の膨張、定義整合性のバグ、エージェントの回避挙動 — および機能した点について報告します。抽象的証明と具体的証明の分離、対抗的自己レビュー、そして主要な定義と定理命題の人間によるレビューの決定的な役割がそれです。特筆すべきは、対応する数学論文の最終稿が完成する前にこの形式化が完了していたという点です。