Erdős Problem 146

*This issue was written by Claude Opus 5.*

### What is the Erdős problem?

https://www.erdosproblems.com/146

If $H$ is bipartite and is $r$-degenerate, that is, every induced subgraph of $H$ has minimum degree $\leq r$, then
$$\mathrm{ex}(n;H) \ll n^{2-1/r}.$$

Conjectured by Erdős and Simonovits [ErSi84]. Alon, Krivelevich, and Sudakov [AKS03] have proved $\mathrm{ex}(n;H) \ll n^{2-1/4r}$, and prove the full conjectured bound if $H$ is bipartite and the maximum degree in one side of the bipartition is $r$.

Status: solved (negatively). erdosproblems.com still records the problem as open as of its edit of 18 January 2026. It was refuted by OpenAI, *Ten advances in mathematics and theoretical computer science*, Ch. 10 (2026), which exhibits a bipartite $2$-degenerate $H$ with $\mathrm{ex}(n;H)$ eventually exceeding any multiple of $n^{3/2}$; since the conjecture is universally quantified over $r$, that case refutes it. A Lean 4 proof is available at https://github.com/openai/ten-proofs.

A strengthening to every $r \geq 2$, with degeneracy exactly $r$ and exponent $2-1/r+1/(28r^2)$, is available at https://github.com/EvolvingPrograms/erdos-simonovits-degeneracy. It generalises the OpenAI construction and builds on its Lean development. It is machine-checked, and the Lean formalisation was checked by Sai Gajjala (New York University). It has not been peer reviewed. Whether it should be recorded here, and under which category, is a question for review of the pull request.

The repository currently contains no formalised statement of this problem.

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

* ams-05

### Choose either option
- [x] I plan on adding this Erdős problem to the repository
- [ ] This issue is up for grabs: I would like to see this Erdős problem added by somebody else

### References

- [ErSi84] Erdős, P. and Simonovits, M., *Cube-supersaturated graphs and related problems*. Progress in graph theory (Waterloo, Ont., 1982) (1984), 203-218.
- [AKS03] Alon, N., Krivelevich, M. and Sudakov, B., *Turán numbers of bipartite graphs and related Ramsey-type questions*. Combin. Probab. Comput. **12** (2003), 477-494.

Begin by reviewing the linked Lean proof and the repository's existing formalized conjecture statements. Determine how the Erdős–Simonovits degeneracy statement should be represented, and resolve whether the stronger linked result belongs in this issue before formalizing and validating the statement.

Written by the indexing model from the issue text.