---

The claim. The manuscript The sharp terminal leave in random triangle removal of the OpenAI mathematics release, dated 25 September 2026 and authored by OpenAI (its intake card is openai_2026_sharp_terminal_leave_random_triangle_removal, and its main result is paged at Theorem 1.1), states in its Theorem 1.1 that for the process of Problem 1155, which starts from $K_n$ and repeatedly deletes the three edges of a uniformly chosen remaining triangle until no triangle is left, the number $F_n$ of edges of the terminal triangle-free graph (the problem's $f(n)$) satisfies

$$\mathbb E\left[\left(\frac{F_n}{n^{3/2}}-\frac1{2\sqrt2}\right)^2\right] \longrightarrow0,$$

so that $F_n/n^{3/2}\to1/(2\sqrt2)$ in probability and $\mathbb EF_n/n^{3/2}\to1/(2\sqrt2)$. The manuscript presents this as the triangle case of the sharp terminal-leave conjecture of Joos and Kühn (Conjecture 16.2 of The hypergraph removal process, arXiv:2412.15039, version 2), in the stronger $L^2$ form, and says that its only external proof input is the early-prefix control of Joos and Kühn, used through its Proposition 2.2. By its introduction, the argument runs the process to a deterministic step where the edge density is $n^{-1/2+1/2000}$, represents the continuation by independent uniform priorities on the remaining triangles, compares the survival probability of an edge with Spencer's scalar law $(1+2Dt)^{-1/2}$ through a semigroup bound for the edge-adjacency matrix of the triangle hypergraph, and couples one- and two-edge survival queries to an independent unfolding whose collision probability is small enough to give the first two moments of $F_n$. Read depth: the statement and the statements of its main inputs, clause by clause in the release's TeX source; the proof for structure only, with no step checked.

Covers. The two displayed questions, in sharper form: $\mathbb Ef(n)\sim n^{3/2}/(2\sqrt2)$, so $\mathbb Ef(n)\asymp n^{3/2}$, and $f(n)/n^{3/2}\to1/(2\sqrt2)$ in probability, so $f(n)\ll n^{3/2}$ with probability tending to one, the reading of the problem's "almost surely" stated on the problem page. Not covered: the problem's first request, to describe the typical parameters and structure of the terminal graph; the manuscript asserts no fluctuation law for $F_n$ and no result for other starting graphs.

The formalization. The release's Lean tree at the pinned revision states the theorem in lean/ComparatorChallenges/TriangleRemoval.lean as OAI.SharpTerminalLeave.sharp_terminal_leave (body sorry, the challenge form), a conjunction of the three limits: a graph is a finite set of finite subsets of Fin n, started from the set of all two-element subsets, one step chooses a remaining triangle uniformly and removes its three edges (and does nothing once no triangle remains), the terminal law is $\binom n2$ steps from the complete graph, the normalized leave is the edge count over $n^{3/2}$, and the constant is $1/(2\sqrt2)$. The solution module lean/OAI/Combinatorics/TriangleRemoval/Main.lean proves a declaration of the same name from three named limits (sharp_terminal_leave_l2, sharp_terminal_leave_probability, sharp_terminal_leave_expectation); the release's own catalog lean/formalization.yaml does not list the manuscript, while its page lean/docs/188.md describes the formalization's scope and the comparator sidecar lean/ComparatorChallenges/TriangleRemoval.json permits only propext, Classical.choice and Quot.sound. The build and the statement audit are recorded in the Acceptance paragraph below.

Acceptance. Formalized, as a partial claim. This corpus's verification built OAI.SharpTerminalLeave.sharp_terminal_leave at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked its axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the comparator challenge lean/ComparatorChallenges/TriangleRemoval.lean pins the declaration with its model of the process, and its fingerprint was found identical to the challenge. A statement audit unfolded every definition to Mathlib and found that the model is the process of the problem: the complete graph is the set of all two-element subsets of Fin n, a step draws a remaining triangle from the uniform distribution and removes exactly its three edges, and a triangle-free graph is left fixed; each real step removes three of the $\binom n2$ edges, so the law after $\binom n2$ steps is the law of the terminal graph. Expectation and probability are finite sums against that distribution, the normalization is the real power $n^{3/2}$, and the three conjuncts are exactly the $L^2$ limit, the convergence in probability for every $\varepsilon>0$ and the limit of the mean displayed above, with no hypotheses and nothing vacuous. The declaration certifies the manuscript's Theorem 1.1 in full. It gives $\mathbb Ef(n)\sim n^{3/2}/(2\sqrt2)$, so $\mathbb Ef(n)\asymp n^{3/2}$ for large $n$, and $\mathbb P(f(n)\le Cn^{3/2})\to1$ for every $C>1/(2\sqrt2)$, which answer both displayed questions under the problem page's reading of "almost surely" as with probability tending to one. The scope stays partial because the problem's request to describe the typical parameters and structure of the terminal graph is not addressed; being partial, the claim leaves the problem open. Not reviewed: the manuscript is a release preprint with no journal record, no arXiv version and no independent review, and the release's README says its manuscripts were produced by an internal OpenAI model and stand at different stages of verification, not all with Lean formalizations; the claimant is the organization.

Depends on. No page of this wiki. The result of Bohman, Frieze and Lubetzky recorded on the problem page is prior work, which the manuscript cites but does not use as a proof input.