在Lean中形式化标志代数
Formalizing Flag Algebras in Lean
浏览论文内容
中文总结 AI 辅助
研究在Lean中形式化标志代数方法，通过编译器将外部证书数据转为代数证明，涵盖方法基础。案例研究给出多个图兰型上界形式证明，还进行了相关构造与证明，以及对施加图约束方式的比较并给出可根植性标准。
中文摘要 AI 辅助
拉兹博罗夫的标志代数方法是证明极值图论中渐近不等式的有力工具，通常将任务简化为通过半定规划找到有限证书。我们给出了有限简单图方法的机器检查形式化，以及一个证书到证明的编译器，它将外部生成的证书数据转换为由Lean检查的代数证明。形式化涵盖了该方法的基础：部分标记图、它们在大图中的密度、密度表达式的商代数、通过正同态的图极限语义以及用于平均标签的向下算子。编译器将外部半定规划输出视为候选数据而非可信输入：Lean独立计算所需的密度和乘法事实，精确验证在有理数域上的正半定性，并执行标志代数证明的代数归一化步骤。我们的案例研究给出了七个图兰型上界的形式证明，包括曼特尔定理和埃尔德什五边形定理、无三角形图的\(C_4\)密度界以及无\(K_4\)、无\(K_5\)和无\(C_5\)图的边密度界。独立于编译器，我们形式化了完成曼特尔定理和埃尔德什五边形定理精确图兰密度的匹配构造，并证明了古德曼的两个不等式。我们的约束语义还促使对施加图约束的两种方式进行元理论比较：从一开始就在标志代数中构建遗传约束，或者随后在随机选择标签的约束图极限上测试不等式。我们陈述了两种方法一致时的结果可根植性标准；即将发表的论文将给出完整说明。
英文摘要
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.
发表机构
- KAIST（韩国科学技术院）
- Institute for Basic Science (IBS)（基础科学研究院（IBS））
- Korea Institute for Advanced Study (KIAS)（韩国高等研究院（KIAS））
机构由 AI 辅助整理，请以论文原文为准。
