Source and verification
This article explains family 188 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.
🏷️ Random triangle removal
Start from . At each step choose uniformly from the triangles whose three edges remain and delete those edges. Stop when the graph is triangle-free. The removed triangles are edge-disjoint, and the remaining edges form the leave. Let be its size.
This is a random greedy triangle packing. It does not choose a maximum packing, and the terminal graph need not have the smallest possible number of edges among all triangle-free remainders.
Manuscript claim
The normalized leave converges in mean square:
Consequently, the same normalization converges in probability, and . (OpenAI, 2026)
The theorem concerns the complete-graph starting state. It asserts neither a fluctuation law nor the same constant for arbitrary initial graphs or general hypergraph-removal processes.
🏷️ What mean-square convergence adds
If and , Markov’s inequality gives
Cauchy–Schwarz similarly gives . Thus the probability and expectation conclusions follow directly from the stronger moment statement.
Convergence in probability alone would not justify the expectation conclusion without a tail argument. This distinction is particularly relevant because the unnormalized leave can range up to order .
🏷️ Stopping at a controlled prefix
The proof first stops at a deterministic time when edge density is approximately for a small fixed . Existing early-process estimates supply a graph with roughly
triangles through each edge, with suitable uniform count and error controls. This early-prefix theorem is an external input; the source proves the subsequent continuation estimates.
The process is then represented by assigning fresh independent uniform priorities to remaining triangles and scanning them in order, accepting a triangle precisely when all its edges are still present. Removing edges can only destroy available triangles, so this random priority order produces the same continuation law as successive uniform choices among available triangles.
🏷️ A branching survival equation
To determine whether an edge survives until priority , examine triangles containing it. A triangle removes the edge only if its other two edges survive until the triangle’s priority. This gives a recursive backward query.
An auxiliary unfolding treats different occurrences of triangle types as independent. Its scalar comparison law is
It solves with . The cubic factor records the survival of an edge together with its two potential partners in the simplified branching model.
At , the predicted leave is
This calculation explains the constant. It is not by itself a proof: the real graph has repeated triangle types and dependent recursive queries, and the effective time tends to infinity.
🏷️ Stability beyond a fixed time window
The independent unfolding satisfies product equations. To compare them uniformly with , the manuscript controls a matrix acting on the surviving edges. Cycle counts inside vertex links show that normalized link matrices are close to averaging projections.
The sum of these projections has a controlled semigroup in maximum norm. A finite perturbation expansion transfers that stability to the actual link matrices. Maximum-norm control is needed to keep the approximation uniform over individual edge queries throughout the growing time interval.
A local approximation valid only at fixed rescaled time would not reach the terminal estimate. Nor would an average spectral estimate alone provide the required uniform survival bounds.
🏷️ Two-root errors at the correct scale
The second moment requires joint survival of two root edges. Their other-edge tests use one jointly ordered candidate list. This ordering controls which recursive calls are actually visited; counting all potential calls would overestimate collisions.
A repeated triangle type forces an additional graph edge in the union of at most two ancestral query paths. Rooted-template counts bound the number of these witnesses, while joint priority ordering bounds their visitation probabilities.
The source obtains absolute error . This is the relevant scale because the two-root survival probability is itself of order . An error merely tending to zero would be too large after summing over edge pairs and normalizing the second moment.
Finally, the estimates are uniform over good prefix graphs, and the prefix failure probability is small enough to control its contribution to the second moment. This closes the passage from the branching constant to the claimed unconditional limit.
🏷️ Key steps and proof outlines
Couple the actual execution, including candidates never traversed
A triangle type is a particular triangle of the good prefix graph. An occurrence is one appearance of that type in a recursive unfolding. The finite process shares one priority between all occurrences of a type; the independent model assigns each occurrence a fresh priority. Distinguishing these objects identifies the only possible source of coupling failure. (OpenAI, 2026)
Expose the entire candidate list at every visited call before sorting it. This includes candidates above the call’s threshold and candidates never traversed because an earlier test terminates the search. At the first exposure of a type , use its finite priority in both experiments. At each repeated exposure, give the independent unfolding a fresh uniform variable.
Why does this still produce independent occurrence priorities despite adaptive queries? Conditional on the execution history, every previously unexposed is still independent and uniform: the next type is determined by the graph, root labels, and already exposed information. Induction over exposures proves the asserted law. Until a type repeats, the sorted lists, recursive calls, answers, and stopping decisions agree exactly.
If is the repetition event for roots, the coupling bounds the difference in the probability of any event concerning the root answers by . Counting only traversed repetitions would miss a way that the two sorted candidate lists can already disagree.
A repeated type creates an extra edge on two ancestral paths
Build a formal graph from the visited calls. Each root begins with its own formal edge. A child reached through edge introduces a new vertex and the edges , retaining . Distinct formal vertices may later receive the same actual graph label, but every individual gluing triangle has three distinct labels.
The construction has two crucial invariants: no step joins two already existing formal vertices, and every formal triangle is one of the gluing triangles. Also, an edge is focused only at its birth call, and a child omits its parent triangle from its candidates.
Suppose first that all labels are distinct. If a type appears in two candidate lists, two different focus edges represent two edges of the same actual triangle. Unless an additional actual edge joins formally nonadjacent vertices, those three vertices form a formal gluing triangle. But the birth-and-parent rules let that triangle appear in at most one candidate list, a contradiction.
If labels repeat, consider the first repetition. Its two attachment edges either expose the same additional adjacency among earlier vertices or force a forbidden reuse of an earlier gluing triangle. Thus a collision has a witness consisting of an extra actual edge supported on the union of at most two ancestral paths. Repeated root labels contribute a separate error. The rooted-template estimates and ordered visitation probabilities can now be applied to these small witnesses instead of the entire potential recursion tree.
Match the error scale to the second moment
Uniformly over good prefix graphs, the source obtains
for the finite-versus-independent root-answer discrepancy. Since the predicted one-root survival probability is , the decisive comparison is
It controls relative two-root error; absolute error alone would not suffice.
Sample the roots independently with replacement from the prefix edges. Conditional on the terminal graph, the probability all survive is exactly , including coincident samples. In the independent unfolding the root trees are independent even if their labels coincide, so the corresponding probability is the th power of the average unfolding survival probability. Uniform stability of that probability gives, for ,
Subtract twice the first identity from the second and add one to obtain conditional mean-square convergence. Removing repeated root samples would change the second-moment identity and require an extra correction.
Remove the conditioning with a quantitative tail budget
The deterministic normalization satisfies
On an arbitrary bad prefix, the elementary bound gives . Therefore the bad-prefix contribution is at most , using the quantitative prefix theorem. On good prefixes, the conditional estimates are uniform. This final tail calculation is what upgrades the branching prediction to the claimed unconditional mean-square limit. The coupling and moments sections provide these steps; the independent-unfolding stability estimate remains a separate necessary analytic input.
See Also
- Cycle-and-edge decompositions concerns deterministic partitions of every edge, unlike the random process’s triangle-free leave.
- Ordered matrix removal uses “removal” in the different sense of edit distance to a forbidden-pattern property.
🏷️ Manuscripts and verification scope
- The sharp terminal leave in random triangle removal — pinned manuscript and companion source.
The family scope page describes selected formalization coverage. The page selects mean-square convergence and its probability and expectation consequences for removal from the complete graph. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.
OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.