Combinatorics

A graph $H$ is $r$-degenerate if every nonempty subgraph of $H$ has a vertex of degree at most $r$. Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite $r$-degenerate graph $H$ satisfies

The conjecture was known in several cases: when one bipartition class has maximum degree at most $r$, for $r$-degenerate blow-ups of trees, and, for $r = 2$, for grids and certain critical 2-degenerate graphs. The best general bound was the weaker $\mathrm{ex}(n,H) = O(n^{2-1/(4r)})$ of Alon, Krivelevich and Sudakov.

This mission carries a complete Lean 4 formalisation refuting it at $r = 2$.

Theorem. There exist a fixed connected bipartite 2-degenerate graph $H$ and constants $c, \varepsilon > 0$ such that

for all sufficiently large $n$. Since the conjectured bound at $r = 2$ is $O(n^{3/2})$, the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if $\mathrm{ex}(n,H) = O(n^{3/2})$; Janzer had already disproved the reverse implication, and this result refutes the forward one.

The construction. The counterexample $H$ is built in layers: starting from a layer $V_0$ of size $L_0$, each subsequent layer is $V_i = \binom{V_{i-1}}{2}$, and every vertex $\{a,b\} \in V_i$ is joined to its two parents $a, b \in V_{i-1}$. The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.

The lower bound comes from a sampled Hamming-ball graph. With $U = \{0,1\}^m$, two disjoint copies $U_L, U_R$ are joined whenever their Hamming distance is at most $k = \lfloor \tau m\rfloor$, and each vertex is retained independently with probability $p = 2^{-\beta m}$. The two parameters are governed by the thresholds

and the construction needs a sampling exponent with $A(\tau) < \beta < C(\tau)$. The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than $n^{3/2}$ edges.

Exclusion runs on a conditional-entropy functional $E(u,z) = \frac{1}{m}\sum_j H(Z_j \mid X_j, Y_j)$ over parent and child arrays. An array of conditional entropy $E$ has at most $2^{mME + O(m\log_2 M)}$ realisations, while requiring its $M = \binom{L}{2}$ children to survive sampling costs $2^{-\beta mM}$ — which dominates the $2^{mL}$ possible parent arrays whenever $E < \beta$. An embedding of $H$ would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has $\Omega(n^{3/2+\varepsilon})$ edges, and padding extends the construction to every sufficiently large order.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from [propext, Classical.choice, Quot.sound] alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.

This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.

Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family $\mathcal{F}$ whose members all contain a cycle, there should be some $F \in \mathcal{F}$ and $C>0$ with $\mathrm{ex}(n,F) \le C\,\mathrm{ex}(n,\mathcal{F})$ for all large $n$. The cycle hypothesis is essential — the folklore family $\{K_{1,2}, 2K_2\}$ already defeats the original formulation — and the corrected conjecture is Erdős problem #180.

This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family $\mathcal{F}$ of connected bipartite graphs, each containing a cycle, with

The two bounds are separated by a polynomial factor $n^{1/48}$, so no member can dominate the family up to any constant. The family is $\mathcal{F} = \{C_4, C_6\} \cup \mathcal{J} \cup \mathcal{K}$, where $\mathcal{J}$ and $\mathcal{K}$ are the admissible quotients of two properly $2$-coloured templates built from the subdivisions of $K_{3,2}$ and $K_{3,3}$. The upper bound comes from counting short paths in an $\mathcal{F}$-free graph: excluding $\mathcal{J}$ bounds the number of vertices that fail to be centres of a subdivided $K_{3,3}$, and excluding $\mathcal{K}$ forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles $W(q)$, with the characteristic of the underlying field chosen to suit the forbidden member — even $q$ for $\mathcal{J}$, odd $q$ for $\mathcal{K}$ — which is exactly the freedom a family bound does not have.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers"), re-verified in this environment. Every node is proved; the mission is offered as a curated, closed campaign whose definitions and lemmas are reusable foundations for further work in extremal graph theory.

How fast do multicolour Ramsey numbers grow? Write $R_k$ for the least $n$ such that every colouring of the edges of $K_n$ with $k$ colours contains a monochromatic triangle. The classical bounds, essentially unimproved for decades, place $R_k$ between $c^k$ and $e\cdot k!$, and Erdős asked repeatedly whether the truth is closer to the exponential lower end — his Problem 183 asks whether $R_k^{1/k}\to\infty$, i.e. whether the growth is genuinely superexponential.

This mission carries a complete Lean 4 formalisation resolving that question in the affirmative, with an explicit bound: $R_k \ge \left(\tfrac{1}{6e^{38}}\,k^{1/3}/\log k\right)^{k}$ for all sufficiently large $k$, from which $R_k^{1/k}\to\infty$ follows, together with the matching two-sided estimate $\log R_k = \Theta(k\log k)$ pinning the sharp coefficients. The argument is constructive: it builds triangle-free colourings by a recursive palette construction whose colour count grows fast enough to beat every exponential.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science, re-verified in this environment. Every node is proved — the mission is offered as a curated, closed campaign whose milestones map the attack path and whose lemmas are reusable foundations for further work on multicolour Ramsey theory.

Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.

