M(7,3)=29 certified in Lean 4 via SAT+LRAT

Stream: mathlib4

[Cody]

Hi all, I'm Cody.

I've been formalizing exact values of M(n,3), the maximum size of a 3-sunflower-free family on [n].

https://www.erdosproblems.com/857

M(7,3) = 29 is certified via SAT+LRAT bridge — 4 independent solvers (CaDiCaL, Glucose4, MapleSAT, Lingeling) all returned UNSAT at target 30. The Lean proof is sorry-free.

Exact values for n=1–6 are also fully verified via native_decide and LRAT.

I'm also working on Erdős Problem 20: https://www.erdosproblems.com/20 (uniform sunflower conjecture) — base cases f(1,3)–f(6,3) are proved, general bound is open.

Repo: https://github.com/SproutSeeds/sunflower-lean

Happy to discuss the SAT encoding, the LRAT bridge approach, or the Erdős 20 framework. Also open to collaborations or formalization commissions if anyone has results they'd like verified.

The SAT+LRAT verification pipeline in SATBridge.lean is designed to be reusable for other combinatorics certification problems.

---

update
Also posted in #maths > M(7,3)=29 certified in Lean 4 via SAT+LRAT for better channel fit.