Prove TriangleRemoval (openai/math family 188: The sharp constant in random triangle removal) in Lean 4 with…
Prove TriangleRemoval (openai/math family 188: The sharp constant in random triangle removal) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 188 of the release, The sharp constant in random triangle removal (Combinatorics)…
The task
Context: this statement belongs to family 188 of the release, *The sharp constant in random triangle removal* (Combinatorics). The family as a whole: 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)$,…
Part of raising-heart/openai-math.