oai-math-revised beta

Browse › Combinatorics › 188 The sharp terminal leave in random triangle removal

The sharp terminal leave in random triangle removal

OpenAI · September 25, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

Starting from the complete graph on n vertices, repeatedly remove the three edges of a uniformly chosen remaining triangle. We prove that the number of edges left at termination, divided by n3/2, converges in L2 to $1/(2\sqrt2)$. This proves the triangle case of the sharp-constant conjecture of Joos and Kühn. In particular, the same limit holds in probability and for the normalized expectation.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • Peter Keevash, The terminal leave in random greedy hypergraph matching (arXiv:2610.20414, 14 Oct 2026). Proves that the edge count of the terminal graph of random triangle removal from $K_n$, divided by $n^{3/2}$, converges in $L^2$ to $1/(2\sqrt2)$, the same statement as Theorem 1.1 here, and extends it to any fixed strictly $k$-balanced $k$-graph; its §2 gives a triangle-case exposition of the approach (freezing the process, tree survival prediction, comparison with the finite random matching).

Comments and discussion

Formalization

  • OpenAI math release, Lean scope note 188 (release repository, 2026-10-06). The scope note says the Lean formalization proves the $L^2$ convergence of $F_n/n^{3/2}$ to $1/(2\sqrt2)$, also states convergence in probability and of the normalized expectation, and links the comparator statement TriangleRemoval.lean. [AI-generated per source]
  • OpenAI, lean/OAI/Combinatorics/TriangleRemoval/Main.lean (openai/math, commit adc7f12, Oct 2026). The top-level Lean file states sharp_terminal_leave_l2, sharp_terminal_leave_probability, sharp_terminal_leave_expectation and their conjunction sharp_terminal_leave in namespace OAI.SharpTerminalLeave.
  • google-deepmind/formal-conjectures, Issue #1984: Erdős Problem 1155 (opened 1 Feb 2026). An open request to formalize the statement of the Bollobás–Erdős random triangle-removal problem, with an unmerged related PR #3587 whose opaque declarations a reviewer noted are not tied to the actual process; it does not mention this paper.
  • Felix Joos and Marcus Kühn, The hypergraph removal process (arXiv:2412.15039v2, 2025-08-03). Keevash's follow-up cites this work for approximate terminal exponents and estimates used before the final stage, complementing the release manuscript's use of its early-prefix control and sharp-constant conjecture.

Possibly relevant literature (found by the agent, not checked)

  • Erdős Problems, Problem #1155 (erdosproblems.com, last edited 25 Jan 2026). Records the Bollobás–Erdős question of whether $\mathbb E f(n)\asymp n^{3/2}$ for the leave of random triangle removal, on which the paper's statement $\mathbb E F_n/n^{3/2}\to1/(2\sqrt2)$ bears directly; the entry does not mention the paper.

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:The-Sharp-Terminal-Leave-in-Random-Triangle-Removal-September-25-2026,
  author = {{OpenAI}},
  title = {{The sharp terminal leave in random triangle removal}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Sharp-Terminal-Leave-in-Random-Triangle-Removal-September-25-2026/The-Sharp-Terminal-Leave-in-Random-Triangle-Removal-September-25-2026.pdf}{OAI:The-Sharp-Terminal-Leave-in-Random-Triangle-Removal-September-25-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/188.md. The Lean statements have not been checked by people against the paper's claims.

Family 188: The sharp terminal leave in random triangle removal

Starting from the complete graph on n vertices, repeatedly delete a uniformly chosen remaining triangle. The terminal edge count is asymptotic to $n^{3/2}/(2\sqrt2)$, with mean-square convergence after normalization by n3/2. This proves the triangle case of the Joos–Kühn sharp-constant conjecture.

This is the only paper in this family.