diff --git a/apn/data/erdos/Isolated/Erdos1020.erdos_1020.lean b/apn/data/erdos/Isolated/Erdos1020.erdos_1020.lean
new file mode 100644
index 00000000..b52b5ed9
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos1020.erdos_1020.lean
@@ -0,0 +1,36 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1020
+
+*Reference:* [erdosproblems.com/1020](https://www.erdosproblems.com/1020)
+-/
+
+namespace Erdos1020
+
+/-- The maximum number of edges in an `r`-uniform hypergraph on `n` vertices containing no
+matching of size `k` (i.e. no `k` pairwise vertex-disjoint edges). -/
+noncomputable def f (n r k : ℕ) : ℕ :=
+  open scoped Classical in
+  let candidates :=
+    (((Finset.univ : Finset (Fin n)).powersetCard r).powerset).filter fun H ↦
+      ¬ ∃ M : Finset (Finset (Fin n)),
+          M ⊆ H ∧ M.card = k ∧ (M : Set (Finset (Fin n))).PairwiseDisjoint id
+  candidates.sup Finset.card
+
+/--
+Let $f(n;r,k)$ be the maximal number of edges in an $r$-uniform hypergraph which contains no set of $k$ many independent edges. 
+
+For all $r\geq 3$,\[f(n;r,k)=\max\left(\binom{rk-1}{r}, \binom{n}{r}-\binom{n-k+1}{r}\right).\]
+
+Note: the displayed formula is stated on the standard Erdős matching conjecture range
+`k ≥ 1` and `n ≥ r*k - 1`; with fully unrestricted `n` the equality is trivially false
+(e.g. `r = 3`, `k = 2`, `n = 4`), and for `n < r*k - 1` the source remarks the problem
+is trivial (the complete `r`-uniform hypergraph has no `k`-matching).
+-/
+theorem erdos_1020 :
+    ∀ (r : ℕ), 3 ≤ r → ∀ n k : ℕ, 0 < k → r * k - 1 ≤ n →
+      f n r k = max ((r * k - 1).choose r) (n.choose r - (n - k + 1).choose r) := by
+  sorry
+
+end Erdos1020
diff --git a/apn/data/erdos/Isolated/Erdos104.erdos_104.lean b/apn/data/erdos/Isolated/Erdos104.erdos_104.lean
new file mode 100644
index 00000000..f490050b
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos104.erdos_104.lean
@@ -0,0 +1,35 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 104
+
+*Reference:* [erdosproblems.com/104](https://www.erdosproblems.com/104)
+-/
+
+open Filter
+open scoped EuclideanGeometry
+
+namespace Erdos104
+
+open EuclideanGeometry
+
+/-- The number of distinct unit circles containing at least three points of `P`. -/
+noncomputable def unitCircleCount (P : Finset ℝ²) : ℕ :=
+  Set.ncard {s : Sphere ℝ² | s.radius = 1 ∧ 3 ≤ {p ∈ (P : Set ℝ²) | p ∈ s}.ncard}
+
+/-- The set of unit-circle counts attained by configurations of `n` points in the plane. -/
+noncomputable def possibleUnitCircleCounts (n : ℕ) : Set ℕ :=
+  {k | ∃ P : Finset ℝ², P.card = n ∧ unitCircleCount P = k}
+
+/-- The maximum number of qualifying unit circles attained by a configuration of `n` points. -/
+noncomputable def maxUnitCircleCount (n : ℕ) : ℕ :=
+  sSup (possibleUnitCircleCounts n)
+
+/--
+Given $n$ points in $\mathbb{R}^2$ the number of distinct unit circles containing at least three points is $o(n^2)$.
+-/
+theorem erdos_104 :
+    (fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2) := by
+  sorry
+
+end Erdos104
diff --git a/apn/data/erdos/Isolated/Erdos1083.erdos_1083.lean b/apn/data/erdos/Isolated/Erdos1083.erdos_1083.lean
new file mode 100644
index 00000000..615b6352
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos1083.erdos_1083.lean
@@ -0,0 +1,30 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1083
+
+*Reference:* [erdosproblems.com/1083](https://www.erdosproblems.com/1083)
+-/
+
+open Filter
+
+namespace Erdos1083
+
+/--
+The minimum number of distinct distances determined by an $n$-point subset of
+$d$-dimensional Euclidean space.
+-/
+noncomputable def f (d n : ℕ) : ℕ :=
+  sInf {m : ℕ | ∃ points : Finset (EuclideanSpace ℝ (Fin d)),
+    points.card = n ∧ distinctDistances points = m}
+
+/--
+Let $d\geq 3$, and let $f_d(n)$ be the minimal $m$ such that every set of $n$ points in $\mathbb{R}^d$ determines at least $m$ distinct distances. Estimate $f_d(n)$ - in particular, is it true that\[f_d(n)=n^{\frac{2}{d}-o(1)}?\]
+-/
+theorem erdos_1083 :
+    (∀ d : ℕ, 3 ≤ d → ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
+      ∀ᶠ n : ℕ in atTop,
+        (f d n : ℝ) = (n : ℝ) ^ ((2 : ℝ) / (d : ℝ) - o n)) := by
+  sorry
+
+end Erdos1083
diff --git a/apn/data/erdos/Isolated/Erdos1159.erdos_1159.lean b/apn/data/erdos/Isolated/Erdos1159.erdos_1159.lean
new file mode 100644
index 00000000..49e409ba
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos1159.erdos_1159.lean
@@ -0,0 +1,26 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1159
+
+*Reference:*
+- [erdosproblems.com/1159](https://www.erdosproblems.com/1159)
+-/
+
+open Configuration
+
+namespace Erdos1159
+
+/--
+Determine whether there exists a constant $C>1$ such that the following holds.
+
+Let $P$ be a finite <a href="https://en.wikipedia.org/wiki/Projective_plane" rel="nofollow noopener noreferrer ugc" target="_blank">projective plane</a>. Must there exist a set of points $S$ such that $1\leq \lvert S\cap \ell\rvert \leq C$ for all lines $\ell$?
+-/
+theorem erdos_1159 :
+    (∃ C : ℕ, 1 < C ∧
+      ∀ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L),
+        ∀ _ : ProjectivePlane P L, ∃ S : Set P, ∀ l : L,
+          1 ≤ (S ∩ {p : P | p ∈ l}).ncard ∧ (S ∩ {p : P | p ∈ l}).ncard ≤ C) := by
+  sorry
+
+end Erdos1159
diff --git a/apn/data/erdos/Isolated/Erdos1206.erdos_1206.parts.i.lean b/apn/data/erdos/Isolated/Erdos1206.erdos_1206.parts.i.lean
new file mode 100644
index 00000000..964d7d12
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos1206.erdos_1206.parts.i.lean
@@ -0,0 +1,20 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1206
+
+*Reference:* [erdosproblems.com/1206](https://www.erdosproblems.com/1206)
+-/
+
+namespace Erdos1206
+
+/--
+Does $\{1,2^3,\ldots,N^3\}$ contain a Sidon set of size $\gg N$?
+-/
+theorem erdos_1206.parts.i :
+    ∃ c : ℝ, 0 < c ∧ ∀ᶠ N in Filter.atTop, ∃ S : Finset ℕ,
+      S ⊆ (Finset.Icc 1 N).image (fun n => n ^ 3) ∧
+      IsSidon (S : Set ℕ) ∧ c * (N : ℝ) ≤ (S.card : ℝ) := by
+  sorry
+
+end Erdos1206
diff --git a/apn/data/erdos/Isolated/Erdos1206.erdos_1206.parts.ii.lean b/apn/data/erdos/Isolated/Erdos1206.erdos_1206.parts.ii.lean
new file mode 100644
index 00000000..6c8f056d
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos1206.erdos_1206.parts.ii.lean
@@ -0,0 +1,19 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1206
+
+*Reference:* [erdosproblems.com/1206](https://www.erdosproblems.com/1206)
+-/
+
+namespace Erdos1206
+
+/--
+Is there an infinite set $A\subset \mathbb{N}$ of positive density such that $\{a^3 : a\in A\}$ is a Sidon set?
+-/
+theorem erdos_1206.parts.ii :
+    ∃ A : Set ℕ, A.Infinite ∧ 0 < A.lowerDensity ∧
+      IsSidon ((fun a : ℕ => a ^ 3) '' A) := by
+  sorry
+
+end Erdos1206
diff --git a/apn/data/erdos/Isolated/Erdos1207.erdos_1207.lean b/apn/data/erdos/Isolated/Erdos1207.erdos_1207.lean
new file mode 100644
index 00000000..769f98ce
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos1207.erdos_1207.lean
@@ -0,0 +1,33 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1207
+
+*Reference:* [erdosproblems.com/1207](https://www.erdosproblems.com/1207)
+-/
+
+open Filter
+
+namespace Erdos1207
+
+/-- A set is isosceles-free if no three distinct points in it form an isosceles triangle. -/
+def IsIsoscelesFree {α : Type*} [Dist α] (A : Set α) : Prop :=
+  A.Triplewise fun x y z => ¬ IsIsosceles x y z
+
+/--
+`P d n` is the largest number such that every set of `n` points in Euclidean `d`-space has an
+isosceles-free subset of at least that size.
+-/
+noncomputable def P (d n : ℕ) : ℕ :=
+  sInf {m : ℕ | ∃ S : Finset (EuclideanSpace ℝ (Fin d)), S.card = n ∧
+    m = sSup {k : ℕ | ∃ A : Finset (EuclideanSpace ℝ (Fin d)),
+      A ⊆ S ∧ IsIsoscelesFree (A : Set (EuclideanSpace ℝ (Fin d))) ∧ A.card = k}}
+
+/--
+Let $P_d(n)$ be such that in any set of $n$ points in $\mathbb{R}^d$ there exist at least $P_d(n)$ many points which do not contain an isosceles triangle. Estimate $P_d(n)$ - in particular, is it true that\[P_2(n)<n^{1-c}\]for some constant $c>0$?
+-/
+theorem erdos_1207 :
+    (∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (P 2 n : ℝ) < (n : ℝ) ^ (1 - c)) := by
+  sorry
+
+end Erdos1207
diff --git a/apn/data/erdos/Isolated/Erdos181.erdos_181.lean b/apn/data/erdos/Isolated/Erdos181.erdos_181.lean
new file mode 100644
index 00000000..40e2d10d
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos181.erdos_181.lean
@@ -0,0 +1,27 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 181
+
+*Reference:* [erdosproblems.com/181](https://www.erdosproblems.com/181)
+-/
+
+namespace Erdos181
+
+open SimpleGraph
+
+/-- The diagonal Ramsey number of a finite graph `G`: the least `N` such that every red-blue
+colouring of the edges of the complete graph on `N` vertices contains a monochromatic copy of `G`.
+A graph `R` records the red edges, and `Rᶜ` records the blue edges. -/
+noncomputable def diagonalRamseyNumber {α : Type*} [Fintype α] (G : SimpleGraph α) : ℕ :=
+  sInf {N : ℕ | ∀ R : SimpleGraph (Fin N), G.IsContained R ∨ G.IsContained Rᶜ}
+
+/--
+Let $Q_n$ be the $n$-dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Prove that\[R(Q_n) \ll 2^n.\]
+-/
+theorem erdos_181 :
+    ∃ C > (0 : ℝ), ∀ n : ℕ,
+      (diagonalRamseyNumber (hypercube n) : ℝ) ≤ C * 2 ^ n := by
+  sorry
+
+end Erdos181
diff --git a/apn/data/erdos/Isolated/Erdos322.erdos_322.lean b/apn/data/erdos/Isolated/Erdos322.erdos_322.lean
new file mode 100644
index 00000000..bbb1c8f4
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos322.erdos_322.lean
@@ -0,0 +1,25 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 322
+
+*Reference:* [erdosproblems.com/322](https://www.erdosproblems.com/322)
+-/
+
+namespace Erdos322
+
+/-- For `k ≥ 3`, the number of ordered representations of `n` as a sum of `k` many `k`th
+powers of nonnegative integers. The bases can be restricted to the interval from `0` to `n`. -/
+def representationCount (k n : ℕ) : ℕ :=
+  ((Finset.univ : Finset (Fin k → Fin (n + 1))).filter
+    (fun a ↦ ∑ i, (a i : ℕ) ^ k = n)).card
+
+/--
+Let $k\geq 3$ and $A\subset \mathbb{N}$ be the set of $k$th powers. What is the order of growth of $1_A^{(k)}(n)$, i.e. the number of representations of $n$ as the sum of $k$ many $k$th powers? Does there exist some $c>0$ and infinitely many $n$ such that\[1_A^{(k)}(n) >n^c?\]
+-/
+theorem erdos_322 :
+    (∀ k : ℕ, 3 ≤ k → ∃ c > (0 : ℝ),
+      {n : ℕ | (n : ℝ) ^ c < representationCount k n}.Infinite) := by
+  sorry
+
+end Erdos322
diff --git a/apn/data/erdos/Isolated/Erdos431.erdos_431.lean b/apn/data/erdos/Isolated/Erdos431.erdos_431.lean
new file mode 100644
index 00000000..26e8ce27
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos431.erdos_431.lean
@@ -0,0 +1,21 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 431
+
+*Reference:* [erdosproblems.com/431](https://www.erdosproblems.com/431)
+-/
+
+open scoped Pointwise
+
+namespace Erdos431
+
+/--
+Are there two infinite sets $A$ and $B$ such that $A+B$ agrees with the set of prime numbers up to finitely many exceptions?
+-/
+theorem erdos_431 :
+    (∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧
+      (symmDiff (A + B) {p : ℕ | p.Prime}).Finite) := by
+  sorry
+
+end Erdos431
diff --git a/apn/data/erdos/Isolated/Erdos478.erdos_478.lean b/apn/data/erdos/Isolated/Erdos478.erdos_478.lean
new file mode 100644
index 00000000..121234ee
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos478.erdos_478.lean
@@ -0,0 +1,23 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 478
+
+*Reference:* [erdosproblems.com/478](https://www.erdosproblems.com/478)
+-/
+
+namespace Erdos478
+
+/--
+Let $p$ be a prime and\[A_p = \{ k! \pmod{p} : 1\leq k<p\}.\]Is it true that\[\lvert A_p\rvert \sim (1-\tfrac{1}{e})p?\]
+-/
+theorem erdos_478 :
+    Filter.Tendsto
+      (fun p : ℕ =>
+        (((Finset.Ico 1 p).image (fun k => Nat.factorial k % p)).card : ℝ) / p)
+      (Filter.atTop ⊓ Filter.principal {p : ℕ | p.Prime})
+      (nhds (1 - 1 / Real.exp 1))
+      := by
+  sorry
+
+end Erdos478
diff --git a/apn/data/erdos/Isolated/Erdos548.erdos_548.lean b/apn/data/erdos/Isolated/Erdos548.erdos_548.lean
new file mode 100644
index 00000000..a7ae2afb
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos548.erdos_548.lean
@@ -0,0 +1,22 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 548
+
+*Reference:* [erdosproblems.com/548](https://www.erdosproblems.com/548)
+-/
+
+open SimpleGraph
+
+namespace Erdos548
+
+/--
+Let $n\geq k+1$. Every graph on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.
+-/
+theorem erdos_548 :
+    ∀ (n k : ℕ), k + 1 ≤ n → ∀ G : SimpleGraph (Fin n),
+      ((k : ℚ) - 1) / 2 * n + 1 ≤ (G.edgeSet.ncard : ℚ) →
+        ∀ T : SimpleGraph (Fin (k + 1)), T.IsTree → T.IsContained G := by
+  sorry
+
+end Erdos548
diff --git a/apn/data/erdos/Isolated/Erdos571.erdos_571.lean b/apn/data/erdos/Isolated/Erdos571.erdos_571.lean
new file mode 100644
index 00000000..2e40dbad
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos571.erdos_571.lean
@@ -0,0 +1,25 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 571
+
+*References:*
+- [erdosproblems.com/571](https://www.erdosproblems.com/571)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos571
+
+/--
+Show that for any rational $\alpha \in [1,2)$ there exists a bipartite graph $G$ such that\[\mathrm{ex}(n;G)\asymp n^{\alpha}.\]
+-/
+theorem erdos_571 :
+    ∀ α : ℚ, 1 ≤ α → α < 2 →
+      ∃ q : ℕ, ∃ G : SimpleGraph (Fin q), G.IsBipartite ∧
+        Asymptotics.IsTheta atTop
+          (fun n : ℕ => (extremalNumber n G : ℝ))
+          (fun n : ℕ => (n : ℝ) ^ (α : ℝ)) := by
+  sorry
+
+end Erdos571
diff --git a/apn/data/erdos/Isolated/Erdos583.erdos_583.lean b/apn/data/erdos/Isolated/Erdos583.erdos_583.lean
new file mode 100644
index 00000000..93b6ce83
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos583.erdos_583.lean
@@ -0,0 +1,44 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 583
+
+*References:*
+- [erdosproblems.com/583](https://www.erdosproblems.com/583)
+- [Er71] Erdős, P., *Some unsolved problems in graph theory and combinatorial analysis*.
+  Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
+-/
+
+open SimpleGraph
+
+namespace Erdos583
+
+/--
+A subgraph `H` of `G` is a path subgraph if it is the subgraph traced out by a path in `G`,
+i.e. a walk with no repeated vertices.
+-/
+def IsPathSubgraph {V : Type*} {G : SimpleGraph V} (H : G.Subgraph) : Prop :=
+  ∃ (u v : V) (p : G.Walk u v), p.IsPath ∧ H = p.toSubgraph
+
+/--
+`D` is a partition of `G` into edge-disjoint subgraphs: the edge sets of the members of `D`
+are pairwise disjoint and their union is the edge set of `G`.
+-/
+def IsDecomposition {V : Type*} (G : SimpleGraph V) (D : Finset G.Subgraph) : Prop :=
+  Set.PairwiseDisjoint (D : Set G.Subgraph) (fun H ↦ H.edgeSet) ∧
+  (⋃ H ∈ D, H.edgeSet) = G.edgeSet
+
+/--
+Every connected graph on $n$ vertices can be partitioned into at most $\lceil n/2\rceil$
+edge-disjoint paths.
+
+A problem of Erdős and Gallai.
+-/
+theorem erdos_583 {V : Type*} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) :
+    ∃ D : Finset G.Subgraph,
+      (∀ H ∈ D, IsPathSubgraph H) ∧
+      IsDecomposition G D ∧
+      D.card ≤ ⌈(Fintype.card V : ℚ) / 2⌉₊ := by
+  sorry
+
+end Erdos583
diff --git a/apn/data/erdos/Isolated/Erdos713.erdos_713.parts.i.lean b/apn/data/erdos/Isolated/Erdos713.erdos_713.parts.i.lean
new file mode 100644
index 00000000..fd947fe3
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos713.erdos_713.parts.i.lean
@@ -0,0 +1,29 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 713
+
+*References:*
+- [erdosproblems.com/713](https://www.erdosproblems.com/713)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos713
+
+open scoped Classical in
+/--
+Is it true that, for every bipartite graph $G$, there exists some $\alpha\in [1,2)$ and $c>0$ such that\[\mathrm{ex}(n;G)\sim cn^\alpha?\]
+
+The condition that $G$ have at least two edges excludes degenerate forbidden graphs whose
+extremal number is eventually zero, for which the displayed asymptotic with $c>0$ is impossible.
+-/
+theorem erdos_713.parts.i :
+    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
+      ∃ α c : ℝ, α ∈ Set.Ico 1 2 ∧ 0 < c ∧
+        Asymptotics.IsEquivalent atTop
+          (fun n : ℕ => (extremalNumber n G : ℝ))
+          (fun n : ℕ => c * (n : ℝ) ^ α) := by
+  sorry
+
+end Erdos713
diff --git a/apn/data/erdos/Isolated/Erdos713.erdos_713.parts.ii.lean b/apn/data/erdos/Isolated/Erdos713.erdos_713.parts.ii.lean
new file mode 100644
index 00000000..0baaba39
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos713.erdos_713.parts.ii.lean
@@ -0,0 +1,30 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 713
+
+*References:*
+- [erdosproblems.com/713](https://www.erdosproblems.com/713)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos713
+
+open scoped Classical in
+/--
+Must $\alpha$ be rational?
+
+The same nondegeneracy condition on $G$ is used as in part (i). Rationality means that the real
+number $\alpha$ lies in the image of the canonical embedding $\mathbb{Q}\to\mathbb{R}$.
+-/
+theorem erdos_713.parts.ii :
+    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
+      ∀ α c : ℝ, α ∈ Set.Ico 1 2 → 0 < c →
+        Asymptotics.IsEquivalent atTop
+          (fun n : ℕ => (extremalNumber n G : ℝ))
+          (fun n : ℕ => c * (n : ℝ) ^ α) →
+        α ∈ Set.range ((↑) : ℚ → ℝ) := by
+  sorry
+
+end Erdos713
diff --git a/apn/data/erdos/Isolated/Erdos714.erdos_714.lean b/apn/data/erdos/Isolated/Erdos714.erdos_714.lean
new file mode 100644
index 00000000..42847602
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos714.erdos_714.lean
@@ -0,0 +1,23 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 714
+
+*References:*
+- [erdosproblems.com/714](https://www.erdosproblems.com/714)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos714
+
+/--
+Is it true that\[\mathrm{ex}(n; K_{r,r}) \gg n^{2-1/r}?\]
+-/
+theorem erdos_714 :
+    (∀ r : ℕ, 2 ≤ r → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
+      c * (n : ℝ) ^ ((2 : ℝ) - 1 / (r : ℝ)) ≤
+        (extremalNumber n (completeBipartiteGraph (Fin r) (Fin r)) : ℝ)) := by
+  sorry
+
+end Erdos714
diff --git a/apn/data/erdos/Isolated/Erdos773.erdos_773.lean b/apn/data/erdos/Isolated/Erdos773.erdos_773.lean
new file mode 100644
index 00000000..88cb9e75
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos773.erdos_773.lean
@@ -0,0 +1,23 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 773
+
+*Reference:* [erdosproblems.com/773](https://www.erdosproblems.com/773)
+-/
+
+namespace Erdos773
+
+open Filter
+
+/--
+What is the size of the largest Sidon subset $A\subseteq\{1,2^2,\ldots,N^2\}$? Is it $N^{1-o(1)}$?
+-/
+theorem erdos_773 :
+    (∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop,
+      (N : ℝ) ^ (1 - ε) ≤
+        (Finset.maxSidonSubsetCard
+          (Finset.image (fun n : ℕ => n ^ 2) (Finset.Icc 1 N)) : ℝ)) := by
+  sorry
+
+end Erdos773
diff --git a/apn/data/erdos/Isolated/Erdos86.erdos_86.lean b/apn/data/erdos/Isolated/Erdos86.erdos_86.lean
new file mode 100644
index 00000000..5f9b71d7
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos86.erdos_86.lean
@@ -0,0 +1,23 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 86
+
+*Reference:* [erdosproblems.com/86](https://www.erdosproblems.com/86)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos86
+
+/--
+Let $Q_n$ be the $n$-dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Is it true that every subgraph of $Q_n$ with\[\geq \left(\frac{1}{2}+o(1)\right)n2^{n-1}\]many edges contains a $C_4$?
+-/
+theorem erdos_86 :
+    (∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, ∀ H : SimpleGraph (Fin n → Bool),
+      H ≤ hypercube n →
+        (1 / 2 + ε) * n * 2 ^ (n - 1 : ℕ) ≤ (H.edgeSet.ncard : ℝ) →
+          cycleGraph 4 ⊑ H) := by
+  sorry
+
+end Erdos86
diff --git a/apn/data/erdos/Isolated/Erdos970.erdos_970.lean b/apn/data/erdos/Isolated/Erdos970.erdos_970.lean
new file mode 100644
index 00000000..ffc49c64
--- /dev/null
+++ b/apn/data/erdos/Isolated/Erdos970.erdos_970.lean
@@ -0,0 +1,32 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 970
+
+*Reference:* [erdosproblems.com/970](https://www.erdosproblems.com/970)
+-/
+
+namespace Erdos970
+
+/--
+`IsJacobsthalBound k m` says that every interval of `m` consecutive integers contains an
+integer coprime to every positive natural number having at most `k` distinct prime factors.
+-/
+def IsJacobsthalBound (k m : ℕ) : Prop :=
+  ∀ n : ℕ, 0 < n → n.primeFactors.card ≤ k →
+    ∀ a : ℤ, ∃ i : ℕ, i < m ∧ (a + i).natAbs.Coprime n
+
+/--
+Jacobsthal's function, uniformly parametrized by the maximum number of distinct prime factors.
+-/
+noncomputable def jacobsthalFunction (k : ℕ) : ℕ :=
+  sInf {m : ℕ | IsJacobsthalBound k m}
+
+/--
+Let $h(k)$ be Jacobsthal's function, defined to as the minimal $m$ such that, if $n$ has at most $k$ prime factors, then in any set of $m$ consecutive integers there exists an integer coprime to $n$. Determine the order of magnitude of $h(k)$. In particular, is it true that\[h(k) \ll k^2?\]
+-/
+theorem erdos_970 :
+    (∃ C > (0 : ℝ), ∀ k : ℕ, 0 < k → (jacobsthalFunction k : ℝ) ≤ C * k ^ 2) := by
+  sorry
+
+end Erdos970
diff --git a/apn/data/erdos/Sources/1020.lean b/apn/data/erdos/Sources/1020.lean
new file mode 100644
index 00000000..a926c638
--- /dev/null
+++ b/apn/data/erdos/Sources/1020.lean
@@ -0,0 +1,37 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1020
+
+*Reference:* [erdosproblems.com/1020](https://www.erdosproblems.com/1020)
+-/
+
+namespace Erdos1020
+
+/-- The maximum number of edges in an `r`-uniform hypergraph on `n` vertices containing no
+matching of size `k` (i.e. no `k` pairwise vertex-disjoint edges). -/
+noncomputable def f (n r k : ℕ) : ℕ :=
+  open scoped Classical in
+  let candidates :=
+    (((Finset.univ : Finset (Fin n)).powersetCard r).powerset).filter fun H ↦
+      ¬ ∃ M : Finset (Finset (Fin n)),
+          M ⊆ H ∧ M.card = k ∧ (M : Set (Finset (Fin n))).PairwiseDisjoint id
+  candidates.sup Finset.card
+
+/--
+Let $f(n;r,k)$ be the maximal number of edges in an $r$-uniform hypergraph which contains no set of $k$ many independent edges. 
+
+For all $r\geq 3$,\[f(n;r,k)=\max\left(\binom{rk-1}{r}, \binom{n}{r}-\binom{n-k+1}{r}\right).\]
+
+Note: the displayed formula is stated on the standard Erdős matching conjecture range
+`k ≥ 1` and `n ≥ r*k - 1`; with fully unrestricted `n` the equality is trivially false
+(e.g. `r = 3`, `k = 2`, `n = 4`), and for `n < r*k - 1` the source remarks the problem
+is trivial (the complete `r`-uniform hypergraph has no `k`-matching).
+-/
+@[category research open, AMS 5]
+theorem erdos_1020 :
+    ∀ (r : ℕ), 3 ≤ r → ∀ n k : ℕ, 0 < k → r * k - 1 ≤ n →
+      f n r k = max ((r * k - 1).choose r) (n.choose r - (n - k + 1).choose r) := by
+  sorry
+
+end Erdos1020
diff --git a/apn/data/erdos/Sources/104.lean b/apn/data/erdos/Sources/104.lean
new file mode 100644
index 00000000..ad55c961
--- /dev/null
+++ b/apn/data/erdos/Sources/104.lean
@@ -0,0 +1,36 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 104
+
+*Reference:* [erdosproblems.com/104](https://www.erdosproblems.com/104)
+-/
+
+open Filter
+open scoped EuclideanGeometry
+
+namespace Erdos104
+
+open EuclideanGeometry
+
+/-- The number of distinct unit circles containing at least three points of `P`. -/
+noncomputable def unitCircleCount (P : Finset ℝ²) : ℕ :=
+  Set.ncard {s : Sphere ℝ² | s.radius = 1 ∧ 3 ≤ {p ∈ (P : Set ℝ²) | p ∈ s}.ncard}
+
+/-- The set of unit-circle counts attained by configurations of `n` points in the plane. -/
+noncomputable def possibleUnitCircleCounts (n : ℕ) : Set ℕ :=
+  {k | ∃ P : Finset ℝ², P.card = n ∧ unitCircleCount P = k}
+
+/-- The maximum number of qualifying unit circles attained by a configuration of `n` points. -/
+noncomputable def maxUnitCircleCount (n : ℕ) : ℕ :=
+  sSup (possibleUnitCircleCounts n)
+
+/--
+Given $n$ points in $\mathbb{R}^2$ the number of distinct unit circles containing at least three points is $o(n^2)$.
+-/
+@[category research open, AMS 52]
+theorem erdos_104 :
+    (fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2) := by
+  sorry
+
+end Erdos104
diff --git a/apn/data/erdos/Sources/1083.lean b/apn/data/erdos/Sources/1083.lean
new file mode 100644
index 00000000..00fe2cc5
--- /dev/null
+++ b/apn/data/erdos/Sources/1083.lean
@@ -0,0 +1,31 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1083
+
+*Reference:* [erdosproblems.com/1083](https://www.erdosproblems.com/1083)
+-/
+
+open Filter
+
+namespace Erdos1083
+
+/--
+The minimum number of distinct distances determined by an $n$-point subset of
+$d$-dimensional Euclidean space.
+-/
+noncomputable def f (d n : ℕ) : ℕ :=
+  sInf {m : ℕ | ∃ points : Finset (EuclideanSpace ℝ (Fin d)),
+    points.card = n ∧ distinctDistances points = m}
+
+/--
+Let $d\geq 3$, and let $f_d(n)$ be the minimal $m$ such that every set of $n$ points in $\mathbb{R}^d$ determines at least $m$ distinct distances. Estimate $f_d(n)$ - in particular, is it true that\[f_d(n)=n^{\frac{2}{d}-o(1)}?\]
+-/
+@[category research open, AMS 52]
+theorem erdos_1083 :
+    (∀ d : ℕ, 3 ≤ d → ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
+      ∀ᶠ n : ℕ in atTop,
+        (f d n : ℝ) = (n : ℝ) ^ ((2 : ℝ) / (d : ℝ) - o n)) := by
+  sorry
+
+end Erdos1083
diff --git a/apn/data/erdos/Sources/1159.lean b/apn/data/erdos/Sources/1159.lean
new file mode 100644
index 00000000..a3c77218
--- /dev/null
+++ b/apn/data/erdos/Sources/1159.lean
@@ -0,0 +1,27 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1159
+
+*Reference:*
+- [erdosproblems.com/1159](https://www.erdosproblems.com/1159)
+-/
+
+open Configuration
+
+namespace Erdos1159
+
+/--
+Determine whether there exists a constant $C>1$ such that the following holds.
+
+Let $P$ be a finite <a href="https://en.wikipedia.org/wiki/Projective_plane" rel="nofollow noopener noreferrer ugc" target="_blank">projective plane</a>. Must there exist a set of points $S$ such that $1\leq \lvert S\cap \ell\rvert \leq C$ for all lines $\ell$?
+-/
+@[category research open, AMS 5 51]
+theorem erdos_1159 :
+    (∃ C : ℕ, 1 < C ∧
+      ∀ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L),
+        ∀ _ : ProjectivePlane P L, ∃ S : Set P, ∀ l : L,
+          1 ≤ (S ∩ {p : P | p ∈ l}).ncard ∧ (S ∩ {p : P | p ∈ l}).ncard ≤ C) := by
+  sorry
+
+end Erdos1159
diff --git a/apn/data/erdos/Sources/1206.lean b/apn/data/erdos/Sources/1206.lean
new file mode 100644
index 00000000..1e260532
--- /dev/null
+++ b/apn/data/erdos/Sources/1206.lean
@@ -0,0 +1,30 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1206
+
+*Reference:* [erdosproblems.com/1206](https://www.erdosproblems.com/1206)
+-/
+
+namespace Erdos1206
+
+/--
+Does $\{1,2^3,\ldots,N^3\}$ contain a Sidon set of size $\gg N$?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_1206.parts.i :
+    ∃ c : ℝ, 0 < c ∧ ∀ᶠ N in Filter.atTop, ∃ S : Finset ℕ,
+      S ⊆ (Finset.Icc 1 N).image (fun n => n ^ 3) ∧
+      IsSidon (S : Set ℕ) ∧ c * (N : ℝ) ≤ (S.card : ℝ) := by
+  sorry
+
+/--
+Is there an infinite set $A\subset \mathbb{N}$ of positive density such that $\{a^3 : a\in A\}$ is a Sidon set?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_1206.parts.ii :
+    ∃ A : Set ℕ, A.Infinite ∧ 0 < A.lowerDensity ∧
+      IsSidon ((fun a : ℕ => a ^ 3) '' A) := by
+  sorry
+
+end Erdos1206
diff --git a/apn/data/erdos/Sources/1207.lean b/apn/data/erdos/Sources/1207.lean
new file mode 100644
index 00000000..bb0edfe1
--- /dev/null
+++ b/apn/data/erdos/Sources/1207.lean
@@ -0,0 +1,34 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1207
+
+*Reference:* [erdosproblems.com/1207](https://www.erdosproblems.com/1207)
+-/
+
+open Filter
+
+namespace Erdos1207
+
+/-- A set is isosceles-free if no three distinct points in it form an isosceles triangle. -/
+def IsIsoscelesFree {α : Type*} [Dist α] (A : Set α) : Prop :=
+  A.Triplewise fun x y z => ¬ IsIsosceles x y z
+
+/--
+`P d n` is the largest number such that every set of `n` points in Euclidean `d`-space has an
+isosceles-free subset of at least that size.
+-/
+noncomputable def P (d n : ℕ) : ℕ :=
+  sInf {m : ℕ | ∃ S : Finset (EuclideanSpace ℝ (Fin d)), S.card = n ∧
+    m = sSup {k : ℕ | ∃ A : Finset (EuclideanSpace ℝ (Fin d)),
+      A ⊆ S ∧ IsIsoscelesFree (A : Set (EuclideanSpace ℝ (Fin d))) ∧ A.card = k}}
+
+/--
+Let $P_d(n)$ be such that in any set of $n$ points in $\mathbb{R}^d$ there exist at least $P_d(n)$ many points which do not contain an isosceles triangle. Estimate $P_d(n)$ - in particular, is it true that\[P_2(n)<n^{1-c}\]for some constant $c>0$?
+-/
+@[category research open, AMS 52]
+theorem erdos_1207 :
+    (∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (P 2 n : ℝ) < (n : ℝ) ^ (1 - c)) := by
+  sorry
+
+end Erdos1207
diff --git a/apn/data/erdos/Sources/181.lean b/apn/data/erdos/Sources/181.lean
new file mode 100644
index 00000000..690db298
--- /dev/null
+++ b/apn/data/erdos/Sources/181.lean
@@ -0,0 +1,28 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 181
+
+*Reference:* [erdosproblems.com/181](https://www.erdosproblems.com/181)
+-/
+
+namespace Erdos181
+
+open SimpleGraph
+
+/-- The diagonal Ramsey number of a finite graph `G`: the least `N` such that every red-blue
+colouring of the edges of the complete graph on `N` vertices contains a monochromatic copy of `G`.
+A graph `R` records the red edges, and `Rᶜ` records the blue edges. -/
+noncomputable def diagonalRamseyNumber {α : Type*} [Fintype α] (G : SimpleGraph α) : ℕ :=
+  sInf {N : ℕ | ∀ R : SimpleGraph (Fin N), G.IsContained R ∨ G.IsContained Rᶜ}
+
+/--
+Let $Q_n$ be the $n$-dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Prove that\[R(Q_n) \ll 2^n.\]
+-/
+@[category research open, AMS 5]
+theorem erdos_181 :
+    ∃ C > (0 : ℝ), ∀ n : ℕ,
+      (diagonalRamseyNumber (hypercube n) : ℝ) ≤ C * 2 ^ n := by
+  sorry
+
+end Erdos181
diff --git a/apn/data/erdos/Sources/322.lean b/apn/data/erdos/Sources/322.lean
new file mode 100644
index 00000000..c0aa13cf
--- /dev/null
+++ b/apn/data/erdos/Sources/322.lean
@@ -0,0 +1,26 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 322
+
+*Reference:* [erdosproblems.com/322](https://www.erdosproblems.com/322)
+-/
+
+namespace Erdos322
+
+/-- For `k ≥ 3`, the number of ordered representations of `n` as a sum of `k` many `k`th
+powers of nonnegative integers. The bases can be restricted to the interval from `0` to `n`. -/
+def representationCount (k n : ℕ) : ℕ :=
+  ((Finset.univ : Finset (Fin k → Fin (n + 1))).filter
+    (fun a ↦ ∑ i, (a i : ℕ) ^ k = n)).card
+
+/--
+Let $k\geq 3$ and $A\subset \mathbb{N}$ be the set of $k$th powers. What is the order of growth of $1_A^{(k)}(n)$, i.e. the number of representations of $n$ as the sum of $k$ many $k$th powers? Does there exist some $c>0$ and infinitely many $n$ such that\[1_A^{(k)}(n) >n^c?\]
+-/
+@[category research open, AMS 11]
+theorem erdos_322 :
+    (∀ k : ℕ, 3 ≤ k → ∃ c > (0 : ℝ),
+      {n : ℕ | (n : ℝ) ^ c < representationCount k n}.Infinite) := by
+  sorry
+
+end Erdos322
diff --git a/apn/data/erdos/Sources/431.lean b/apn/data/erdos/Sources/431.lean
new file mode 100644
index 00000000..f9cfc7b9
--- /dev/null
+++ b/apn/data/erdos/Sources/431.lean
@@ -0,0 +1,22 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 431
+
+*Reference:* [erdosproblems.com/431](https://www.erdosproblems.com/431)
+-/
+
+open scoped Pointwise
+
+namespace Erdos431
+
+/--
+Are there two infinite sets $A$ and $B$ such that $A+B$ agrees with the set of prime numbers up to finitely many exceptions?
+-/
+@[category research open, AMS 11]
+theorem erdos_431 :
+    (∃ A B : Set ℕ, A.Infinite ∧ B.Infinite ∧
+      (symmDiff (A + B) {p : ℕ | p.Prime}).Finite) := by
+  sorry
+
+end Erdos431
diff --git a/apn/data/erdos/Sources/478.lean b/apn/data/erdos/Sources/478.lean
new file mode 100644
index 00000000..6bbf92f0
--- /dev/null
+++ b/apn/data/erdos/Sources/478.lean
@@ -0,0 +1,24 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 478
+
+*Reference:* [erdosproblems.com/478](https://www.erdosproblems.com/478)
+-/
+
+namespace Erdos478
+
+/--
+Let $p$ be a prime and\[A_p = \{ k! \pmod{p} : 1\leq k<p\}.\]Is it true that\[\lvert A_p\rvert \sim (1-\tfrac{1}{e})p?\]
+-/
+@[category research open, AMS 11]
+theorem erdos_478 :
+    Filter.Tendsto
+      (fun p : ℕ =>
+        (((Finset.Ico 1 p).image (fun k => Nat.factorial k % p)).card : ℝ) / p)
+      (Filter.atTop ⊓ Filter.principal {p : ℕ | p.Prime})
+      (nhds (1 - 1 / Real.exp 1))
+      := by
+  sorry
+
+end Erdos478
diff --git a/apn/data/erdos/Sources/548.lean b/apn/data/erdos/Sources/548.lean
new file mode 100644
index 00000000..fdbf8997
--- /dev/null
+++ b/apn/data/erdos/Sources/548.lean
@@ -0,0 +1,23 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 548
+
+*Reference:* [erdosproblems.com/548](https://www.erdosproblems.com/548)
+-/
+
+open SimpleGraph
+
+namespace Erdos548
+
+/--
+Let $n\geq k+1$. Every graph on $n$ vertices with at least $\frac{k-1}{2}n+1$ edges contains every tree on $k+1$ vertices.
+-/
+@[category research open, AMS 5]
+theorem erdos_548 :
+    ∀ (n k : ℕ), k + 1 ≤ n → ∀ G : SimpleGraph (Fin n),
+      ((k : ℚ) - 1) / 2 * n + 1 ≤ (G.edgeSet.ncard : ℚ) →
+        ∀ T : SimpleGraph (Fin (k + 1)), T.IsTree → T.IsContained G := by
+  sorry
+
+end Erdos548
diff --git a/apn/data/erdos/Sources/571.lean b/apn/data/erdos/Sources/571.lean
new file mode 100644
index 00000000..30389ac3
--- /dev/null
+++ b/apn/data/erdos/Sources/571.lean
@@ -0,0 +1,26 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 571
+
+*References:*
+- [erdosproblems.com/571](https://www.erdosproblems.com/571)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos571
+
+/--
+Show that for any rational $\alpha \in [1,2)$ there exists a bipartite graph $G$ such that\[\mathrm{ex}(n;G)\asymp n^{\alpha}.\]
+-/
+@[category research open, AMS 5]
+theorem erdos_571 :
+    ∀ α : ℚ, 1 ≤ α → α < 2 →
+      ∃ q : ℕ, ∃ G : SimpleGraph (Fin q), G.IsBipartite ∧
+        Asymptotics.IsTheta atTop
+          (fun n : ℕ => (extremalNumber n G : ℝ))
+          (fun n : ℕ => (n : ℝ) ^ (α : ℝ)) := by
+  sorry
+
+end Erdos571
diff --git a/apn/data/erdos/Sources/583.lean b/apn/data/erdos/Sources/583.lean
new file mode 100644
index 00000000..597fabdd
--- /dev/null
+++ b/apn/data/erdos/Sources/583.lean
@@ -0,0 +1,45 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 583
+
+*References:*
+- [erdosproblems.com/583](https://www.erdosproblems.com/583)
+- [Er71] Erdős, P., *Some unsolved problems in graph theory and combinatorial analysis*.
+  Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
+-/
+
+open SimpleGraph
+
+namespace Erdos583
+
+/--
+A subgraph `H` of `G` is a path subgraph if it is the subgraph traced out by a path in `G`,
+i.e. a walk with no repeated vertices.
+-/
+def IsPathSubgraph {V : Type*} {G : SimpleGraph V} (H : G.Subgraph) : Prop :=
+  ∃ (u v : V) (p : G.Walk u v), p.IsPath ∧ H = p.toSubgraph
+
+/--
+`D` is a partition of `G` into edge-disjoint subgraphs: the edge sets of the members of `D`
+are pairwise disjoint and their union is the edge set of `G`.
+-/
+def IsDecomposition {V : Type*} (G : SimpleGraph V) (D : Finset G.Subgraph) : Prop :=
+  Set.PairwiseDisjoint (D : Set G.Subgraph) (fun H ↦ H.edgeSet) ∧
+  (⋃ H ∈ D, H.edgeSet) = G.edgeSet
+
+/--
+Every connected graph on $n$ vertices can be partitioned into at most $\lceil n/2\rceil$
+edge-disjoint paths.
+
+A problem of Erdős and Gallai.
+-/
+@[category research open, AMS 5]
+theorem erdos_583 {V : Type*} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) :
+    ∃ D : Finset G.Subgraph,
+      (∀ H ∈ D, IsPathSubgraph H) ∧
+      IsDecomposition G D ∧
+      D.card ≤ ⌈(Fintype.card V : ℚ) / 2⌉₊ := by
+  sorry
+
+end Erdos583
diff --git a/apn/data/erdos/Sources/713.lean b/apn/data/erdos/Sources/713.lean
new file mode 100644
index 00000000..9121f75d
--- /dev/null
+++ b/apn/data/erdos/Sources/713.lean
@@ -0,0 +1,47 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 713
+
+*References:*
+- [erdosproblems.com/713](https://www.erdosproblems.com/713)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos713
+
+open scoped Classical in
+/--
+Is it true that, for every bipartite graph $G$, there exists some $\alpha\in [1,2)$ and $c>0$ such that\[\mathrm{ex}(n;G)\sim cn^\alpha?\]
+
+The condition that $G$ have at least two edges excludes degenerate forbidden graphs whose
+extremal number is eventually zero, for which the displayed asymptotic with $c>0$ is impossible.
+-/
+@[category research open, AMS 5]
+theorem erdos_713.parts.i :
+    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
+      ∃ α c : ℝ, α ∈ Set.Ico 1 2 ∧ 0 < c ∧
+        Asymptotics.IsEquivalent atTop
+          (fun n : ℕ => (extremalNumber n G : ℝ))
+          (fun n : ℕ => c * (n : ℝ) ^ α) := by
+  sorry
+
+open scoped Classical in
+/--
+Must $\alpha$ be rational?
+
+The same nondegeneracy condition on $G$ is used as in part (i). Rationality means that the real
+number $\alpha$ lies in the image of the canonical embedding $\mathbb{Q}\to\mathbb{R}$.
+-/
+@[category research open, AMS 5]
+theorem erdos_713.parts.ii :
+    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
+      ∀ α c : ℝ, α ∈ Set.Ico 1 2 → 0 < c →
+        Asymptotics.IsEquivalent atTop
+          (fun n : ℕ => (extremalNumber n G : ℝ))
+          (fun n : ℕ => c * (n : ℝ) ^ α) →
+        α ∈ Set.range ((↑) : ℚ → ℝ) := by
+  sorry
+
+end Erdos713
diff --git a/apn/data/erdos/Sources/714.lean b/apn/data/erdos/Sources/714.lean
new file mode 100644
index 00000000..f4552eb1
--- /dev/null
+++ b/apn/data/erdos/Sources/714.lean
@@ -0,0 +1,24 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 714
+
+*References:*
+- [erdosproblems.com/714](https://www.erdosproblems.com/714)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos714
+
+/--
+Is it true that\[\mathrm{ex}(n; K_{r,r}) \gg n^{2-1/r}?\]
+-/
+@[category research open, AMS 5]
+theorem erdos_714 :
+    (∀ r : ℕ, 2 ≤ r → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
+      c * (n : ℝ) ^ ((2 : ℝ) - 1 / (r : ℝ)) ≤
+        (extremalNumber n (completeBipartiteGraph (Fin r) (Fin r)) : ℝ)) := by
+  sorry
+
+end Erdos714
diff --git a/apn/data/erdos/Sources/773.lean b/apn/data/erdos/Sources/773.lean
new file mode 100644
index 00000000..a3c6f9a6
--- /dev/null
+++ b/apn/data/erdos/Sources/773.lean
@@ -0,0 +1,24 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 773
+
+*Reference:* [erdosproblems.com/773](https://www.erdosproblems.com/773)
+-/
+
+namespace Erdos773
+
+open Filter
+
+/--
+What is the size of the largest Sidon subset $A\subseteq\{1,2^2,\ldots,N^2\}$? Is it $N^{1-o(1)}$?
+-/
+@[category research open, AMS 11]
+theorem erdos_773 :
+    (∀ ε > (0 : ℝ), ∀ᶠ N : ℕ in atTop,
+      (N : ℝ) ^ (1 - ε) ≤
+        (Finset.maxSidonSubsetCard
+          (Finset.image (fun n : ℕ => n ^ 2) (Finset.Icc 1 N)) : ℝ)) := by
+  sorry
+
+end Erdos773
diff --git a/apn/data/erdos/Sources/86.lean b/apn/data/erdos/Sources/86.lean
new file mode 100644
index 00000000..7f33b673
--- /dev/null
+++ b/apn/data/erdos/Sources/86.lean
@@ -0,0 +1,24 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 86
+
+*Reference:* [erdosproblems.com/86](https://www.erdosproblems.com/86)
+-/
+
+open Filter SimpleGraph
+
+namespace Erdos86
+
+/--
+Let $Q_n$ be the $n$-dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Is it true that every subgraph of $Q_n$ with\[\geq \left(\frac{1}{2}+o(1)\right)n2^{n-1}\]many edges contains a $C_4$?
+-/
+@[category research open, AMS 5]
+theorem erdos_86 :
+    (∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, ∀ H : SimpleGraph (Fin n → Bool),
+      H ≤ hypercube n →
+        (1 / 2 + ε) * n * 2 ^ (n - 1 : ℕ) ≤ (H.edgeSet.ncard : ℝ) →
+          cycleGraph 4 ⊑ H) := by
+  sorry
+
+end Erdos86
diff --git a/apn/data/erdos/Sources/970.lean b/apn/data/erdos/Sources/970.lean
new file mode 100644
index 00000000..729a646c
--- /dev/null
+++ b/apn/data/erdos/Sources/970.lean
@@ -0,0 +1,33 @@
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 970
+
+*Reference:* [erdosproblems.com/970](https://www.erdosproblems.com/970)
+-/
+
+namespace Erdos970
+
+/--
+`IsJacobsthalBound k m` says that every interval of `m` consecutive integers contains an
+integer coprime to every positive natural number having at most `k` distinct prime factors.
+-/
+def IsJacobsthalBound (k m : ℕ) : Prop :=
+  ∀ n : ℕ, 0 < n → n.primeFactors.card ≤ k →
+    ∀ a : ℤ, ∃ i : ℕ, i < m ∧ (a + i).natAbs.Coprime n
+
+/--
+Jacobsthal's function, uniformly parametrized by the maximum number of distinct prime factors.
+-/
+noncomputable def jacobsthalFunction (k : ℕ) : ℕ :=
+  sInf {m : ℕ | IsJacobsthalBound k m}
+
+/--
+Let $h(k)$ be Jacobsthal's function, defined to as the minimal $m$ such that, if $n$ has at most $k$ prime factors, then in any set of $m$ consecutive integers there exists an integer coprime to $n$. Determine the order of magnitude of $h(k)$. In particular, is it true that\[h(k) \ll k^2?\]
+-/
+@[category research open, AMS 11]
+theorem erdos_970 :
+    (∃ C > (0 : ℝ), ∀ k : ℕ, 0 < k → (jacobsthalFunction k : ℝ) ≤ C * k ^ 2) := by
+  sorry
+
+end Erdos970
diff --git a/apn/data/erdos/samples.jsonl b/apn/data/erdos/samples.jsonl
index 00ae555d..ec8e0cff 100644
--- a/apn/data/erdos/samples.jsonl
+++ b/apn/data/erdos/samples.jsonl
@@ -142,3 +142,23 @@
 {"id": "Erdos975.erdos_975.variants.n2_plus_1_strong", "source": "Sources/975.lean", "erdos_number": 975, "category_at_pin": "research solved", "answer_form": null}
 {"id": "Erdos975.erdos_975.variants.quadratic", "source": "Sources/975.lean", "excluded": "value-typed answer(sorry): the placeholder elaborates to a position-labeled sorryAx in the statement's type, so the statement cannot be closed (or even stated) without the paper's google.answer \"with_auxiliary\" machinery, and SafeVerify cannot score it", "erdos_number": 975, "category_at_pin": "research solved"}
 {"id": "Erdos975.erdos_975.variants.upper_bound", "source": "Sources/975.lean", "erdos_number": 975, "category_at_pin": "research solved", "answer_form": null}
+{"id": "Erdos86.erdos_86", "source": "Sources/86.lean", "erdos_number": 86, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos104.erdos_104", "source": "Sources/104.lean", "erdos_number": 104, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos181.erdos_181", "source": "Sources/181.lean", "erdos_number": 181, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos322.erdos_322", "source": "Sources/322.lean", "erdos_number": 322, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos431.erdos_431", "source": "Sources/431.lean", "erdos_number": 431, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos478.erdos_478", "source": "Sources/478.lean", "erdos_number": 478, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos548.erdos_548", "source": "Sources/548.lean", "erdos_number": 548, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos571.erdos_571", "source": "Sources/571.lean", "erdos_number": 571, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos583.erdos_583", "source": "Sources/583.lean", "erdos_number": 583, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos713.erdos_713.parts.i", "source": "Sources/713.lean", "erdos_number": 713, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos713.erdos_713.parts.ii", "source": "Sources/713.lean", "erdos_number": 713, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos714.erdos_714", "source": "Sources/714.lean", "erdos_number": 714, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos773.erdos_773", "source": "Sources/773.lean", "erdos_number": 773, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos970.erdos_970", "source": "Sources/970.lean", "erdos_number": 970, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos1020.erdos_1020", "source": "Sources/1020.lean", "erdos_number": 1020, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos1083.erdos_1083", "source": "Sources/1083.lean", "erdos_number": 1083, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos1159.erdos_1159", "source": "Sources/1159.lean", "erdos_number": 1159, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos1206.erdos_1206.parts.i", "source": "Sources/1206.lean", "erdos_number": 1206, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos1206.erdos_1206.parts.ii", "source": "Sources/1206.lean", "erdos_number": 1206, "category_at_pin": "research open", "answer_form": null}
+{"id": "Erdos1207.erdos_1207", "source": "Sources/1207.lean", "erdos_number": 1207, "category_at_pin": "research open", "answer_form": null}
diff --git a/apn/data/erdos/subsets/target18.json b/apn/data/erdos/subsets/target18.json
new file mode 100644
index 00000000..34705707
--- /dev/null
+++ b/apn/data/erdos/subsets/target18.json
@@ -0,0 +1,25 @@
+{
+  "description": "The 18 Erdős problems from the 2026-08-25 autoformalization target run (epoch-research/autoformalization results/2026-08-25-erdos-target-run): problems absent from google-deepmind/formal-conjectures, autoformalized and gate-passed at FC 9cbe1d3c (1020 from hold/, the rest from submit/). 20 statements: 713 and 1206 each have two parts. Throwaway smoke-run subset -- a solve at a modest budget is a misformalization red flag.",
+  "ids": [
+    "Erdos86.erdos_86",
+    "Erdos104.erdos_104",
+    "Erdos181.erdos_181",
+    "Erdos322.erdos_322",
+    "Erdos431.erdos_431",
+    "Erdos478.erdos_478",
+    "Erdos548.erdos_548",
+    "Erdos571.erdos_571",
+    "Erdos583.erdos_583",
+    "Erdos713.erdos_713.parts.i",
+    "Erdos713.erdos_713.parts.ii",
+    "Erdos714.erdos_714",
+    "Erdos773.erdos_773",
+    "Erdos970.erdos_970",
+    "Erdos1020.erdos_1020",
+    "Erdos1083.erdos_1083",
+    "Erdos1159.erdos_1159",
+    "Erdos1206.erdos_1206.parts.i",
+    "Erdos1206.erdos_1206.parts.ii",
+    "Erdos1207.erdos_1207"
+  ]
+}
diff --git a/configs/erdos-target18-smoke.yaml b/configs/erdos-target18-smoke.yaml
new file mode 100644
index 00000000..03cbc94d
--- /dev/null
+++ b/configs/erdos-target18-smoke.yaml
@@ -0,0 +1,86 @@
+# Schema reference for eval-set config:
+# https://github.com/METR/hawk/blob/main/hawk/api/EvalSetConfig.schema.json
+#
+# THROWAWAY misformalization smoke run: the 18 Erdős problems autoformalized in
+# the 2026-08-25 autoformalization target run (epoch-research/autoformalization
+# results/2026-08-25-erdos-target-run; 20 statements -- 713 and 1206 have two
+# parts each), vendored into apn/data/erdos on the erdos-target-smoke branch
+# (stacked on PR #28). These are open problems: a solve at a modest $50/sample
+# budget is a red flag that the statement was misformalized (too easy), not a
+# mathematical breakthrough.
+#
+# COST (2 models x 20 statements x 1 epoch = 40 samples, $50/sample cap):
+#   Max: 40 x $50 = $2,000 hard ceiling; expected near max (open problems --
+#   most samples should burn the cap without a solve).
+retry_attempts: 0
+
+tasks:
+  - package: git+ssh://git@github.com/epoch-research/LeanOpenProblems.git@erdos-target-smoke
+    name: apn
+    items:
+      - name: apn_erdos
+        args:
+          subset: target18
+
+name: erdos-target18-smoke
+epochs: 1
+models:
+  # Epoch model wrappers (bypass middleman): API keys come straight from the
+  # secrets below; max_tokens/context window come from the package's models.yaml.
+  - package: git+https://github.com/epoch-research/benchmarks@giles-hawkbench-newstuff
+    name: epoch
+    items:
+      - name: claude-fable-5
+        args:
+          config:
+            reasoning_effort: "high"
+            max_retries: 7
+            # max_sandboxes isn't user-settable; Hawk sizes it as
+            # 2 x sum(max_connections) across providers
+            max_connections: 40
+      - name: gpt-5.6-sol
+        args:
+          config:
+            # Defaults to 'none' in GPT 5.4
+            reasoning_effort: "high"
+            max_retries: 7
+            max_connections: 40
+
+# Per-sample spend cap -- the real budget.
+cost_limit: 50.0
+working_limit: 43_200  # 12h
+
+# Prices in dollars per 1M tokens (match the epoch package's models.yaml).
+# Keys must match Inspect's resolved <provider>/<model> names.
+model_cost_config:
+  epoch/claude-fable-5:
+    input: 10.0
+    output: 50.0
+    input_cache_read: 1.0
+    input_cache_write: 12.5
+  epoch/gpt-5.6-sol:
+    input: 5.0
+    output: 30.0
+    input_cache_read: 0.5
+    input_cache_write: 6.25
+
+secrets:
+  - name: ANTHROPIC_API_KEY
+  - name: OPENAI_API_KEY
+  - name: GOOGLE_API_KEY
+  - name: LEAN_OPEN_PROBLEMS_IMAGE_NAME
+    description: "The ECR repo containing the LeanOpenProblems sandbox images"
+
+runner:
+  memory: 200Gi
+  environment:
+    # TODO: Remove once default in Hawk
+    INSPECT_LOG_CONDENSE: "true"
+    ANTHROPIC_BASE_URL: https://api.anthropic.com
+    OPENAI_BASE_URL: https://api.openai.com/v1
+    GOOGLE_BASE_URL: https://generativelanguage.googleapis.com
+    HAWK_RUNNER_REFRESH_CLIENT_ID: ""
+    HAWK_RUNNER_REFRESH_TOKEN: ''
+
+packages:
+  - inspect-ai==0.3.245