Math and TheoryExact three-uniform Berge-path saturation numbers and a counterexample to a conjectured formula
Problem and result
- Problem
- Berge-path saturation conjecture (English–Graber–Kirkpatrick–Methuku–Sullivan, Conjecture 2.4)
- Posed in
- English, Graber, Kirkpatrick, Methuku and Sullivan, Saturation of Berge hypergraphs, arXiv:1710.03735v1, Conjecture 2.4
- Status
- Disproved for three-uniform hypergraphs; exact formula given
- Result
- Two loose 8-cycles plus two isolated vertices give a Berge-P₁₀-saturated 3-graph on 34 vertices with 16 edges, not 17; the exact 3-uniform formula holds for all m ≥ 10, n ≥ 2a_m + 1.
Abstract
English, Graber, Kirkpatrick, Methuku and Sullivan conjectured that the three-uniform Berge-P_m saturation number is ⌈(n − ⌊n/b⌋)/2⌉ for all m ≥ 10 and n ≥ b = 2a_m + 1. Two disjoint loose 8-cycles with two isolated vertices form a Berge-P₁₀-saturated hypergraph on 34 vertices with 16 hyperedges, one below the conjectured 17. The preprint determines the saturation number on the whole conjectured range: it is one less than the conjectured value exactly when b < n < 2b and n ≡ 2 (mod 2(m − 2)), and the extremal hypergraph at those orders is unique.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Extremal hypergraph theory
- Subject
- Graph theory and graph polynomials
- Result type
- Counterexample to a published conjecture and exact formula with reproducible proof package
- Formal proof
- Standalone Lean package
- Family
berge-path-saturation- Keywords
- Berge hypergraphs, Berge paths, saturation numbers, three-uniform hypergraphs, loose cycles, isolated vertices, extremal hypergraph theory
Statement and scope
Formal scope. Lean 4.35.0 proves, for actual three-uniform hypergraphs, Berge paths and saturation under every absent triple, that t disjoint loose d-cycles with two isolated vertices are Berge-P_{d+2}-saturated for every d ≥ 3, that the explicit 34-vertex hypergraph is Berge-P₁₀-saturated with 16 hyperedges, and that the three-uniform case of the conjecture fails for every m ≥ 10. The matching lower bound, the exact formula and the uniqueness of extremal hypergraphs have conventional proofs that use two results of the source paper.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf283 KB- PDF on GitHub
papers/mathematics/ berge-path-saturation/ manuscript.pdf - LaTeX source
papers/mathematics/ berge-path-saturation/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ berge-path-saturation/ - Lean project
papers/5 Lean filesmathematics/ berge-path-saturation/ lean/ - Lakefile
papers/mathematics/ berge-path-saturation/ lean/ lakefile.toml - Toolchain
leanprover/lean4:v4.35.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
bash scripts/verify.sh /tmp/berge-path-verification- README
papers/mathematics/ berge-path-saturation/ README.md - Verification guide
papers/mathematics/ berge-path-saturation/ verification/ README.md - Verification record
papers/mathematics/ berge-path-saturation/ VERIFICATION.md - Authorship
papers/mathematics/ berge-path-saturation/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Prior work. English, Graber, Kirkpatrick, Methuku and Sullivan, arXiv:1710.03735v1, Conjecture 2.4.
Questions and answers
Is the conjectured saturation number of Berge paths correct?
Not for three-uniform hypergraphs. For m = 10 the conjecture predicts 17 hyperedges at n = 34, but two disjoint loose 8-cycles with two isolated vertices are Berge-P₁₀-saturated with 16. For every m ≥ 10 the conjecture fails exactly at the orders n = 2t(m − 2) + 2 with b < n < 2b, where b = 2a_m + 1.
What is the exact three-uniform Berge-path saturation number?
For m ≥ 10 and n ≥ b it equals ⌈(n − ⌊n/b⌋)/2⌉ minus one at the exceptional orders and equals ⌈(n − ⌊n/b⌋)/2⌉ otherwise; at each exceptional order the unique extremal hypergraph is a disjoint union of loose (m − 2)-cycles with two isolated vertices. The lower bound uses the source paper's tree-size theorem and upper construction. Uniformities above three and n < b are not addressed.
Is the result formally verified?
Partly. Lean 4 proves that the loose-cycle hypergraphs are saturated for every cycle length, that the explicit 34-vertex hypergraph is saturated with 16 hyperedges, and that the three-uniform conjecture fails for every m ≥ 10. The matching lower bound and uniqueness have conventional proofs.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026bergepathsaturation,
author = {Goyal, Dev D.},
title = {Exact Three-Uniform {Berge}-Path Saturation Numbers and a Counterexample to a Conjectured Formula},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/berge-path-saturation}
}