THROWAWAY: smoke-run the 2026-08-25 autoformalization target problems (misformalization check)

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

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

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

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

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

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

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

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

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

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

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

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

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

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