---

Claim. For every integer $k\ge0$ there is $f(k)$ such that if every subgraph $H$ of a graph $G$ has an independent set of at least $(|H|-k)/2$ vertices, then $G$ has a set $X$ of at most $f(k)$ vertices with $G-X$ bipartite. This is the main theorem of B. Reed, Mangoes and blueberries, Combinatorica 19 (1999), no. 2, 267--296; András Pluhár's zbMATH review of the paper (Zbl 0928.05059) states the theorem in this form and describes it as a conjecture of Erdős and Hajnal, and the site credits Reed with the proof. It is the question of Problem 73 as the page states it, with $O_k(1)=f(k)$. The case $k=0$ needs no proof: an odd cycle on $2m+1$ vertices has no independent set of $m+1$ vertices, so a graph with the hypothesis at $k=0$ has no odd cycle and is itself bipartite.

Acceptance. The paper is a refereed publication in Combinatorica, issued in February 1999, and the site's curator, Thomas Bloom, records the problem as proved by it, which is the reviewed evidence listed. The paper is not held by this corpus (the publisher's page is access-controlled); the statement above follows the site's formulation, in the site's normalization of $k$, which the review's statement and the formal-conjectures docstring below match, and the site's attribution of the proof to the paper. The acceptance recorded here rests on the publication and the site's acceptance, not on a local review.

Formalization. The file src/latest/ErdosProblems/Erdos73.lean of Boris Alexeev's repository plby/lean-proofs, at the pinned commit, names OpenAI Codex as its author and proves Erdos73.erdos_73 : Erdos73.Problem73 by assembling problem73_of_defectHighOrderBramble with reedDefectHighOrderBramble from the development's imported modules; its Foundations module says it fixes the quantifier order and a division-free form of the problem and formalizes the packing, deletion, separation, bramble, odd-minor and stable-defect steps of Reed's proof, reducing the general case to a controlled-wall, high-order-bramble statement that its docstring calls still to be proved; the main file's docstring says instead that the imported modules fully prove the bramble, linkage and wall layers and that the high-order bramble induction gives the unconditional result. The formal-conjectures statement file for the problem, added 2026-09-09, carries since 2026-09-19 a formal_proof attribute pointing to this file's erdos_73, whose docstring credits the proof to Alexeev and Codex following Reed's argument; its statement takes, for every finite graph, an independent set of real size at least $(|S|-k)/2$ in every induced subgraph on a vertex set $S$, and concludes a deletion set of size bounded by a constant depending on $k$ whose removal leaves a bipartite graph. The community database records the problem formalized since 2026-09-09. The development declares itself a formalization of Reed's theorem, so it is a link on this page and not a claim of its own. This corpus has not built or audited it, so no formalized evidence is listed.