Strong Mason conjecture for matroid independent sets

strong_mason_conjecture

Submitter: Kim Morrison.

Notes: For a finite Mathlib `Matroid`, `independentSetCount M k` is exactly the number of independent `k`-element subsets of its ground set. The theorem is the division-free form of ultra-log-concavity of these counts: if the ground set has cardinality `n` and `0 < k < n`, then `I_k^2 k(n-k) >= I_{k-1} I_{k+1} (k+1)(n-k+1)`. Using `M.E.ncard`, rather than the cardinality of the ambient type, is essential because Mathlib matroids carry an explicit ground set.

Source: P. Branden and J. Huh, 'Lorentzian polynomials', Ann. of Math. 192 (2020), 821-891, Theorem 4.14, https://doi.org/10.4007/annals.2020.192.3.4; independently N. Anari, K. Liu, S. Oveis Gharan, and C. Vinzant, 'Log-concave polynomials III: Mason's ultra-log-concavity conjecture for independent sets of matroids', https://arxiv.org/abs/1811.01600.

Informal solution: Branden and Huh associate to a matroid its homogenized multivariate Tutte polynomial and prove that this polynomial is Lorentzian. Lorentzian polynomials remain Lorentzian under the relevant specializations and directional derivatives, and their coefficients satisfy normalized log-concavity. Applying this to the independent-set generating polynomial gives `(I_k / choose n k)^2 >= (I_{k-1} / choose n (k-1)) (I_{k+1} / choose n (k+1))`. Clearing the positive binomial denominators for `0 < k < n` yields exactly the natural-number inequality in the Lean statement. Anari, Liu, Oveis Gharan, and Vinzant independently proved the same strongest form using complete log-concavity and high-dimensional random walks.

theorem declaration uses `sorry`strong_mason_conjecture {α : Type*} (M : Matroid α) [M.Finite]
    (k : ℕ) (hk : 0 < k) (hkn : k < M.E.ncard) :
    independentSetCount M (k - 1) * independentSetCount M (k + 1) *
          (k + 1) * (M.E.ncard - k + 1) ≤
      independentSetCount M k ^ 2 * k * (M.E.ncard - k) := byα:Type u_1M:Matroid αinst✝:M.Finitek:ℕhk:0 < khkn:k < M.E.ncard⊢ independentSetCount M (k - 1) * independentSetCount M (k + 1) * (k + 1) * (M.E.ncard - k + 1) ≤
  independentSetCount M k ^ 2 * k * (M.E.ncard - k)
  sorryAll goals completed! 🐙

Solved by

• @ZhengyangZhang06 with Humanifa + GPT 5.6 sol on Aug 3, 2026

• @hanwenzhu with Seed Prover (ByteDance) on Aug 4, 2026