論文の概要: Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
- arxiv url: http://arxiv.org/abs/2603.15929v1
- Date: Mon, 16 Mar 2026 21:21:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-18 17:42:06.997806
- Title: Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
- Title（参考訳）: Vlasov-Maxwell-Landau平衡の半自動形式化
- Authors: Vasily Ilin,
- Abstract要約: 本稿では、VML(Vlasov-Maxwell-Landau)システムにおける平衡特性の完全式化について述べる。
プロジェクトはAIによる数学的研究の完全なループを実証する。
- 参考スコア（独自算出の注目度）: 0.564046562677526
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 本稿では,VML(Vlasov-Maxwell-Landau)システムにおける平衡特性の完全式化について述べる。
AI推論モデル(Gemini DeepThink)が予想から証明を生成し、エージェントコーディングツール(Claude Code)が自然言語のプロンプトからリーンに翻訳し、特殊な証明者(Aristotle)が111の補題を閉じ、Leanカーネルが結果を検証した。
1人の数学者が200ドルというコストで10日間にわたってプロセスを監督し、ゼロ行のコードを書いた。
開発プロセス全体が公開されており、すべての229人のプロンプトと213のgitコミットがリポジトリにアーカイブされている。
AIの障害モード -- 仮説のクリープ、定義の調整バグ、エージェントの回避行動 -- に関する詳細な教訓を報告します。
特に、公式化は、対応する数学論文の最終草案が完成する前に完了した。
関連論文リスト
- Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。
エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。
この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
論文 参考訳（メタデータ） (2026-02-02T16:24:53Z) - Mathematics with large language models as provers and verifiers [1.1029146548022293]
ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
論文 参考訳（メタデータ） (2025-10-11T20:35:25Z) - Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph [7.606625807305093]
リーンの予想レベルの形式化のためのシステムであるAriaを紹介します。
Ariaは、2フェーズのGraph-of-Thoughtプロセスを通じて、人間の専門家による推論をエミュレートする。
AriaScorerは、用語レベルの接地のためにMathlibから定義を検索する。
論文 参考訳（メタデータ） (2025-10-06T06:25:11Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。