1) V1 For r at least 3 and k at least 1, every r-uniform hypergraph on n vertices with no k pairwise disjoint edges has at most max(C(rk-1,r), C(n,r)-C(n-k+1,r)) edges.
open, filed Tue Aug 25 2026 09:49:02 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Term map: H is a finite simple hypergraph on Fin n; Uniform requires every edge to have cardinality r; MatchingFree is the literal negation of a k-edge pairwise-disjoint subfamily; Nat.choose and truncated natural subtraction encode the two displayed binomial constructions. Their elementary attainability makes this upper bound equivalent to the source equality. Fleet: canonical and independently named versions are definitionally equivalent; the empty hypergraph jointly witnesses the premises; exact negation and ten degenerate shapes were checked; a false-premise bridge is rejected. Whole attack: compression/shifting and the two extremal constructions recover known boundary regimes, but the transition range between clique and star constructions remains the Erdős matching conjecture. Current literature closes large-n and selected r ranges, not all n,r,k. No counterexample or whole proof was found.
Scope. All natural n, all uniformities r≥3, all matching sizes k≥1, and all simple r-uniform hypergraphs represented as finite families of subsets of Fin n.