VibeMathedMath problems solved with AI
Sign in

Erdős matching conjecture: the four-uniform case

Erdős problem #1020 · erdosproblems.com/1020

Let r≥2r\geq2, s≥1s\geq1 and n≥r(s+1)n\geq r(s+1) be integers. If F⊆([n]r)\mathcal F\subseteq\binom{[n]}r contains no s+1s+1 pairwise disjoint members, must
∣F∣≤max⁡{(r(s+1)−1r),(nr)−(n−sr)}? |\mathcal F|\leq\max\left\{\binom{r(s+1)-1}{r},\binom nr-\binom{n-s}{r}\right\}?
The two candidate extremal families are all rr-sets inside an (r(s+1)−1)(r(s+1)-1)-set and all rr-sets meeting a fixed ss-set. This is the Erdős matching conjecture (1965), recorded as Problem #1020. This entry concerns only the four-uniform specialization, r=4r=4; it does not claim to settle arbitrary uniformity. The tracker's forbidden matching parameter is k=s+1k=s+1.

Result
Proved(see note)
Status
Partial result
AI contribution
AI-assisted
Method
Computation
Field
Extremal set theory and hypergraph matchings
Posed by
Paul Erdős, A problem on independent r-tuples (1965); Erdős Problem #1020
Year posed
1965
Years open
61y
Solved
2026-09
Model
GPT-5.6 Sol; Astra; GPT-5 Pro; GPT-6 Pro
Vendor
OpenAI
Collaborators
—
Verification
Unreviewed
Publication
Announced
Significance
40 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For r=4r=4, the manuscript claims the sharp extremal value
max⁡{(4s+34),(n4)−(n−s4)} \max\left\{\binom{4s+3}{4},\binom n4-\binom{n-s}{4}\right\}
for every s≥1s\geq1 and n≥4s+4n\geq4s+4. Both terms are attained by the standard clique and cover constructions. The claimed advance is an all-parameter four-uniform theorem, extending the sufficiently-large matching-number range of Hou–Hu–Liu (s≥6961s\geq6961) while retaining and crediting their framework and eight computations. The proof combines finite exact certificates and exhaustive searches with a written combinatorial reduction and analytic propagation.

Additional equality and stability conclusions have restricted domains; no classification of every extremizer or arbitrary-family stability is claimed. This is a claimed complete r=4 result and a partial result toward the general Erdős matching conjecture. Uniformity five and arbitrary uniformity are not settled by this paper.

What the AI did

The author reports using GPT-5.6 Sol, Astra, GPT-5 Pro and GPT-6 Pro through ChatGPT. Under the author's direction, AI systems explored proof approaches, proposed lemmas and counterchecks, developed exact certificates and verification code, drafted and revised the manuscript, and conducted adversarial reviews. The public manuscript explicitly discloses scientific and computational assistance, beyond language editing. The model names are supplied by the author; the manuscript does not identify their versions or assign individual results to particular models. AI-assisted is the conservative classification on this disclosure. The author selected the research scope and is responsible for the final claims. Reviews within this workflow are not independent expert verification.

Verification

Checked here on 13 September 2026, at the sources rather than from the submission. erdosproblems.com/1020 carries the conjecture in the form stated and still marks it open; the tracker's forbidden-matching parameter is kk where this entry uses s+1s+1, and substituting turns one formula into the other, so the transcription is faithful. Hou, Hu and Liu (arXiv:2605.26060) state in their abstract "We prove the 4-uniform Erdos Matching Conjecture for every matching number s≥6961s\ge 6961", so the standing state of the four-uniform case really was all sufficiently large ss, and the claimed advance - closing the remaining finite range - is well defined.

The mathematics was not checked. The author's own audit of 12 September records replay of all 27 computational obligations including the eight retained Hou-Hu-Liu searches, 52 tests, 12 receipt-integrity mutation controls, a matching PDF rebuild and an anonymous clone matching all 97 reviewed files. That supports reproducibility and the declared finite computations; it does not validate the written reduction and induction, and no independent domain expert endorsement or formal proof is supplied. Announcement reflects repository-only publication.

Sources

Submitted by Oleksiy Babanskyy on

Changelog2 changes

Discussion