論文の概要: A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game

• arxiv url: http://arxiv.org/abs/2607.08986v1
• Date: Thu, 09 Jul 2026 23:17:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-13 14:47:12.75558
• Title: A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game
• Title（参考訳）: フラソフ方程式の平均場微分の形式化:戦略ゲームとしてのAI支援型リーン形式化
• Authors: Joseph K. Miller,
• Abstract要約: 我々は、数学者がAIシステムに指示することで、Lean 4証明アシスタントの研究結果を形式化し、そのアクティビティを形式化ゲームとしてフレーム化する。 目的は文書をリーンに変えることである。ゲームは開発がコンパイルされたときに勝利し、残念なことは含まない。マシンチェックは、目標定理がリーンの基本公理にのみ依存していることを示している。 ケーススタディは、ドブルシンの平均場経路を通した非線形ブラソフ方程式の正当性に対する完全で公理クリーンな定式化である。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game. The objective is to turn a LaTeX document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone. Reuse is a second check, by a definition we introduce: whether the development yields a self-contained layer of general mathematics the wider library could absorb. The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route -- existence, uniqueness, the stability estimate and mean-field limit, and a short-window superposition principle (weak solutions are Lagrangian). The human's role was to direct, not to write proofs: to scope the definitions, steer the decompositions, and triage the library's gaps; the AI agent executed. The formalization certifies the proof of each statement as written; whether the written statement is the intended theorem stays the mathematician's judgment. The optimal-transport machinery that fell out of the build (in particular, properties of the Wasserstein-1 metric and the Kantorovich-Rubinstein duality theorem) separates into a self-contained layer that compiles against Mathlib alone: about a sixth of the development (49 of 299 declarations), behind a 22-declaration interface with no reverse dependency. The headline theorems ran in about a week, the full development in about a month. We report the quantitative claims as observations of one game, not as general laws. The game's rules name no particular system, so the methodological framing is meant to outlast the tools of any one run.
• Abstract（参考訳）: 我々は、数学者がAIシステムに指示することで、Lean 4証明アシスタントの研究結果を形式化し、そのアクティビティを形式化ゲームとしてフレーム化する。 目的は、LaTeXドキュメントをリーンに変換することです。 ゲームは、開発がコンパイルされたときに勝利し、残念なことはなく、マシンチェックは、目標定理がリーンの基本公理にのみ依存していることを示している。 リユース(Reuse)は、私たちが導入した定義によれば、一般数学の自己完結した層が、より広いライブラリに吸収されるかどうかという2つ目のチェックである。 ケーススタディは、ドブルシンの平均場経路(存在、一意性、安定性推定および平均場限界)および短窓重ね合わせ原理(弱解はラグランジアンである)を介して非線形ブラソフ方程式の正当性の完全公理的形式化である。 人間の役割は、証明を書くのではなく、定義をスコープし、分解を操縦し、ライブラリのギャップを埋めることであった。 形式化は各文の証明を書式として証明し、書式が意図された定理であるか否かは数学者の判断のままである。 ビルドから外れた最適輸送機械(特にワッサーシュタイン1計量とカントロヴィチ・ルビンシュタイン双対性定理の特性)は、マドリブのみに対してコンパイルされる自己完結層に分離される。 見出し定理は約1週間で実行され、完全な開発は約1ヶ月で完了した。 定量的な主張は、一般的な法則ではなく、一つのゲームの観察として報告する。 ゲームのルールは特定のシステムとは呼ばないので、方法論的なフレーミングは、どのランニングツールよりも長持ちすることを意味している。

関連論文リスト

• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。 最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。 汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-06-30T05:05:03Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。 4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。 我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
  論文  参考訳（メタデータ） (2026-06-03T20:09:39Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving [13.446180044466324]
  メカニック(Mechanic)は、謝罪駆動の形式的分解戦略を採用した新しいエージェントシステムである。 未解決のサブゴールを正確に分離するために、リーンの残念なプレースホルダーを活用することで、Mechanicは失敗するサブプロブレムを、クリーンで自己完結したコンテキストに抽出し、独立して解決する。
  論文  参考訳（メタデータ） (2026-03-25T16:12:08Z)
• Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium [0.564046562677526]
  本稿では、VML(Vlasov-Maxwell-Landau)システムにおける平衡特性の完全式化について述べる。 プロジェクトはAIによる数学的研究の完全なループを実証する。
  論文  参考訳（メタデータ） (2026-03-16T21:21:53Z)
• Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
  本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。 エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。 この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
  論文  参考訳（メタデータ） (2026-02-02T16:24:53Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。