The sharp constant for the terminal leave of random triangle removal (triangle case of the Joos-Kühn conjecture)
Start from and repeatedly delete the three edges of a uniformly random remaining triangle until none is left; let be the number of edges remaining. Bollobas and Erdos conjectured (1990) that has order ; after work of Spencer, Rodl-Thoma and Grable, Bohman, Frieze and Lubetzky proved with high probability (2015). Joos and Kuhn (2024) studied removal of a general strictly balanced hypergraph and conjectured (Conjecture 16.2) an asymptotic constant for the terminal leave, whose triangle case predicts in probability. Is that so?
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Random graph processes; random greedy packing
- Posed by
- Felix Joos and Marcus Kühn (Conjecture 16.2 of The hypergraph removal process); order of magnitude conjectured by Bollobás and Erdős (1990)
- Year posed
- 2024
- Years open
- 2y
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 22 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: for uniform triangle removal from , ; hence in probability and . The paper says it does not give the sharp constant for other starting graphs, for general hypergraph removal (the rest of Joos-Kuhn Conjecture 16.2), or a fluctuation law.
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region whose write-up was human-edited). The manuscripts are authored 'OpenAI' and name no human author. Single manuscript dated September 25, 2026. It states that its only external proof input is Joos and Kuhn's early-prefix control; all continuation estimates are proved in the paper.
Verification
No independent mathematician has checked this yet. Checked here: introduction and Theorem 1.1 read against the triangle case of Joos-Kuhn Conjecture 16.2 as the paper states it. Lean: the challenge lean/ComparatorChallenges/TriangleRemoval.json (solution_module OAI.Combinatorics.TriangleRemoval.Main, present at the pinned commit) is not in the formalization catalogue lean/formalization.yaml. The statement OAI.SharpTerminalLeave.sharp_terminal_leave was read here: it defines the process as a PMF on edge sets run for steps from and asserts convergence of to , convergence in probability and convergence of the normalized mean. That is the headline. Not rebuilt here. Entry is partial because the conjecture covers general strictly balanced hypergraphs.