Binomial Edge Ideals

Formalization of Herzog–Hibi–Hreinsdóttir–Kahle–Rauh (2010)

This project formalizes the main algebraic results of Binomial edge ideals and conditional independence statements in Lean. The Gröbner basis, radicality, prime decomposition, dimension, and conditional-independence bridge are formalized. The remaining paper-level gap is the Cohen–Macaulay step around Proposition 1.6 and the corollaries that depend on it.

Overview Definitions Section 1 Section 2 Section 3 Section 4

Published paper arXiv Detailed status

18 / 21 main results completed

3 paper-level gaps remain

Current status: the project already covers the main Gröbner, radicality, prime-decomposition, and conditional-independence results from the paper. What remains is the depth-based Cohen–Macaulay route behind Proposition 1.6 and its consequences.

Start Here

Binomial edge ideals attach a quadratic binomial ideal to a graph. The paper studies when these ideals admit quadratic Gröbner bases, how their prime decomposition reflects the graph, and how they connect to conditional independence statements from algebraic statistics.

This site is organized by the paper’s four sections. Each section page lists the paper results, the corresponding Lean declarations, and how closely the formal statement matches the published one.

Main Results

Closed graphs and quadratic Gröbner bases Theorem 1.1 and the main Section 1 graph-theoretic consequences are formalized.

Section 2 complete The Gröbner basis theorem and the radicality corollary are formalized.

Prime decomposition and dimension theory The prime ideals, prime decomposition, dimension formula, minimal primes, and non-Cohen–Macaulay cycle branches are formalized.

Section 4 complete Conditional independence ideals are linked to binomial edge ideals, with bridge theorems, radicality, prime decomposition, and minimal-prime results.

Remaining Cohen–Macaulay step The paper-faithful Cohen–Macaulay proof of Proposition 1.6, and the downstream CM branches of Corollaries 3.4 and 3.7, are still open.

Explore By Section

Foundations Definitions, term order, and Gröbner setup the main objects and theorems used across the project Section 1 Closed graphs and quadratic Gröbner bases 5 done, 1 open Section 2 Reduced Gröbner basis and radicality complete Section 3 Prime decomposition, dimension, minimal primes prime and dimension results complete; CM branch partial Section 4 Conditional independence ideals and robustness bridge theorems and the main binary-output results are complete

Featured Theorems

Each card shows a paper statement and the corresponding Lean theorem. The Lean side includes the declaration name and a representative snippet, but the section pages give the fuller context.

Paper

The quadratic generators of $J_G$ form a Gröbner basis for the lexicographic order $x_1 > \cdots > x_n > y_1 > \cdots > y_n$ if and only if $G$ is closed.

Lean

theorem_1_1

theorem theorem_1_1 (G : SimpleGraph V) :
    binomialEdgeMonomialOrder.IsGroebnerBasis (generatorSet (K := K) G)
      (binomialEdgeIdeal (K := K) G) ↔
    IsClosedGraph G :=
  ⟨groebner_implies_closed G, closed_implies_groebner G⟩

View proof in ClosedGraphs.lean

Paper

The binomial edge ideal $J_G$ is radical.

Lean

corollary_2_2

theorem corollary_2_2 (G : SimpleGraph V) :
    (binomialEdgeIdeal (K := K) G).IsRadical := by

View proof in Radical.lean

Paper

The binomial edge ideal decomposes as $J_G = \bigcap_{S \subseteq V(G)} P_S(G)$.

Lean

theorem_3_2

theorem theorem_3_2 (G : SimpleGraph V) :
    binomialEdgeIdeal (K := K) G =
      ⨅ S : Finset V, primeComponent (K := K) G S := by

View proof in PrimeDecomposition.lean

Paper

For a binary-output robustness specification, the conditional independence ideal equals the binomial edge ideal of the associated union graph.

Lean

ciIdealSpec_eq_binomialEdgeIdeal

theorem ciIdealSpec_eq_binomialEdgeIdeal (stmt : ι → CIStatement Ω) :
    (ciIdealSpec stmt : Ideal (MvPolynomial (BinomialEdgeVars Ω) K)) =
    binomialEdgeIdeal (ciGraphSpec stmt) := by

View proof in CIIdeals.lean

Current Paper-Level Gaps

Proposition 1.6 Final Cohen–Macaulay step

The graph reduction and most of the Herzog–Hibi side are formalized. The remaining step is the final Cohen–Macaulay base case on the HH side, followed by the transfer back to the original ideal.

See Section 1

Corollary 3.4 Dimension from Cohen–Macaulayness

The project proves the equidimensional consequence. The paper's Cohen–Macaulay implication is still waiting on Proposition 1.6.

See Section 3

Corollary 3.7 Cycle-graph CM branch

The prime and unmixed branches are formalized. The Cohen–Macaulay branch remains open for the same reason as Proposition 1.6.

See Section 3

Code And Status

Lean files Supporting library Formalization map Current task list