diff --git a/FormalConjectures/ErdosProblems/111.lean b/FormalConjectures/ErdosProblems/111.lean
new file mode 100644
index 0000000000..4bdaf8b71f
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/111.lean
@@ -0,0 +1,144 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 111
+
+*References:*
+- [erdosproblems.com/111](https://www.erdosproblems.com/111)
+- [Er81] Erdős, P., Some combinatorial problems in graph theory. (1981)
+- [EHS82] Erdős, P., Hajnal, A., and Szemerédi, E., On almost bipartite large chromatic graphs.
+  Annals of Discrete Math. (1982), 117–123.
+- [Er87] Erdős, P., Problems and results on chromatic numbers in finite and infinite graphs. (1987)
+- [Er90] Erdős, P., Some of my favourite problems in various branches of combinatorics. (1990)
+- [Er97d] Erdős, P., Some problems on elementary geometry. (1997)
+- [Er97f] Erdős, P., Some of my favourite unsolved problems. (1997)
+
+See also Erdős Problem [74].
+
+## Formalization notes
+
+- **`bipartiteDistance G`**: the minimum number of edges to delete from a (finite) simple graph $G$
+  to make it bipartite. Defined as the infimum over all spanning subgraphs $H \leq G$ with
+  `H.IsBipartite` of the number of edges in `G.edgeSet \ H.edgeSet`.
+
+- **`hG G n`**: for a graph $G$ on vertex type $V$, `hG G n` is the supremum over all sets $S$ of
+  vertices of cardinality $n$ of `bipartiteDistance (G.induce S)`. This matches the problem's
+  formulation: "any subgraph of $G$ on $n$ vertices can be made bipartite after deleting at most
+  $h_G(n)$ edges."
+-/
+
+open Filter Asymptotics Cardinal SimpleGraph Set
+
+namespace Erdos111
+
+/-- The **bipartite distance** of a finite simple graph `G`: the minimum number of edges
+that must be deleted from `G` to make it bipartite.
+
+Formally, this is the infimum of `Set.ncard (G.edgeSet \ H.edgeSet)` over all spanning
+subgraphs `H ≤ G` (as relations on the same vertex set) such that `H` is bipartite. -/
+noncomputable def bipartiteDistance {V : Type*} (G : SimpleGraph V) : ℕ :=
+  sInf {k : ℕ | ∃ H : SimpleGraph V, H ≤ G ∧ H.IsBipartite ∧
+    Set.ncard (G.edgeSet \ H.edgeSet) = k}
+
+/-- The function $h_G(n)$: for a graph $G$ on vertex type $V$, `hG G n` is the supremum over
+all sets $S \subseteq V$ with $|S| = n$ of the bipartite distance of the induced subgraph on $S$.
+
+This captures the problem's notion: "any subgraph of $G$ on $n$ vertices can be made bipartite
+after deleting at most $h_G(n)$ edges." -/
+noncomputable def hG {V : Type*} (G : SimpleGraph V) (n : ℕ) : ℕ :=
+  sSup {k : ℕ | ∃ S : Set V, S.ncard = n ∧ bipartiteDistance (G.induce S) = k}
+
+/- ## Main open problem -/
+
+/--
+**Erdős Problem 111** (Erdős, Hajnal, Szemerédi [EHS82]):
+
+If $G$ is a graph with chromatic number $\aleph_1$, is it true that $h_G(n)/n \to \infty$?
+
+Formally: for every graph $G$ (on a type $V$) with chromatic cardinal $\aleph_1$, the ratio
+$h_G(n)/n$ is unbounded, i.e., for every constant $C$, there are arbitrarily large $n$ such
+that $h_G(n) > C \cdot n$.
+-/
+@[category research open, AMS 5]
+theorem erdos_111 : answer(sorry) ↔
+    ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
+      Filter.Tendsto (fun n : ℕ => (hG G n : ℝ) / n) Filter.atTop Filter.atTop := by
+  sorry
+
+/- ## Variants and known partial results -/
+
+/--
+**Linear lower bound (ZFC, [EHS82])**: Every graph $G$ with chromatic number $\aleph_1$ has
+$h_G(n) \geq c \cdot n$ for some positive constant $c > 0$ and all sufficiently large $n$
+(i.e., the *linear* lower bound $h_G(n) \gg n$ is known).
+
+This follows from the fact that every graph with uncountable chromatic number contains
+$\aleph_1$ vertex-disjoint odd cycles of some fixed odd length $\ell$: any induced subgraph
+on $n$ vertices containing $\gg n / \ell$ such cycles requires removing $\gg n$ edges to
+become bipartite.
+
+This is a *strictly weaker* statement than the headline `erdos_111`, which asks for
+$h_G(n)/n \to \infty$ (i.e., $h_G(n)$ grows *super-linearly* — the constant `c` could be
+taken arbitrarily large for a fixed graph $G$). Whether the linear lower bound can be
+improved to super-linear remains the open question.
+-/
+@[category research solved, AMS 5]
+theorem erdos_111.variants.lower_bound :
+    ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
+      ∃ c : ℝ, 0 < c ∧
+        ∀ᶠ n : ℕ in Filter.atTop, c * n ≤ hG G n := by
+  sorry
+
+/--
+**Upper bound existence (Erdős-Hajnal-Szemerédi [EHS82])**: There exists a graph $G$ with
+chromatic number $\aleph_1$ such that $h_G(n) \ll n^{3/2}$, i.e., there is a constant $C > 0$
+with $h_G(n) \leq C \cdot n^{3/2}$ for all $n$.
+
+This shows that Erdős's conjecture (if true) would be essentially tight in its exponent:
+the true exponent lies in $(1, 3/2]$.
+-/
+@[category research solved, AMS 5]
+theorem erdos_111.variants.upper_bound_existence :
+    ∃ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 ∧
+      (fun n : ℕ => (hG G n : ℝ)) =O[atTop] (fun n : ℕ => (n : ℝ) ^ (3 / 2 : ℝ)) := by
+  sorry
+
+/--
+**Erdős conjecture (stronger upper bound)**: For every graph $G$ with chromatic number
+$\geq \aleph_1$ and every $\varepsilon > 0$, the function $h_G(n)$ satisfies
+$h_G(n) \ll_\varepsilon n^{1+\varepsilon}$.
+
+That is, for every $\varepsilon > 0$ there exists $C(\varepsilon) > 0$ such that for every graph
+$G$ with $\chi(G) \geq \aleph_1$, we have $h_G(n) \leq C(\varepsilon) \cdot n^{1 + \varepsilon}$
+for all $n$.
+
+This conjecture (if true) would mean that $h_G(n)$ grows only barely super-linearly. The
+quantification is over graphs with $\chi(G) \geq \aleph_1$ (matching the source); using
+$\chi(G) \geq \aleph_1$ is strictly stronger than $\chi(G) = \aleph_1$ as a hypothesis on the
+class of graphs since the bound must hold uniformly for any larger chromatic cardinal too.
+-/
+@[category research open, AMS 5]
+theorem erdos_111.variants.erdos_conjecture : answer(sorry) ↔
+    ∀ (ε : ℝ), 0 < ε →
+      ∃ C : ℝ, 0 < C ∧
+        ∀ (V : Type) (G : SimpleGraph V), ℵ_ 1 ≤ G.chromaticCardinal →
+          ∀ n : ℕ, (hG G n : ℝ) ≤ C * (n : ℝ) ^ (1 + ε) := by
+  sorry
+
+end Erdos111