The sharp constant in random triangle removal
The random triangle removal process starts from the complete graph Kn and repeatedly deletes the three edges of a uniformly chosen remaining triangle until no triangle is left. The question is the size of the terminal graph (the leave), including its leading constant. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the sharp constant. This page summarizes the published claim and lists publicly available follow-up work.
Background
- According to the manuscript's introduction, Bollobás and Erdős conjectured in 1990 that the expected leave has order n3/2. Spencer, and independently Rödl and Thoma, showed that the leave is o(n2) with high probability; Grable proved bounds O(n11/6+ξ) and outlined O(n7/4+ξ); Bohman, Frieze and Lubetzky proved O(n7/4 log5/4 n) and later that the leave is n3/2+o(1) with high probability.
- Joos and Kühn (The hypergraph removal process, arXiv:2412.15039v2) developed removal estimates for strictly balanced hypergraphs. Their Conjecture 16.2 predicts an asymptotic constant for the terminal leave; for triangles it is 1/(2√2).
The original result
- Claim. Let Fn be the number of edges of the terminal graph of uniform triangle removal from Kn. Then Fn/n3/2 converges to 1/(2√2) in mean square (Theorem 1.1), hence also in probability. The manuscript describes this as the triangle case of the Joos–Kühn conjecture.
- Source. The sharp terminal leave in random triangle removal in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/188.md states that the formalization proves the L2 convergence of the normalized terminal edge count to 1/(2√2), and also states convergence in probability and convergence of the normalized expectation. The Comparator statement is
TriangleRemoval.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 16 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family's challenge TriangleRemoval "full" and records a sandboxed Comparator pass. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-15 (listed) | P. Keevash, The terminal leave in random greedy hypergraph matching, arXiv:2610.20414v1 | Independent proof of the same result, with a generalization; public statement on priority | Proves that the normalized terminal edge count converges to 1/(2√2) in L2, and the analogous result for every fixed strictly k-balanced k-graph, from a general theorem on random greedy matchings in nearly regular hypergraphs. The introduction states that the author shared his ideas on the problem with ChatGPT from October 2025, and that his solution "(when specialised to triangles) was essentially the same as that in the recent OpenAI sharing progress in mathematics announcement (manuscript 188)". It continues: "it is plausible that training on my conversations helped the OpenAI model solve the problem, although I have no direct evidence that this occurred", and asks for "clarification from OpenAI about whether their model used my work and how they propose to handle questions of intellectual priority and acknowledgement". | arXiv preprint (version 1). |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim. This page reports the statements of the cited sources and takes no position on the priority question.