Axiom MathMatroid log-concavity

MATROID THEORY / FORMAL PROOF

Log-concavity,
formalized.

Two theorems about the shape of mathematical sequences, with proofs checked in Lean.

The strongest Mason inequality and the Heron–Rota–Welsh theorem. An Axiom Math companion to the accepted formalizations.

Read the writeup Explore the two proofs ↓
A small exampleU3,5U_{3,5}
Independent sets of the uniform matroid U 3,5For subset sizes zero, one, two and three, the numbers of independent sets are 1, 5, 10 and 10.1510100123Subset size

Five elements. Every set of size at most three is independent.

LEAN 4 + MATHLIB2 accepted formalizationsBoth comparator lanes passedVerification record ↗

THE RESULTS

Two sequences.
A shared inequality.

A nonnegative sequence is log-concave when each middle term dominates the geometric mean of its neighbors. Matroids produce two important examples.

01 / INDEPENDENT SETSAccepted · 1 Sep 2026

The strongest
Mason inequality

Count independent sets by size, then divide by the number of all subsets of that size. The resulting sequence is log-concave.

(Ik(nk))2≥Ik−1(nk−1) Ik+1(nk+1)\left(\frac{I_k}{\binom{n}{k}}\right)^2 \ge \frac{I_{k-1}}{\binom{n}{k-1}}\,\frac{I_{k+1}}{\binom{n}{k+1}}
Combinatorial atlas · HyperbolicityRead the proof
02 / CHARACTERISTIC POLYNOMIALAccepted · 5 Sep 2026

The Heron–
Rota–Welsh theorem

Take the absolute values of the characteristic polynomial’s coefficients. These too form a log-concave sequence.

ck+1 2≥ck ck+2c_{k+1}^{\,2} \ge c_k\,c_{k+2}
Flat incidences · Reverse Cauchy–SchwarzRead the proof

WHY MATROIDS?

Independence,
in the abstract.

Linearly independent vectors and forests in a graph obey the same exchange principle. A matroid captures that principle without requiring vectors or a graph.

These theorems show that its counting sequences have a remarkable amount of structure. Their proofs connect finite combinatorics with ideas from geometry and quadratic forms.

Start with the mathematical background ↗

FROM STATEMENT TO SOURCE

A readable guide
to a checkable proof.

The writeup explains the statements and the arguments used by the accepted Lean code. Every major step links to a declaration in a fixed source snapshot.

Read online ↗Download PDF ↓
  1. 01

    The mathematical statement

    Definitions, normalizations, and boundary cases.

  2. 02

    The argument in Lean

    A guided route through the decisive lemmas.

  3. 03

    The verification record

    Accepted artifacts, source hashes, and comparator results.

CITE THIS COMPANION

Built on the mathematics.

The original theorems and their authors are credited in each writeup. This citation identifies the formalization companion.

@misc{axiom-matroid-log-concavity,
  author = {{Axiom Math}},
  title = {Matroid Log-Concavity in Lean},
  year = {2026},
  url = {https://matroids.axiommath.ai},
  note = {Companion to two accepted formalizations}
}