Erdős Problem 1155

### What is the conjecture

Start with the complete graph $K_n$ on $n$ vertices. Repeatedly select a uniformly random triangle and delete all three of its edges, continuing until the graph is triangle-free. Let $f(n)$ denote the random variable representing the number of edges remaining in the final triangle-free graph.

**Main conjectures:**
1. Does $\mathbb{E}[f(n)] \approx n^{3/2}$?
2. Is it true that $f(n) \ll n^{3/2}$ almost surely?

The problem asks for a characterization of the typical structure and edge count of the resulting triangle-free graph generated by this random deletion process.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1155, Bollobás and Erdős (1990) Quo Vadis, Graph Theory?, Grable, D. A. (1997) "A large deviation result for graphs," Bohman, T., Frieze, A., & Lubetzky, E. (2015) "Random triangle removal," Annals of Mathematics

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Real analysis (exponents, asymptotic notation) — standard in Mathlib
- Probability theory (expectation, almost sure events) — in Mathlib
- Finsets and Set operations — standard in Mathlib

Missing pieces (exactly 2; unclear/absent from search results):
- Graph data structure and triangle detection in a formal framework
- Formal semantics for the random triangle-deletion process and its probability distribution

Rating justification (1-2 sentences): Mathlib lacks a formalized graph library with triangle enumeration and random process mechanics. While the statement involves standard probabilistic concepts, defining the graph-theoretic process itself would require moderate engineering of graph structures and stochastic process definitions.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-60

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

Start by reading the linked Erdős Problems page and the cited papers, then inspect existing formalized conjectures in the repository for the expected statement conventions. No repository files, tests, or entry points are named; done would require adding this conjecture in Lean, including the graph and random triangle-deletion foundations identified in the issue.

Written by the indexing model from the issue text.