View source for The sharp constant in random triangle removal

The '''random triangle removal process''' starts from the complete graph ''K''<sub>''n''</sub> 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 ([https://github.com/openai/math 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 ''n''<sup>3/2</sup>. Spencer, and independently Rödl and Thoma, showed that the leave is ''o''(''n''<sup>2</sup>) with high probability; Grable proved bounds ''O''(''n''<sup>11/6+ξ</sup>) and outlined ''O''(''n''<sup>7/4+ξ</sup>); Bohman, Frieze and Lubetzky proved ''O''(''n''<sup>7/4</sup> log<sup>5/4</sup> ''n'') and later that the leave is ''n''<sup>3/2+o(1)</sup> with high probability.
* Joos and Kühn (''The hypergraph removal process'', [https://arxiv.org/abs/2412.15039v2 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 ''F''<sub>''n''</sub> be the number of edges of the terminal graph of uniform triangle removal from ''K''<sub>''n''</sub>. Then ''F''<sub>''n''</sub>/''n''<sup>3/2</sup> 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.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-Sharp-Terminal-Leave-in-Random-Triangle-Removal-September-25-2026 ''The sharp terminal leave in random triangle removal''] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/188.md lean/docs/188.md] states that the formalization proves the ''L''<sup>2</sup> 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 <code>TriangleRemoval.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family's challenge <code>TriangleRemoval</code> "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'', [https://arxiv.org/abs/2610.20414v1 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 ''L''<sup>2</sup>, 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.

[[Category:OpenAI results]]