Motivation

The Angel problem asks whether a piece with a bounded movement range can survive forever on an infinite chessboard while an adversary destroys one square per turn. A large movement range does not settle the question by itself: the adversary may destroy squares far ahead of the moving piece, and no fixed finite board represents all possible plays. The problem therefore combines local geometric restrictions with an infinite strategic requirement. Its formalization provides a concrete setting in which the order of strategic quantifiers and the distinction between finite and infinite play both matter.

This project concerns a published solution, not a new solution to an open conjecture. Andras Mathe proved that power two suffices in The Angel of power 2 wins, published in 2007. The source for this mission is that paper, specifically its definitions in Section 2 and the power-two result in Section 4. The manuscript's internal page numbers run from 1 to 9; they differ from the journal's pages 363-374. The principal target is Theorem 4.6 on manuscript page 8.

Setting

A square is an integer pair in the infinite lattice. The Angel starts at the origin. A move of power $p$ changes each coordinate by at most $p$ in absolute value. Intermediate squares do not constrain a jump. The formalization follows the source's finite-journey convention, which permits zero-length moves. The Devil moves first, and on each turn chooses a square to eat or passes. The Angel then chooses a destination using the observed history. Landing on any previously eaten square, including the square eaten on that turn, loses. The source permits the Devil to name the occupied square; this does not itself end the game before the Angel's next landing.

A strategy is a function of information already revealed. It cannot inspect future opposing actions. Devil strategies take the finite list of visited squares. Angel strategies take that list together with the finite list of Devil actions, including the action on the current turn. Recursion on the number of completed rounds produces a unique play for each pair of strategies. Losing continuations remain formally defined, but are not counted as surviving plays.

A Nice Devil is restricted by the Angel's earlier opportunities. The origin is protected, as is every square within movement range of any visited position before the last position in the current history. This is the restriction used in equation (2) of the paper. Against this restricted opponent, merely staying alive is not the intended objective. The Angel must reach positions outside every finite box centred at the origin. No single bounded region may contain the entire play.

Formalization targets

The main target is Theorem 4.6:

Here $A$ and $D$ range over the history-dependent strategies just described, and survival requires legal, uneaten landings at every round. The existential quantifier over $A$ precedes the universal quantifier over $D$: choosing a different prescient Angel strategy separately for each opponent would not state the target.

The two initial milestones correspond to the paper's main division. Theorem 2.7 supplies a Nice Devil confinement consequence when the Angel has no winning strategy, with the determinacy observation in the introduction included in that formulation. Confinement applies to every finite safe prefix, not merely to plays that already survive forever. Theorem 4.5 supplies a power-two Angel strategy that survives and reaches outside every finite box against every Nice Devil. These milestones retain the infinite-board and unrestricted-history quantifiers.

Significance

The mathematical result gives a fixed movement range sufficient to withstand an adversary operating anywhere on the board. Its conclusion is uniform in the opponent and in the duration of play. A finite simulation, however long, cannot supply that conclusion. Nor does a strategy that succeeds against one chosen Devil establish it against all Devils.

The formalization aims to make the game's conventions, the reduction to the restricted opponent, and the geometric escape argument separately inspectable. The current development contains the game definitions and small checked foundational lemmas. The paper's principal results are open formalization targets. In particular, a proved logical lemma assembling the two milestones does not prove either milestone. The project makes no claim of a completed machine-checked solution at this stage.

Difficulty

The principal obstacles are strategic and geometric. Finite survival statements must support the infinite strategic conclusion without exchanging quantifiers. Restrictions on the Nice Devil must protect exactly the squares specified by the source. In the geometric part, the source's wall-following construction must remain legal while the obstacle configuration changes, and its boundary estimates must connect to actual plays. A numerical contradiction between perimeter bounds is useful only after those bounds have been established for the constructed strategy. These are mathematical obligations, not consequences of successful type checking of the model.

Formalization scope

The initial Lean implementation uses integer coordinate pairs, finite lists, optional Devil actions, and primitive recursion on natural numbers. It is pinned to Lean 4.33.1, matching the selected platform environment. The current files use Lean's standard library; Mathlib can be introduced at the platform's pinned revision when geometric infrastructure requires it. There is no finite-board cutoff and no assumed winning strategy inside the definitions.

The first proposal contains one shared definition bundle, two theorem milestones, and the main theorem. Further decomposition of the milestones will be added only after the corresponding geometric or strategy interfaces are precisely stated and audited. Expected remaining work includes the finite-journey reduction, the compactness/determinacy connection, connected-square boundary estimates from Claim 4.2, and the wall-following construction underlying Proposition 4.3. The present scope is the integer-power Angel game through Theorem 4.6; the fractional-speed King extension in Section 5 is excluded.

Selected references

• Andras Mathe, The Angel of power 2 wins, Combinatorics, Probability and Computing 16 (2007), 363-374. DOI.
• Archived author manuscript, Sections 2 and 4, especially Theorems 2.7, 4.5 and 4.6.