---

Claim. The file src/latest/ErdosProblems/Erdos1077.lean of the repository plby/lean-proofs (Lean v4.33.0, Mathlib v4.33.0; first added to the repository on 16 August 2026, the date of this page) proves Erdos1077.not_erdos_1077, the negation of the right-hand side of the formal-conjectures statement of Problem 1077: it is not the case that for every $0<\epsilon<1$ and $0<\alpha<1$, eventually in $D$ and then in $n$, every graph on Fin n with more than $n^{1+\alpha}$ edges has a $D$-balanced subgraph on more than $n^{1-\alpha}$ vertices with more than $\epsilon m^{1+\alpha}$ edges. The proof specializes $\epsilon=\tfrac12$ and $\alpha=\tfrac14$ and uses the complete bipartite graph $K_{2k,k^4-2k}$ on $k^4$ vertices, whose edge count exceeds $(k^4)^{5/4}$ while every $D$-balanced subgraph with at least one edge has at most $2(D+1)k$ vertices, through the lemma balanced_subgraph_vertex_bound, which assumes an edge, since the edgeless subgraph on all $k^4$ vertices is $D$-balanced; the file defines IsBalanced as maximum degree at most $D$ times minimum degree, ends with #print axioms Erdos1077.not_erdos_1077 and an alias erdos_1077 for the negation, and has no occurrence of sorry, axiom, native_decide or unsafe. The formal-conjectures file at the pinned commit states erdos_1077 as answer(False) under category research solved and names line 265 of this file, at its revision of 30 August 2026 (the second link above), in its formal_proof attribute; its choices, upper bounds $\epsilon<1$ and $\alpha<1$ where the site's wording has none and strict edge counts where the site says "at least", are recorded on the problem page. The header names the Formal Conjectures authors as statement authors and carries a copyright line naming Boris Alexeev; it lists GPT-5.6 Sol as informal author and Codex and GPT-5.6 Sol as formal authors, and the copyright block's Authors line names OpenAI Codex, so the argument is the file's own and the claimant is the repository's owner. The witness family is the one that JunGao's comment and the site name (JunGao), taken at $\alpha=\tfrac14$, but the file does not cite the comment and credits its informal argument to GPT-5.6 Sol. The formal-conjectures statement file is linked from the problem page and is not a formalization of this result.

Depends on. Nothing in this wiki; the file is self-contained.

Acceptance. Formalized. This corpus's verification built the repository at the pinned commit of 15 September 2026, in its src/latest project (Lean v4.33.0, Mathlib v4.33.0), compiling the module ErdosProblems.Erdos1077 and the repository's comparator challenge for it, ComparatorChallenges/ErdosProblems/Erdos1077.lean, and checked the axioms of Erdos1077.not_erdos_1077, which are exactly propext, Classical.choice and Quot.sound. The challenge states that theorem without proof together with the definition SimpleGraph.IsBalanced, and the fingerprint of the theorem and of that definition was found identical in the module and the challenge, so the module's own choice of decidability instances leaves the statement unchanged. The module built is a later revision of the one the formal-conjectures file names: a lint of 31 August 2026 expands one simp call and drops an instance argument of balanced_subgraph_vertex_bound, and leaves the theorem's statement and the challenge as they were. The statement was audited clause by clause against the problem's Statement, the wording as printed, which implies the formal statement under every reading of how large $D$ and $n$ must be: the bounds $\epsilon<1$ and $\alpha<1$, a threshold in $n$ that may depend on $D$, a real $D$ (balance is monotone in $D$) and the strict edge hypothesis only weaken what is asserted, and the strict edge conclusion follows from the wording applied with $2\epsilon$, since $m\ge1$; IsBalanced applied to H.coe compares the maximum and minimum degrees within the subgraph, and an arbitrary subgraph covers an induced reading as well. So the theorem refutes the printed wording, the full-scope disproof this page claims. Not reviewed: the formal-conjectures maintainers link the file as the formal proof, but the site's commentary and thanks line credit JunGao's witness and do not name the file, and no outside examination of it is published. Not refereed: the result exists only as a file in a public repository.