---

Claim. Let $f(m)$ be the largest $k$ such that every triangle-free graph with $m$ edges contains a bipartite subgraph with at least $k$ edges, the function of Problem 581. There are absolute constants $c',C'>0$ such that for every $m>1$

$$\frac m2+c'm^{4/5}\le f(m)\le\frac m2+C'm^{4/5},$$

so $f(m)=m/2+\Theta(m^{4/5})$ and the exponent $4/5$ cannot be improved. The lower bound holds for every triangle-free graph with $m$ edges; the upper bound is witnessed by explicit triangle-free graphs. The claim value is answered: the question asks to determine $f(m)$, and the result is neither a proof nor a disproof but a determination of the order of the surplus over $m/2$, which the site's estimate vocabulary calls resolved and this corpus reads the same way; the exact value of $f(m)$, the best constants and the small values are not known from any source on record (Alon writes on p. 8 that determining the minimum precisely "seems more difficult").

The result. Theorem 1.2 of N. Alon, Bipartite subgraphs, Combinatorica 16 (1996), no. 3, 301--311, doi:10.1007/BF01261315, with the sharpness half proved as Proposition 3.2; the result pages theorem_1_2 and proposition_3_2 state both in the corpus's words with the proof pointers, and the source card identifies the edition, the author's final version. In the paper's notation $f(G)$ is the largest number of edges of a bipartite subgraph of $G$, and the theorem says that every triangle-free graph with $e>1$ edges has $f(G)\ge e/2+c'e^{4/5}$, while for every $e$ some triangle-free graph with $e$ edges has $f(G)\le e/2+C'e^{4/5}$; with $e=m$ these are the two inequalities above. The lower bound improves Shearer's exponent $3/4$ (and his independent, earlier $4/5-\epsilon$, recorded in the paper's note added in proof); the upper bound comes from the eigenvalue bound of Lemma 3.1 applied to Alon's explicit triangle-free regular graphs, extended to every $e$ by disjoint copies and isolated edges. The constants are not made explicit. Read depth, as the problem page records: claims checked for Theorem 1.2 and Proposition 3.2; the proof of the lower bound read for structure and not checked; nothing independently reviewed here.

Formalization. The file Erdos581.lean of Boris Alexeev's repository lean-proofs (added 17 August 2026; the link is pinned) declares itself "a Lean formalization of a solution to Erdős Problem 581", names Noga Alon as its informal author and Codex and GPT-5.6 Sol as its formal authors, and proves erdos_581, the two-sided bound for every $m$ with the explicit constants $c_1=1/1024$ and $c_2=1024$, from its LowerBound and UpperBound modules. The formal-conjectures statement file ErdosProblems/581.lean (added 20 September 2026) links it as the formal proof of its erdos_581 under research solved, as the problem page's Formalization records. This corpus has not built or audited the file, so it is a formalization link on this page and not formalized evidence; the evidence stays reviewed and refereed.

Acceptance. refereed: Combinatorica is a refereed journal; the Crossref record of the DOI gives the issue as September 1996, which dates this page to that month (the day is the month's first, since the record gives no day). reviewed: the site's curator, Thomas Bloom, labels the problem SOLVED and credits the resolution to this theorem in the problem's commentary (the site's page, accessed 2026-09-18, with an empty thread and an empty proof-claim tab), a documented acceptance by the site in its estimate sense. The site's label SOLVED, which it defines as a resolution by some means other than a proof or a disproof, is the discussion link. The community database lists the problem as solved, its record last updated 31 August 2025.