∑math20

Combinatorics · Result 188

The sharp terminal leave in random triangle removal

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The sharp terminal leave in random triangle removal

The sharp terminal leave in random triangle removal

OpenAI · September 25, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

Start with the complete graph on \(n\) vertices and repeatedly delete the three edges of a uniformly chosen remaining triangle. The formalization proves that the number of edges at termination, divided by \(n^{3/2}\), converges in \(L^2\) to \(1/(2\sqrt2)\). It also states convergence in probability and convergence of the normalized expectation to the same constant. This is the triangle case of the sharp terminal-leave conjecture of Joos and Kühn.

Comparator links

ResultComparator statement
Sharp terminal edge count in random triangle removalTriangleRemoval.lean

Scope note on GitHub →