Claim. There are constants $c>0$ and $n_0$ such that for every even $n>n_0$ and $e=n^2/2$, every graph with $e$ edges contains a bipartite subgraph with at least

edges. This is Theorem 1.1 of N. Alon, Bipartite subgraphs, Combinatorica 16 (1996), no. 3, 301--311; the corpus states it and reconstructs its proof on its result page. The Edwards baseline of [[problems/extremal_graph_theory/E0127/_index|Problem 127]] is $e/2+(\sqrt{8e+1}-1)/8=e/2+\sqrt{e/8}+O(1)$, so the correction satisfies $f(n^2/2)\ge ce^{1/4}-O(1)\gg n^{1/2}$ along this sequence, in the integer convention of the page as well as the real one, and $f(m_i)\to\infty$ for $m_i=i^2/2$ with $i$ even. The answer to the question is yes. The same paper's inequality (2) gives $f(m)\ll m^{1/4}$ for every $m$, so the exponent $1/4$ is best possible.

Depends on. Nothing in this wiki.

Acceptance. The paper is a refereed publication in Combinatorica, issued in September 1996 (the day of issue is not recorded, and this page's date is the first of that month), which is the refereed evidence, and the site's curator, Thomas Bloom, records the problem as proved by it, which is the reviewed evidence; Bloom took no part in the paper. The corpus's reconstruction of the proof on the result page is author-recorded compilation work, not an independent review. The acceptance recorded here rests on the publication and the site's acceptance.

Formalization. The file src/latest/ErdosProblems/Erdos127.lean of Boris Alexeev's plby/lean-proofs repository, at the commit linked above, declares itself a formalization of this theorem: it names Alon as the informal author, names Codex and GPT-5.6 Sol as its formal authors, and records the toolchain as Lean 4.33.0 with Mathlib v4.33.0. It defines the Edwards baseline $m/2+(\sqrt{8m+1}-1)/8$ as a real number, defines correction m as the greatest integer $k\le m$ such that every finite simple graph with $m$ edges has a bipartite subgraph with at least baseline plus $k$ edges, and declares, in the namespace Erdos127,

theorem erdos_127 :
    ∃ mseq : ℕ → ℕ, Tendsto mseq atTop atTop ∧
      Tendsto (fun i ↦ correction (mseq i)) atTop atTop

through an explicit Alon-type lower bound alon_correction_lower_bound on the edge counts $(2^{20}t^2)^2/2$: the question in the integer convention the problem page adopts. Its first commit in the repository is dated 2026-08-17. This corpus has not built the development, printed its axioms, or audited the definitions against the problem statement beyond the account on the problem page, and only the pinned commit is described. The development is therefore a link on this page and no formalized evidence. The community database lists the site's formal status as Lean as of its last update on 24 August 2026, without dating the change of state, and records the statement as formalized since 19 September 2026, when the formal-conjectures statement file for the problem registered this development's erdos_127, at a later commit than the one linked above, as its formal proof.