The uniform Turán density of the tetrahedron
The uniform Turán density of a 3-uniform hypergraph is the smallest such that every sufficiently large hypergraph in which all linear-sized subsets induce density above contains . Erdős and Sós asked in the 1982 paper that founded the subject for the value of , the complete 3-graph on four vertices, and for . The second was settled at in 2018 by Glebov, Kráľ and Volec; the tetrahedron itself resisted for forty-four years, with the conjectured value from a known lower-bound construction. What is ?
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Extremal hypergraph theory
- Posed by
- Paul Erdős and Vera T. Sós, in the 1982 paper that introduced uniform Turán densities
- Year posed
- 1982
- Years open
- 44y
- Solved
- 2026-09-10
- Model
- ChatGPT 6 Pro; Aristotle
- Vendor
- OpenAI; Harmonic
- Collaborators
- Matija Bucić
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 48 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
, matching the long-known lower-bound construction. The AI contribution is one identity inside the argument rather than the argument, which is why this is recorded as AI-assisted; it is included in the catalog because the identity is a step of the proof, not a matter of exposition.
What the AI did
From the paper's declaration of AI use: identity (6) in the proof was found by ChatGPT 6 Pro, after an early draft containing the author's ideas was uploaded to it. Separately, the paper relies on a computational verifier; besides the author hand-checking that verifier's correctness, Aristotle was used to check it in Lean and to run a separate audit. The mathematical frame, the reduction and the write-up are the author's; the model supplied one identity inside it.
Verification
Checked here on 22 September 2026 against arXiv:2609.11802: the abstract states the value and that it answers a question of Erdős and Sós from the founding 1982 paper, and the introduction names that paper and the companion question about . The AI declaration is quoted as written. The mathematics was not checked here. Aristotle's Lean check covers the computational verifier used inside the proof, not the proof as a whole, so this is not a formalisation of the theorem and the entry does not claim one. Twelve days old, no referee.