The Erdos-Lovasz Cover Number Problem
Let be the fewest edges in an -uniform intersecting hypergraph with cover number . Erdos and Lovasz proved . An elementary argument gives , and building on it with Kahn's small-codegree edge-colouring theorem pushes the bound further.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Extremal combinatorics
- Posed by
- Paul Erdos, Laszlo Lovasz
- Year posed
- 1975
- Years open
- 51y
- Solved
- 2026-06-23
- Model
- ChatGPT 5.5 Pro, Aristotle
- Vendor
- OpenAI / Harmonic
- Collaborators
- Varun Sivashankar
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
an improved lower bound; the true order of g(r) remains open
What the AI did
The acknowledgement states the proof was discovered with the help of ChatGPT 5.5 Pro, and that Theorem 1 was then formalized in Lean with Harmonic's Aristotle.
Verification
The Lean formalization is partial by the author's own account: part (i) of Theorem 1 is formalized in full and part (ii) only conditional on Kahn's theorem. We have not compiled it. arXiv preprint, not peer-reviewed.
Source
arXiv:2606.24878 - An Improved Lower Bound for the Erdos-Lovasz Cover Number Problem