Formalizing Flag Algebras in Lean

• URL: http://arxiv.org/abs/2607.23500v1
• Date: Sun, 26 Jul 2026 07:07:29 GMT
• Title: Formalizing Flag Algebras in Lean
• Abstract summary: Razborov's flag algebra method is a powerful tool for proving inequalities in extremal graph theory.<n>We present a machine-checked formalization of the method, together with a certificate-to-proof compiler.<n>Case studies yield formal proofs of seven Turn-type upper bounds.
• Score: 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.

Related papers

• AutoGraphForge: Towards Automated Graph Theory Discovery [0.0]
  AutoGraphForge is an automated graph-theoretic conjecturing-refuting-formalizing-trivial system.<n>A novelty filter decides via a linear program whether a candidate is already implied by known results.<n>Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset.
  arXiv  Detail & Related papers  (2026-09-03T07:35:29Z)
• Neurosymbolic Discovery of Algebraic Graph Constructions [22.962110170304594]
  We ask whether one can automatically discover a short algebraic description if only this raw data is provided.<n>We propose an agent that runs on a general-purpose large language model with no fine-tuning or per-target training.<n>We test the approach on a benchmark of 100 highly symmetric graphs.
  arXiv  Detail & Related papers  (2026-08-08T13:07:51Z)
• Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound [0.0]
  The best known lower bound for the minimum Kochen-Specker vector system in $mathbbR3$ rests on a computational proof whose half emits DRAT but whose geometric half does not.<n>We introduce exact rational case-tree certificates of real nonembeddability, whose splits are factorizations and rational sum-of-squares decompositions.<n>All certificates, checkers, and proofs are available and replayable from a single build.
  arXiv  Detail & Related papers  (2026-07-29T02:53:00Z)
• VeriGraph: Towards Verifiable Data-Analytic Agents [71.17693022916896]
  LLM-based agents have demonstrated strong capabilities in data-intensive analytical tasks, yet their outputs are rarely verifiable.<n>We propose VeriGraph, a traceable neuro-symbolic reasoning framework that enables agents to construct an explicit heterogeneous evidence directed acyclic graph.<n>Our results suggest that explicit evidence-graph construction is a promising path toward verifiable data-analytic agents.
  arXiv  Detail & Related papers  (2026-06-15T11:50:56Z)
• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  We evaluate the robustness of current ATP systems when applied to a novel definitional framework.<n>We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I.<n>For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem.
  arXiv  Detail & Related papers  (2026-03-13T07:39:47Z)
• Dimensional Constraints from SU(2) Representation Theory in Graph-Based Quantum Systems [0.0]
  We investigate dimensional constraints arising from representation theory when abstract graph edges possess internal degrees of freedom but lack geometric properties.<n>We prove that such internal degrees of freedom can only encode directional information, necessitating quantum states in $mathbbC2$ as the minimal representation.<n>This result demonstrates how dimensional structure can be derived from information-theoretic constraints, with potential relevance to quantum information theory, discrete geometry, and quantum foundations.
  arXiv  Detail & Related papers  (2026-01-20T10:40:22Z)
• Jet Functors and Weil Algebras in Automatic Differentiation: A Geometric Analysis [0.0]
  We present a geometric formulation of automatic differentiation (AD) using jet bundles and Weil algebras.<n>We derive concise statements on correctness, stability, and complexity.<n>This framework interprets AD theory through the lens of differential geometry.
  arXiv  Detail & Related papers  (2025-10-16T06:25:24Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• A framework for generalizing toric inequalities for holographic entanglement entropy [0.10923877073891444]
  We conjecture a generalization of the toric inequalities of citeCzech:2023xed. We then extend their proof methods for the generalized toric inequalities in two ways. The first extension constructs the graph corresponding to the toric inequalities and the generalized toric conjectures by tiling the Euclidean space. In the second extension, we exploit the cyclic nature of the inequalities and conjectures to construct cycle graphs.
  arXiv  Detail & Related papers  (2024-08-08T19:51:23Z)
• Tight and fast generalization error bound of graph embedding in metric space [54.279425319381374]
  We show that graph embedding in non-Euclidean metric space can outperform that in Euclidean space with much smaller training data than the existing bound has suggested. Our new upper bound is significantly tighter and faster than the existing one, which can be exponential to $R$ and $O(frac1S)$ at the fastest.
  arXiv  Detail & Related papers  (2023-05-13T17:29:18Z)
• Isotropic Gaussian Processes on Finite Spaces of Graphs [71.26737403006778]
  We propose a principled way to define Gaussian process priors on various sets of unweighted graphs. We go further to consider sets of equivalence classes of unweighted graphs and define the appropriate versions of priors thereon. Inspired by applications in chemistry, we illustrate the proposed techniques on a real molecular property prediction task in the small data regime.
  arXiv  Detail & Related papers  (2022-11-03T10:18:17Z)
• From Width-Based Model Checking to Width-Based Automated Theorem Proving [8.131328180219962]
  We introduce a general framework to convert a large class of width-based model-checking algorithms into algorithms that can be used to test the validity of graph-theoretic conjectures. Our framework is modular and can be applied with respect to several well-studied width measures for graphs, including treewidth and cliquewidth.
  arXiv  Detail & Related papers  (2022-05-23T01:56:52Z)
• Learning Sparse Graph with Minimax Concave Penalty under Gaussian Markov Random Fields [51.07460861448716]
  This paper presents a convex-analytic framework to learn from data. We show that a triangular convexity decomposition is guaranteed by a transform of the corresponding to its upper part.
  arXiv  Detail & Related papers  (2021-09-17T17:46:12Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.