論文の概要: Formalizing Flag Algebras in Lean
- arxiv url: http://arxiv.org/abs/2607.23500v1
- Date: Sun, 26 Jul 2026 07:07:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-28 22:34:15.132184
- Title: Formalizing Flag Algebras in Lean
- Title（参考訳）: リーンにおけるフラッグ代数の形式化
- Abstract要約: ラズボロフのフラッグ代数法は、極端グラフ理論の不等式を証明する強力なツールである。
本手法の機械チェックによる形式化と,証明から保護までのコンパイラについて述べる。
ケーススタディは7つのターン型上界の形式的証明を与える。
- 参考スコア（独自算出の注目度）: 8.924529562496874
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Razborov's flag algebra method is a powerful tool for proving asymptotic inequalities in extremal graph theory, often reducing the task to finding a finite certificate by semidefinite programming. We present a machine-checked formalization of the method for finite simple graphs, together with a certificate-to-proof compiler that turns externally generated certificate data into algebraic proofs checked by Lean. The formalization covers the foundations of the method: partially labeled graphs, their densities in large graphs, the quotient algebra of density expressions, graph-limit semantics through positive homomorphisms, and the downward operators used to average out labels. The compiler treats the external semidefinite programming output as candidate data rather than trusted input: Lean independently computes the required density and multiplication facts, verifies positive semidefiniteness exactly over $\mathbb{Q}$, and carries out the algebraic normalization steps of flag-algebra proofs. Our case studies yield formal proofs of seven Turán-type upper bounds, including Mantel's theorem and the Erdős pentagon theorem, a $C_4$-density bound for triangle-free graphs, and edge-density bounds for $K_4$-free, $K_5$-free, and $C_5$-free graphs. Independently of the compiler, we formalize the matching constructions that complete the exact Turán densities of Mantel's theorem and the Erdős pentagon theorem, and prove two inequalities of Goodman. Our constrained semantics also prompted a meta-theoretic comparison of two ways of imposing graph constraints: building a hereditary constraint into the flag algebra from the start, or testing inequalities afterward on constrained graph limits with labels chosen at random. We state the resulting root-plantability criterion characterizing when the two approaches agree; a forthcoming paper will present the complete account.
- Abstract（参考訳）: ラズボロフのフラグ代数法は、極端グラフ理論における漸近的不等式を証明する強力なツールであり、半有限計画法によって有限証明を見つけるタスクを減少させる。
本稿では,有限単純グラフに対する手法のマシンチェックによる形式化と,外部から生成された証明データをLeanがチェックした代数的証明に変換する証明対保護コンパイラを提案する。
形式化は、部分的にラベル付けされたグラフ、大きなグラフの密度、密度表現の商代数、正準同型によるグラフ極限意味論、ラベルを平均化するために使われる下向き作用素などの基礎を包含する。
リーンは、要求された密度と乗算事実を独立に計算し、$\mathbb{Q}$以上で正半定性を検証し、フラグ代数証明の代数正規化ステップを実行する。
我々のケーススタディでは、マンテルの定理やエルデシュの五角形定理、三角形自由グラフに対する$C_4$-density bound、および$K_4$-free、$K_5$-free、$C_5$-free graphに対するエッジ密度境界を含む7つのタラン型の上界の形式的証明が得られている。
コンパイラとは独立に、マンテルの定理とエルデシュの五角形定理の正確なトゥラン密度を完成させる整合構造を形式化し、グッドマンの不等式を2つ証明する。
我々の制約セマンティクスは、グラフの制約を課す2つの方法のメタ理論的比較も引き起こした: フラグ代数に遺伝的制約を最初から組み込んだり、ランダムに選択されたラベルで制約付きグラフの制限で不等式をテストする。
本稿では,2つのアプローチが一致する場合に特徴付ける根植性基準について述べる。
関連論文リスト
- AutoGraphForge: Towards Automated Graph Theory Discovery [0.0]
AutoGraphForgeは、自動グラフ理論の導出-拡散-ホルマライゼーション-自明なシステムである。
新規性フィルタは、既知の結果によって既に候補が示唆されているか否かを線形プログラムを介して決定する。
HPCクラスタ上で数ラウンド実行されると、リフューテーションデータセットを生き残った6,522ドルの予想が生成される。
論文 参考訳（メタデータ） (2026-09-03T07:35:29Z) - Neurosymbolic Discovery of Algebraic Graph Constructions [22.962110170304594]
この生データのみを提供する場合、短い代数的記述を自動的に発見できるかどうかを問う。
本研究では,汎用的な大規模言語モデル上で,微調整や目標ごとの訓練を行わないエージェントを提案する。
提案手法は高対称性グラフ100のベンチマークで検証する。
論文 参考訳（メタデータ） (2026-08-08T13:07:51Z) - Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound [0.0]
mathbbR3$ の最小コシェン=スペクターベクトル系に対する最もよく知られた下界は、半分が DRAT を出力するが、幾何的半分がそうでないような計算証明に依存する。
正則な正則な正則ケースツリー証明を導入し、その分割は分解因子と正則な二乗分解である。
すべての証明書、チェッカー、証明は、単一のビルドから利用可能で、再生可能である。
論文 参考訳（メタデータ） (2026-07-29T02:53:00Z) - VeriGraph: Towards Verifiable Data-Analytic Agents [71.17693022916896]
LLMをベースとしたエージェントは、データ集約分析タスクにおいて強力な能力を示してきたが、その出力は滅多に検証されていない。
We propose VeriGraph, a traceable neuro-symbolic reasoning framework that agent can construct an explicit heterogeneous evidence directed acyclic graph。
以上の結果から,明示的なエビデンスグラフ構築がデータ分析エージェントの検証に期待できる道のりであることが示唆された。
論文 参考訳（メタデータ） (2026-06-15T11:50:56Z) - TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。
本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。
公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
論文 参考訳（メタデータ） (2026-03-13T07:39:47Z) - Dimensional Constraints from SU(2) Representation Theory in Graph-Based Quantum Systems [0.0]
抽象グラフエッジが内部自由度を持つが、幾何学的性質が欠如している場合、表現理論から生じる次元的制約について検討する。
このような内部自由度が方向情報のみを符号化できることを証明し、最小表現として$mathbbC2$の量子状態を必要とする。
この結果は、次元構造が、量子情報理論、離散幾何学、量子基礎と潜在的に関連して、情報理論の制約からどのように導出されるかを示す。
論文 参考訳（メタデータ） (2026-01-20T10:40:22Z) - Jet Functors and Weil Algebras in Automatic Differentiation: A Geometric Analysis [0.0]
ジェットバンドルとワイル代数を用いた自動微分(AD)の幾何学的定式化を提案する。
正確さ、安定性、複雑さに関する簡潔な言明を導き出す。
この枠組みは、微分幾何学のレンズを通してAD理論を解釈する。
論文 参考訳（メタデータ） (2025-10-16T06:25:24Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - A framework for generalizing toric inequalities for holographic entanglement entropy [0.10923877073891444]
我々は citeCzech:2023xed のトーリック不等式の一般化を予想する。
次に、一般化トーリック不等式に対する証明法を2つの方法で拡張する。
最初の拡張はユークリッド空間をタイリングすることによってトーリック不等式と一般化トーリック予想に対応するグラフを構成する。
2つ目の拡張では、不等式と予想の巡回性質を利用してサイクルグラフを構成する。
論文 参考訳（メタデータ） (2024-08-08T19:51:23Z) - Tight and fast generalization error bound of graph embedding in metric
space [54.279425319381374]
非ユークリッド計量空間へのグラフ埋め込みは、既存の有界よりもはるかに少ない訓練データを持つユークリッド空間におけるグラフ埋め込みよりも優れていることを示す。
我々の新しい上限は、既存の上限よりもかなり強く速く、最大で$R$と$O(frac1S)$に指数関数できる。
論文 参考訳（メタデータ） (2023-05-13T17:29:18Z) - Isotropic Gaussian Processes on Finite Spaces of Graphs [71.26737403006778]
種々の非重み付きグラフの集合上でガウス過程の先行を定義するための原理的手法を提案する。
さらに、未重み付きグラフの同値類の集合を検討し、それに対する事前の適切なバージョンを定義する。
化学の応用に触発されて、我々は、小データ構造における実際の分子特性予測タスクについて、提案手法を解説した。
論文 参考訳（メタデータ） (2022-11-03T10:18:17Z) - From Width-Based Model Checking to Width-Based Automated Theorem Proving [8.131328180219962]
本稿では,ワイドベースモデルチェックアルゴリズムをグラフ理論の妥当性を検証できるアルゴリズムに変換するための一般的なフレームワークを提案する。
我々のフレームワークはモジュラーであり、木幅や斜め幅を含むグラフのいくつかのよく研究された幅測度に対して適用することができる。
論文 参考訳（メタデータ） (2022-05-23T01:56:52Z) - Learning Sparse Graph with Minimax Concave Penalty under Gaussian Markov
Random Fields [51.07460861448716]
本稿では,データから学ぶための凸解析フレームワークを提案する。
三角凸分解はその上部に対応する変換によって保証されることを示す。
論文 参考訳（メタデータ） (2021-09-17T17:46:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。