From 222956579b66eefacc96ab9921352ef4b1396197 Mon Sep 17 00:00:00 2001
From: Will Blair <85643015+willblair0708@users.noreply.github.com>
Date: Fri, 3 Jul 2026 12:35:01 -0400
Subject: [PATCH 1/4] ErdosProblems: add 71, 206, 209, 328, 353, 403, 426, 464,
 512, 621, 639, 648 (#3998 sync)

---
 FormalConjectures/ErdosProblems/206.lean |  93 +++++++++++++++
 FormalConjectures/ErdosProblems/209.lean |  71 ++++++++++++
 FormalConjectures/ErdosProblems/328.lean |  57 ++++++++++
 FormalConjectures/ErdosProblems/353.lean | 139 +++++++++++++++++++++++
 FormalConjectures/ErdosProblems/403.lean |  54 +++++++++
 FormalConjectures/ErdosProblems/426.lean |  75 ++++++++++++
 FormalConjectures/ErdosProblems/464.lean |  82 +++++++++++++
 FormalConjectures/ErdosProblems/512.lean |  49 ++++++++
 FormalConjectures/ErdosProblems/621.lean |  65 +++++++++++
 FormalConjectures/ErdosProblems/639.lean |  60 ++++++++++
 FormalConjectures/ErdosProblems/648.lean |  68 +++++++++++
 FormalConjectures/ErdosProblems/71.lean  |  53 +++++++++
 12 files changed, 866 insertions(+)
 create mode 100644 FormalConjectures/ErdosProblems/206.lean
 create mode 100644 FormalConjectures/ErdosProblems/209.lean
 create mode 100644 FormalConjectures/ErdosProblems/328.lean
 create mode 100644 FormalConjectures/ErdosProblems/353.lean
 create mode 100644 FormalConjectures/ErdosProblems/403.lean
 create mode 100644 FormalConjectures/ErdosProblems/426.lean
 create mode 100644 FormalConjectures/ErdosProblems/464.lean
 create mode 100644 FormalConjectures/ErdosProblems/512.lean
 create mode 100644 FormalConjectures/ErdosProblems/621.lean
 create mode 100644 FormalConjectures/ErdosProblems/639.lean
 create mode 100644 FormalConjectures/ErdosProblems/648.lean
 create mode 100644 FormalConjectures/ErdosProblems/71.lean

diff --git a/FormalConjectures/ErdosProblems/206.lean b/FormalConjectures/ErdosProblems/206.lean
new file mode 100644
index 0000000000..8f991e9ecb
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/206.lean
@@ -0,0 +1,93 @@
+/-
+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 206
+
+*References:*
+- [erdosproblems.com/206](https://www.erdosproblems.com/206)
+- [Ko24b] Kovač, V., *On eventually greedy best underapproximations by Egyptian fractions*.
+  arXiv:2406.07218 (2024).
+-/
+
+open MeasureTheory
+
+namespace Erdos206
+
+/- Formalization notes:
+- The problem's greedy recursion ($R_{n+1}(x)=R_n(x)+1/m$ with $m$ minimal such that $m$ does
+  not appear in $R_n(x)$ and the right-hand side is $<x$) is rendered as `EventuallyGreedy`:
+  from some `n₀` on, the best `n`-term underapproximations form a nested chain given by the
+  prefixes of a single strictly increasing sequence of denominators. The two are equivalent:
+  if `S` is a best `n`-term underapproximation and `S ∪ {m}` a best `(n+1)`-term one, then `m`
+  is forced to be the least `k ∉ S` with `egyptianSum S + 1/k < x` (a smaller admissible `k`
+  would give a strictly larger `(n+1)`-term underapproximation), and conversely the greedy
+  recursion produces exactly such a nested chain, with the appended denominators strictly
+  increasing and exceeding `max S` (else swapping out `max S` would improve `S`).
+- "for almost all $x$" is rendered as `∀ᵐ` with respect to Lebesgue measure restricted to
+  $(0,\infty)$.
+-/
+
+/-- The Egyptian fraction sum: `∑_{m ∈ S} 1/m` for a finset of natural numbers. -/
+noncomputable def egyptianSum (S : Finset ℕ) : ℝ :=
+  S.sum (fun m => (1 : ℝ) / m)
+
+/-- All elements of the finset are positive (valid denominators). -/
+def ValidEgyptian (S : Finset ℕ) : Prop :=
+  ∀ m ∈ S, 0 < m
+
+/-- `S` is an Egyptian underapproximation of `x`: valid denominators and sum < x. -/
+def IsUnderapprox (S : Finset ℕ) (x : ℝ) : Prop :=
+  ValidEgyptian S ∧ egyptianSum S < x
+
+/-- `S` achieves the best `n`-term Egyptian underapproximation of `x`,
+i.e. `egyptianSum S` realises $R_n(x)$. -/
+def IsBestNTerm (S : Finset ℕ) (n : ℕ) (x : ℝ) : Prop :=
+  S.card = n ∧ IsUnderapprox S x ∧
+    ∀ T : Finset ℕ, T.card = n → IsUnderapprox T x → egyptianSum T ≤ egyptianSum S
+
+/-- `x` has eventually greedy best Egyptian underapproximations: from some `n₀` on, the best
+`n`-term underapproximations of `x` are the prefixes of a single strictly increasing sequence
+of denominators, so each is obtained from the previous by appending the minimal admissible
+denominator. -/
+def EventuallyGreedy (x : ℝ) : Prop :=
+  x > 0 ∧ ∃ (m : ℕ → ℕ), StrictMono m ∧ (∀ k, 0 < m k) ∧
+    ∃ n₀ : ℕ, ∀ n ≥ n₀,
+      IsBestNTerm (Finset.image m (Finset.range n)) n x
+
+/--
+Let $x>0$ be a real number. For any $n\geq 1$ let
+\[R_n(x) = \sum_{i=1}^n\frac{1}{m_i}<x\]
+be the maximal sum of $n$ distinct unit fractions which is $<x$.
+
+Is it true that, for almost all $x$, for sufficiently large $n$, we have
+\[R_{n+1}(x)=R_n(x)+\frac{1}{m},\]
+where $m$ is minimal such that $m$ does not appear in $R_n(x)$ and the right-hand side is
+$<x$? (That is, are the best underapproximations eventually always constructed in a 'greedy'
+fashion?)
+
+Kovač [Ko24b] has proved that this is false - in fact as false as possible: the set of
+$x\in (0,\infty)$ for which the best underapproximations are eventually 'greedy' has Lebesgue
+measure zero.
+-/
+@[category research solved, AMS 11]
+theorem erdos_206 : answer(False) ↔
+    ∀ᵐ x ∂(volume.restrict (Set.Ioi (0 : ℝ))), EventuallyGreedy x := by
+  sorry
+
+end Erdos206
diff --git a/FormalConjectures/ErdosProblems/209.lean b/FormalConjectures/ErdosProblems/209.lean
new file mode 100644
index 0000000000..de2edc6b13
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/209.lean
@@ -0,0 +1,71 @@
+/-
+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 209
+
+*References:*
+- [erdosproblems.com/209](https://www.erdosproblems.com/209)
+- [FuPa84] Füredi, Z. and Palásti, I., *Arrangements of lines with a large number of triangles*.
+  Proc. Amer. Math. Soc. (1984), 561-566.
+- [Es16] Escudero, Juan García, *Gallai triangles in configurations of lines in the projective
+  plane*. C. R. Math. Acad. Sci. Paris (2016), 551-554.
+-/
+
+open EuclideanGeometry Affine
+
+namespace Erdos209
+
+/-- A line in the plane: the affine span of two distinct points. -/
+def IsLine (L : AffineSubspace ℝ ℝ²) : Prop :=
+  ∃ p q : ℝ², p ≠ q ∧ L = affineSpan ℝ {p, q}
+
+/-- The number of lines from `A` that pass through the point `p`. -/
+noncomputable def pointMultiplicity (A : Finset (AffineSubspace ℝ ℝ²)) (p : ℝ²) : ℕ :=
+  {L ∈ (A : Set (AffineSubspace ℝ ℝ²)) | p ∈ L}.ncard
+
+/--
+A *Gallai triangle* (or *ordinary triangle*) in a collection `A` of lines: three lines from `A`
+which intersect in three points, and each of these intersection points only intersects two
+lines from `A`.
+-/
+def HasGallaiTriangle (A : Finset (AffineSubspace ℝ ℝ²)) : Prop :=
+  ∃ L₁ ∈ A, ∃ L₂ ∈ A, ∃ L₃ ∈ A, L₁ ≠ L₂ ∧ L₂ ≠ L₃ ∧ L₁ ≠ L₃ ∧
+    ∃ p₁ p₂ p₃ : ℝ², p₁ ≠ p₂ ∧ p₂ ≠ p₃ ∧ p₁ ≠ p₃ ∧
+      p₁ ∈ L₁ ∧ p₁ ∈ L₂ ∧ p₂ ∈ L₂ ∧ p₂ ∈ L₃ ∧ p₃ ∈ L₃ ∧ p₃ ∈ L₁ ∧
+      pointMultiplicity A p₁ = 2 ∧ pointMultiplicity A p₂ = 2 ∧ pointMultiplicity A p₃ = 2
+
+/--
+Let $A$ be a finite collection of $d\geq 4$ non-parallel lines in $\mathbb{R}^2$ such that
+there are no points where at least four lines from $A$ meet. Must there exist a 'Gallai
+triangle' (or 'ordinary triangle'): three lines from $A$ which intersect in three points, and
+each of these intersection points only intersects two lines from $A$?
+
+Füredi and Palásti [FuPa84] showed this is false when $d\geq 4$ is not divisible by $9$.
+Escudero [Es16] showed this is false for all $d\geq 4$.
+-/
+@[category research solved, AMS 52]
+theorem erdos_209 : answer(False) ↔
+    ∀ d : ℕ, 4 ≤ d → ∀ A : Finset (AffineSubspace ℝ ℝ²), A.card = d →
+      (∀ L ∈ A, IsLine L) →
+      ((A : Set (AffineSubspace ℝ ℝ²)).Pairwise fun L₁ L₂ => ¬ L₁ ∥ L₂) →
+      (∀ p : ℝ², pointMultiplicity A p ≤ 3) →
+      HasGallaiTriangle A := by
+  sorry
+
+end Erdos209
diff --git a/FormalConjectures/ErdosProblems/328.lean b/FormalConjectures/ErdosProblems/328.lean
new file mode 100644
index 0000000000..a55b39cb0f
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/328.lean
@@ -0,0 +1,57 @@
+/-
+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 328
+
+*References:*
+- [erdosproblems.com/328](https://www.erdosproblems.com/328)
+- [Er80e] Erdős, P., *Some applications of Ramsey's theorem to additive number theory*.
+  European J. Combin. (1980), 43-46.
+- [NeRo85] J. Nešetřil and V. Rödl, *Two proofs in combinatorial number theory*.
+  Proc. Amer. Math. Soc. (1985), 185-188.
+-/
+
+open AdditiveCombinatorics
+
+namespace Erdos328
+
+/--
+Suppose $A\subseteq\mathbb{N}$ and $C>0$ is such that $1_A\ast 1_A(n)\leq C$ for all
+$n\in\mathbb{N}$. Can $A$ be partitioned into $t$ many subsets $A_1,\ldots,A_t$ (where
+$t=t(C)$ depends only on $C$) such that $1_{A_i}\ast 1_{A_i}(n)<C$ for all $1\leq i\leq t$
+and $n\in \mathbb{N}$?
+
+The answer is no. Asked by Erdős and Newman. Nešetřil and Rödl [NeRo85] have shown the
+answer is no for all $C$ (even if $t$ is also allowed to depend on $A$).
+
+Erdős [Er80e] had previously shown the answer is no for $C=3,4$ and infinitely many other
+values of $C$.
+
+See also [774].
+-/
+@[category research solved, AMS 11]
+theorem erdos_328 : answer(False) ↔
+    ∀ C : ℕ, 0 < C →
+      ∃ t : ℕ, ∀ A : Set ℕ, (∀ n, sumRep A n ≤ C) →
+        ∃ P : Fin t → Set ℕ, (⋃ i, P i) = A ∧
+          Set.univ.PairwiseDisjoint P ∧
+          ∀ i, ∀ n, sumRep (P i) n < C := by
+  sorry
+
+end Erdos328
diff --git a/FormalConjectures/ErdosProblems/353.lean b/FormalConjectures/ErdosProblems/353.lean
new file mode 100644
index 0000000000..7a6ea2fb20
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/353.lean
@@ -0,0 +1,139 @@
+/-
+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 353
+
+*References:*
+- [erdosproblems.com/353](https://www.erdosproblems.com/353)
+- [Ko23] Kovač, V., *Coloring and density theorems for configurations of a given volume*.
+  arXiv:2309.09973 (2023).
+- [KoPr24] Kovač, V. and B. Predojević, *Polygons of unit area with vertices in sets of infinite
+  planar measure*. arXiv:2412.11725 (2024).
+- [Ko25] J. Koizumi, *Isosceles trapezoids of unit area with vertices in sets of infinite planar
+  measure*. arXiv:2501.01914 (2025).
+-/
+
+open Affine EuclideanGeometry MeasureTheory
+
+open scoped Real
+
+namespace Erdos353
+
+/--
+`a b c d` are the vertices, in counter-clockwise order, of an isosceles trapezoid:
+they are in strictly convex position, the side `ab` is parallel to the side `cd`
+(the two bases), and the diagonals `ac` and `bd` have equal length. One pair of
+parallel sides together with equal diagonals is the classical characterization of
+an isosceles trapezoid; in particular it rules out non-rectangular parallelograms.
+-/
+def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop :=
+  IsCcwConvexPolygon ![a, b, c, d] ∧
+  line[ℝ, a, b] ∥ line[ℝ, c, d] ∧
+  dist a c = dist b d
+
+/--
+Let $A\subseteq \mathbb{R}^2$ be a measurable set with infinite measure. Must $A$ contain the
+vertices of an isosceles trapezoid of area $1$? What about an isosceles triangle, or a
+right-angled triangle, or a cyclic quadrilateral, or a convex polygon with congruent sides?
+
+Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must
+contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled
+triangle, all of area $1$.
+
+This statement formalizes the leading question, for isosceles trapezoids; the remaining
+configurations are given as variants below. The area of a polygon is taken to be the Lebesgue
+measure of the convex hull of its vertices.
+-/
+@[category research solved, AMS 28 51]
+theorem erdos_353 : answer(True) ↔
+    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
+      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A,
+        IsIsoscelesTrapezoid a b c d ∧
+        volume (convexHull ℝ {a, b, c, d}) = 1 := by
+  sorry
+
+/--
+Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of an
+isosceles triangle of area $1$.
+
+Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must
+contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled
+triangle, all of area $1$.
+
+Note the area condition forces `a`, `b`, `c` to be affinely independent, so no separate
+non-degeneracy hypothesis is needed.
+-/
+@[category research solved, AMS 28 51]
+theorem erdos_353.variants.isosceles_triangle :
+    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
+      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
+        (dist a b = dist a c ∨ dist b a = dist b c ∨ dist c a = dist c b) ∧
+        volume (convexHull ℝ {a, b, c}) = 1 := by
+  sorry
+
+/--
+Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of a
+right-angled triangle of area $1$.
+
+Koizumi [Ko25] has resolved this question, proving that any set with infinite measure must
+contain the vertices of an isosceles trapezoid, an isosceles triangle, and a right-angled
+triangle, all of area $1$.
+
+Note the area condition forces `a`, `b`, `c` to be affinely independent, so no separate
+non-degeneracy hypothesis is needed.
+-/
+@[category research solved, AMS 28 51]
+theorem erdos_353.variants.right_angled_triangle :
+    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
+      ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
+        (∠ b a c = π / 2 ∨ ∠ a b c = π / 2 ∨ ∠ b c a = π / 2) ∧
+        volume (convexHull ℝ {a, b, c}) = 1 := by
+  sorry
+
+/--
+Every measurable $A\subseteq \mathbb{R}^2$ with infinite measure contains the vertices of a
+cyclic quadrilateral of area $1$.
+
+Kovač and Predojević [KoPr24] have proved that this is true for cyclic quadrilaterals - that
+is, every set with infinite measure contains four distinct points on a circle such that the
+quadrilateral determined by these four points has area $1$. The quadrilateral determined by
+four distinct concyclic points is their convex hull.
+-/
+@[category research solved, AMS 28 51]
+theorem erdos_353.variants.cyclic_quadrilateral :
+    ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
+      ∃ Q : Set ℝ², Q ⊆ A ∧ Q.ncard = 4 ∧ Cospherical Q ∧
+        volume (convexHull ℝ Q) = 1 := by
+  sorry
+
+/--
+The answer is negative for convex polygons with congruent sides: Kovač and Predojević
+[KoPr24] prove that there exists a set of infinite measure such that every convex polygon
+with congruent sides and all vertices in the set has area $<1$.
+-/
+@[category research solved, AMS 28 51]
+theorem erdos_353.variants.congruent_sides :
+    ∃ A : Set ℝ², MeasurableSet A ∧ volume A = ⊤ ∧
+      ∀ (n : ℕ) (v : Fin (n + 3) → ℝ²),
+        IsCcwConvexPolygon v → (∀ i, v i ∈ A) →
+        (∀ i, dist (v i) (v (i + 1)) = dist (v 0) (v 1)) →
+        volume (convexHull ℝ (Set.range v)) < 1 := by
+  sorry
+
+end Erdos353
diff --git a/FormalConjectures/ErdosProblems/403.lean b/FormalConjectures/ErdosProblems/403.lean
new file mode 100644
index 0000000000..fa0b017a9e
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/403.lean
@@ -0,0 +1,54 @@
+/-
+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 403
+
+*References:*
+- [erdosproblems.com/403](https://www.erdosproblems.com/403)
+- [Li76] Lin, S., *On two problems of Erdős concerning sums of distinct factorials*.
+  Bell Laboratories internal memorandum (1960).
+-/
+
+namespace Erdos403
+
+/--
+Does the equation
+\[2^m=a_1!+\cdots+a_k!\]
+with $a_1<a_2<\cdots <a_k$ have only finitely many solutions?
+
+Asked by Burr and Erdős. Frankl and Lin [Li76] independently showed that the answer is yes, and
+the largest solution is
+\[2^7=2!+3!+5!.\]
+In fact Lin showed that the largest power of $2$ which can divide a sum of distinct factorials
+containing $2$ is $2^{254}$, and that there are only 5 solutions to $3^m=a_1!+\cdots+a_k!$
+(when $m=0,1,2,3,6$).
+
+See also [404].
+
+A solution is encoded below as a pair $(m, s)$ where $s$ is the finite set
+$\{a_1 < a_2 < \cdots < a_k\}$ of positive integers, so the distinctness of the $a_i$ is
+given by set membership. The empty set contributes no solutions since $2^m \geq 1 > 0$.
+-/
+@[category research solved, AMS 11]
+theorem erdos_403 : answer(True) ↔
+    {p : ℕ × Finset ℕ | (∀ a ∈ p.2, 0 < a) ∧
+      2 ^ p.1 = ∑ a ∈ p.2, a.factorial}.Finite := by
+  sorry
+
+end Erdos403
diff --git a/FormalConjectures/ErdosProblems/426.lean b/FormalConjectures/ErdosProblems/426.lean
new file mode 100644
index 0000000000..692f25f136
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/426.lean
@@ -0,0 +1,75 @@
+/-
+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 426
+
+*References:*
+- [erdosproblems.com/426](https://www.erdosproblems.com/426)
+- [EnEr72] Entringer, R. C. and Erdős, Paul, *On the number of unique subgraphs of a graph*.
+  J. Combinatorial Theory Ser. B (1972), 112-115.
+- [HaSc73] Harary, Frank and Schwenk, Allen J., *On the number of unique subgraphs*.
+  J. Combinatorial Theory Ser. B (1973), 156-160.
+- [Br75] Brouwer, A. E., *Note: "On the number of unique subgraphs of a graph"
+  (J. Combinatorial Theory Ser. B 13 (1972), 112-115) by R. C. Entringer and P. Erdős*.
+  J. Combinatorial Theory Ser. B (1975), 184-185.
+- [BrCh24] Bradač, D. and Christoph, M., *Unique subgraphs are rare*. arXiv:2410.16233 (2024).
+-/
+
+open Filter
+
+namespace Erdos426
+
+/--
+`G` is a **unique subgraph** of `H` if there is exactly one subgraph of `H` isomorphic to `G`.
+Subgraphs of `H` are taken in the spanning sense: elements `G' ≤ H` of the lattice
+`SimpleGraph (Fin n)`, i.e. subsets of the edges of `H` (not necessarily induced).
+-/
+def IsUniqueSubgraph {n : ℕ} (G H : SimpleGraph (Fin n)) : Prop :=
+  ∃! G' : SimpleGraph (Fin n), G' ≤ H ∧ Nonempty (G.Iso G')
+
+/--
+The number of distinct unique subgraphs of `H`: the number of isomorphism classes of graphs
+that occur exactly once as a subgraph of `H`. Each such class contains exactly one subgraph
+`G ≤ H` (uniqueness forbids a second isomorphic copy), so counting those representatives
+counts the classes.
+-/
+noncomputable def uniqueSubgraphCount {n : ℕ} (H : SimpleGraph (Fin n)) : ℕ :=
+  {G : SimpleGraph (Fin n) | G ≤ H ∧ IsUniqueSubgraph G H}.ncard
+
+/--
+We say $H$ is a unique subgraph of $G$ if there is exactly one way to find $H$ as a subgraph
+(not necessarily induced) of $G$. Is there a graph on $n$ vertices with
+\[\gg \frac{2^{\binom{n}{2}}}{n!}\]
+many distinct unique subgraphs?
+
+Bradač and Christoph [BrCh24] have proved the answer is no: if $f(n)$ is the maximum number of
+unique subgraphs in a graph on $n$ vertices then
+\[f(n) = o\left(\frac{2^{\binom{n}{2}}}{n!}\right).\]
+
+The $\gg$ below is read as: some constant $c>0$ works for arbitrarily large $n$. The negation
+of the proposition on the right is then exactly $f(n) = o(2^{\binom{n}{2}}/n!)$, the form in
+which Bradač and Christoph [BrCh24] resolved the problem.
+-/
+@[category research solved, AMS 5]
+theorem erdos_426 : answer(False) ↔
+    ∃ c : ℝ, 0 < c ∧ ∃ᶠ (n : ℕ) in atTop, ∃ H : SimpleGraph (Fin n),
+      c * ((2 : ℝ) ^ n.choose 2 / n.factorial) ≤ (uniqueSubgraphCount H : ℝ) := by
+  sorry
+
+end Erdos426
diff --git a/FormalConjectures/ErdosProblems/464.lean b/FormalConjectures/ErdosProblems/464.lean
new file mode 100644
index 0000000000..c3d0c32785
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/464.lean
@@ -0,0 +1,82 @@
+/-
+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 464
+
+*References:*
+- [erdosproblems.com/464](https://www.erdosproblems.com/464)
+- [AkMo04] Akhunzhanov, R. K. and Moshchevitin, N. G., *On the chromatic number of a distance
+  graph associated with a lacunary sequence*. Dokl. Akad. Nauk (2004), 295-296.
+- [Du06] Dubickas, Artūras, *On the fractional parts of lacunary sequences*. Math. Scand. (2006),
+  136-146.
+- [Ka01] Katznelson, Y., *Chromatic numbers of Cayley graphs on $\mathbb{Z}$ and recurrence*.
+  Combinatorica (2001), 211-219.
+- [PeSc10] Peres, Yuval and Schlag, Wilhelm, *Two Erdős problems on lacunary sequences: chromatic
+  number and Diophantine approximation*. Bull. Lond. Math. Soc. (2010), 295-300.
+- [Po79b] Pollington, A. D., *On the density of sequence $\{n_k\xi\}$*. Illinois J. Math. (1979),
+  511-515.
+- [dM80] de Mathan, B., *Numbers contravening a condition in density modulo $1$*. Acta Math.
+  Acad. Sci. Hungar. (1980), 237-241 (1981).
+-/
+
+namespace Erdos464
+
+/- Formalization notes:
+- Since every $\|\theta n_k\|$ lies in $[0,1/2]$, the literal reading of "$\{\|\theta n_k\|\}$
+  is not dense in $[0,1]$" would be vacuously true. The intended (and solved) content is that
+  the sequence $(\theta n_k)$ is not dense modulo one, which is how the conclusion is rendered
+  here: `¬ Dense (Set.range fun k => (↑(θ * n k) : AddCircle (1 : ℝ)))`. This matches
+  `pollington_de_mathan` in `Problem10_6.lean` of the Bugeaud collection, which formalizes the
+  full-Hausdorff-dimension version of the same de Mathan–Pollington theorem. It is implied by
+  the $\inf_{k\geq 1}\|\theta n_k\| > 0$ that de Mathan and Pollington prove.
+- The lacunarity hypothesis is rendered by the house predicate `IsLacunary`
+  ($\exists c > 1$ with $c \cdot n_k < n_{k+1}$ for all sufficiently large $k$), as in
+  `erdos_355`; for a strictly increasing sequence of positive integers the problem's condition
+  $n_{k+1} \geq (1+\epsilon) n_k$ for all $k$ implies `IsLacunary`, and modifying finitely many
+  terms does not affect density modulo one.
+-/
+
+/--
+Let $A=\{n_1<n_2<\cdots\}\subset \mathbb{N}$ be a lacunary sequence (so there exists some
+$\epsilon>0$ with $n_{k+1}\geq (1+\epsilon)n_k$ for all $k$). Must there exist an irrational
+$\theta$ such that
+$$\{ \|\theta n_k\| : k\geq 1\}$$
+is not dense in $[0,1]$ (where $\| x\|$ is the distance to the nearest integer)?
+
+Solved independently by de Mathan [dM80] and Pollington [Po79b], who showed that, given any
+such $A$, there exists such a $\theta$, with
+$$\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon^4}{\log(1/\epsilon)}.$$
+This bound was improved by Katznelson [Ka01], Akhunzhanov and Moshchevitin [AkMo04], and
+Dubickas [Du06], before Peres and Schlag [PeSc10] improved it to
+$$\inf_{k\geq 1}\| \theta n_k\| \gg \frac{\epsilon}{\log(1/\epsilon)},$$
+and note that the best bound possible here would be $\gg \epsilon$.
+
+This problem has consequences for [894](https://www.erdosproblems.com/894).
+
+The conclusion "$\{\|\theta n_k\|\}$ is not dense in $[0,1]$" is formalized as the sequence
+$(\theta n_k)$ not being dense modulo one; see the formalization notes above.
+-/
+@[category research solved, AMS 11]
+theorem erdos_464 : answer(True) ↔
+    ∀ n : ℕ → ℕ, StrictMono n → (∀ k, 0 < n k) → IsLacunary n →
+      ∃ θ : ℝ, Irrational θ ∧
+        ¬ Dense (Set.range fun k => (↑(θ * n k) : AddCircle (1 : ℝ))) := by
+  sorry
+
+end Erdos464
diff --git a/FormalConjectures/ErdosProblems/512.lean b/FormalConjectures/ErdosProblems/512.lean
new file mode 100644
index 0000000000..16926e9217
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/512.lean
@@ -0,0 +1,49 @@
+/-
+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 512
+
+*References:*
+- [erdosproblems.com/512](https://www.erdosproblems.com/512)
+- [Ko81] Konyagin, S. V., *On the Littlewood problem*. Izv. Akad. Nauk SSSR Ser. Mat. (1981),
+  243-265, 463.
+- [MPS81] McGehee, O. Carruth and Pigno, Louis and Smith, Brent, *Hardy's inequality and the
+  $L^1$ norm of exponential sums*. Ann. of Math. (2) (1981), 613-618.
+-/
+
+namespace Erdos512
+
+/-- Shorthand for the additive character $e(x) = e^{2\pi i x}$. -/
+noncomputable def e (x : ℝ) : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)
+
+/--
+Is it true that, if $A\subset \mathbb{Z}$ is a finite set of size $N$, then
+\[\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N,\]
+where $e(x)=e^{2\pi ix }$?
+
+Littlewood's conjecture, proved independently by Konyagin [Ko81] and McGehee, Pigno, and
+Smith [MPS81].
+-/
+@[category research solved, AMS 11 42]
+theorem erdos_512 : answer(True) ↔
+    ∃ c > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℤ), A.card = N →
+      c * Real.log N ≤ ∫ θ in (0 : ℝ)..1, ‖∑ n ∈ A, e (n * θ)‖ := by
+  sorry
+
+end Erdos512
diff --git a/FormalConjectures/ErdosProblems/621.lean b/FormalConjectures/ErdosProblems/621.lean
new file mode 100644
index 0000000000..2720bb2386
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/621.lean
@@ -0,0 +1,65 @@
+/-
+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 621
+
+*References:*
+- [erdosproblems.com/621](https://www.erdosproblems.com/621)
+- [EGT96] Erdős, Paul and Gallai, Tibor and Tuza, Zsolt, *Covering and independence in triangle
+  structures*. Discrete Math. (1996), 89-101.
+- [NoSu16] S. Norin and Y.-R. Sun, *Triangle-free independent sets vs. cuts*. arXiv:1602.04370
+  (2016).
+-/
+
+open SimpleGraph Classical
+
+namespace Erdos621
+
+/--
+Let $G$ be a graph on $n$ vertices, $\alpha_1(G)$ be the maximum number of edges that contain
+at most one edge from every triangle, and $\tau_1(G)$ be the minimum number of edges that
+contain at least one edge from every triangle.
+
+Is it true that\[\alpha_1(G)+\tau_1(G) \leq \frac{n^2}{4}?\]
+
+A problem of Erdős, Gallai, and Tuza [EGT96], who observe that this is probably quite difficult
+since there are different examples where equality hold: the complete graph, the complete
+bipartite graph, and the graph obtained from $K_{m,m}$ by adding one vertex joined to every
+other.
+
+This is true, and was proved by Norin and Sun [NoSu16], who in fact proved
+that\[\alpha_1(G)+\tau_B(G) \leq \frac{n^2}{4},\]where $\tau_B(G)$ is the minimum number of
+edges that need to be removed to make the graph bipartite.
+
+Here $\alpha_1(G)$ and $\tau_1(G)$ are taken over subsets of the edge set of $G$, and the
+inequality is stated multiplied through by $4$ so that it lives in the natural numbers.
+-/
+@[category research solved, AMS 5]
+theorem erdos_621 : answer(True) ↔
+    ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ),
+      IsGreatest {k : ℕ | ∃ A ⊆ G.edgeFinset, A.card = k ∧
+        ∀ x y z : Fin n, G.Adj x y → G.Adj y z → G.Adj x z →
+          (({s(x, y), s(y, z), s(x, z)} : Finset (Sym2 (Fin n))) ∩ A).card ≤ 1} a →
+      IsLeast {k : ℕ | ∃ T ⊆ G.edgeFinset, T.card = k ∧
+        ∀ x y z : Fin n, G.Adj x y → G.Adj y z → G.Adj x z →
+          (T ∩ ({s(x, y), s(y, z), s(x, z)} : Finset (Sym2 (Fin n)))).Nonempty} t →
+      4 * (a + t) ≤ n ^ 2 := by
+  sorry
+
+end Erdos621
diff --git a/FormalConjectures/ErdosProblems/639.lean b/FormalConjectures/ErdosProblems/639.lean
new file mode 100644
index 0000000000..6d7d263ac1
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/639.lean
@@ -0,0 +1,60 @@
+/-
+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 639
+
+*References:*
+- [erdosproblems.com/639](https://www.erdosproblems.com/639)
+- [KeSu04] Keevash, Peter and Sudakov, Benny, *On the number of edges not covered by monochromatic
+  copies of a fixed graph*. J. Combin. Theory Ser. B (2004), 41-53.
+- [Py86] Pyber, L., *Clique covering of graphs*. Combinatorica (1986), 393-398.
+-/
+
+open Filter
+
+namespace Erdos639
+
+/--
+Is it true that if the edges of $K_n$ are 2-coloured then there are at most $n^2/4$ many edges
+which do not occur in a monochromatic triangle?
+
+Solved by Erdős, Rousseau, and Schelp for large $n$, but unpublished. Alon has observed that this
+also follows from a result of Pyber [Py86], which states that (for large enough $n$) at most
+$\lfloor n^2/4\rfloor+2$ monochromatic cliques cover all edges of a $2$-coloured $K_n$.
+
+This problem was solved completely by Keevash and Sudakov [KeSu04], who proved that the correct
+threshold is $\lfloor n^2/4\rfloor$ for all $n\geq 7$, is $\binom{n}{2}$ for $n\leq 5$, and is
+$10$ for $n=6$.
+
+Since the bound fails for small $n$ (at $n=6$ the threshold is $10 > 6^2/4$), the statement is
+formalized in the asymptotic reading in which the problem was posed and solved: for all
+sufficiently large $n$, every $2$-colouring of the edges of $K_n$ leaves at most $n^2/4$ edges
+not occurring in a monochromatic triangle. Edges of $K_n$ are the non-diagonal unordered pairs
+`Sym2 (Fin n)`; an edge $\{x, y\}$ occurs in a monochromatic triangle if and only if there is a
+third vertex $z$ with $C(\{x, z\}) = C(\{y, z\}) = C(\{x, y\})$.
+-/
+@[category research solved, AMS 5]
+theorem erdos_639 : answer(True) ↔
+    ∀ᶠ (n : ℕ) in atTop, ∀ C : Sym2 (Fin n) → Fin 2,
+      {e : Sym2 (Fin n) | ¬e.IsDiag ∧
+        ∀ x y : Fin n, e = s(x, y) →
+          ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4 := by
+  sorry
+
+end Erdos639
diff --git a/FormalConjectures/ErdosProblems/648.lean b/FormalConjectures/ErdosProblems/648.lean
new file mode 100644
index 0000000000..bfcf5f22e5
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/648.lean
@@ -0,0 +1,68 @@
+/-
+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 648
+
+*References:*
+- [erdosproblems.com/648](https://www.erdosproblems.com/648)
+- [Ca25b] S. Cambie, *On Erdős problem #648*. arXiv:2503.22691 (2025).
+-/
+
+open Filter Asymptotics
+
+namespace Erdos648
+
+/-
+Divergences from the hosted theorems (details in statements/648/draft.json):
+- the sequence range follows the problem text, `2 ≤ a_1 < ⋯ < a_t < n` (`Set.Ico 2 n`);
+  both hosted theorems allow `0 < m ≤ n` (`Set.Ioc 0 n`), which admits `1` and `n`.
+- `P` is the FC-house `Nat.maxPrimeFac`; the hosted files define
+  `P n = (n.primeFactors.max).getD 1`. The two agree on `2 ≤ m`.
+- the sequence is a strictly monotone `a : Fin t → ℕ` (FC house shape); the hosted
+  theorems use a `List ℕ` with `IsChain`.
+-/
+
+/--
+`g n` is the largest `t` such that there exist integers `2 ≤ a 0 < a 1 < ⋯ < a (t - 1) < n`
+whose greatest prime factors are strictly decreasing. -/
+noncomputable def g (n : ℕ) : ℕ :=
+  sSup {t | ∃ a : Fin t → ℕ, StrictMono a ∧ (∀ i, a i ∈ Set.Ico 2 n) ∧
+    StrictAnti fun i => (a i).maxPrimeFac}
+
+/--
+Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1<a_2<\cdots <a_t <n$
+such that \[P(a_1)>P(a_2)>\cdots >P(a_t)\] where $P(m)$ is the greatest prime factor of $m$.
+Estimate $g(n)$.
+
+Stijn Cambie has proved [Ca25b] \[g(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}.\]
+Cambie further asks whether there exists a constant $c$ such that
+\[g(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}.\]
+Cambie's proof shows that such a $c$ must satisfy $2\leq c\leq 2\sqrt{2}$.
+
+The sequence $a_1<a_2<\cdots<a_t$ is packaged as a strictly monotone map `a : Fin t → ℕ`
+with $2\leq a_i<n$, the greatest prime factor $P$ is `Nat.maxPrimeFac`, and $g(n)$ is the
+supremum in `ℕ` of the achievable lengths $t$.
+-/
+@[category research solved, AMS 11,
+  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos648.lean"]
+theorem erdos_648 :
+    (fun n => (g n : ℝ)) =Θ[atTop] fun n => Real.sqrt ((n : ℝ) / Real.log (n : ℝ)) := by
+  sorry
+
+end Erdos648
diff --git a/FormalConjectures/ErdosProblems/71.lean b/FormalConjectures/ErdosProblems/71.lean
new file mode 100644
index 0000000000..0d332bd061
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/71.lean
@@ -0,0 +1,53 @@
+/-
+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 71
+
+*References:*
+- [erdosproblems.com/71](https://www.erdosproblems.com/71)
+- [Bo77] Bollobás, Béla, *Cycles modulo $k$*. Bull. London Math. Soc. (1977), 97-98.
+- [Er82e] Erdős, Paul, *Some of my favourite problems which recently have been solved*.
+  (1982), 59--79.
+-/
+
+namespace Erdos71
+
+/--
+Is it true that for every infinite arithmetic progression $P$ which contains even numbers
+there is some constant $c=c(P)$ such that every graph with average degree at least $c$
+contains a cycle whose length is in $P$?
+
+In [Er82e] Erdős credits this conjecture to himself and Burr. This has been proved by
+Bollobás [Bo77]. The best dependence of the constant $c(P)$ is unknown.
+
+The infinite arithmetic progression is encoded as a set $P \subseteq \mathbb{N}$ satisfying
+`P.IsAPOfLength ⊤` (which forces a positive common difference), and "contains even numbers"
+as the existence of an even element. The average degree of a finite simple graph is
+`SimpleGraph.averageDegree`, i.e. $(\sum_v \deg v)/|V| \in \mathbb{Q}$, and a cycle whose
+length is in $P$ is a cycle walk `w` with `w.length ∈ P`.
+-/
+@[category research solved, AMS 5]
+theorem erdos_71 : answer(True) ↔
+    ∀ P : Set ℕ, P.IsAPOfLength ⊤ → (∃ n ∈ P, Even n) →
+      ∃ c : ℚ, ∀ (V : Type) [Fintype V] [DecidableEq V] (G : SimpleGraph V)
+        [DecidableRel G.Adj], c ≤ G.averageDegree →
+          ∃ (v : V) (w : G.Walk v v), w.IsCycle ∧ w.length ∈ P := by
+  sorry
+
+end Erdos71

From daf095b25409537cc756504c5cd0ac2345d5d4f3 Mon Sep 17 00:00:00 2001
From: Will Blair <85643015+willblair0708@users.noreply.github.com>
Date: Sat, 4 Jul 2026 17:38:25 -0400
Subject: [PATCH 2/4] =?UTF-8?q?Tighten=20Erd=C5=91s=20batch=20references?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 FormalConjectures/ErdosProblems/206.lean | 9 +++++++++
 FormalConjectures/ErdosProblems/209.lean | 3 +++
 FormalConjectures/ErdosProblems/328.lean | 4 ++++
 FormalConjectures/ErdosProblems/353.lean | 2 ++
 FormalConjectures/ErdosProblems/403.lean | 2 ++
 FormalConjectures/ErdosProblems/426.lean | 2 ++
 FormalConjectures/ErdosProblems/464.lean | 5 +++++
 FormalConjectures/ErdosProblems/512.lean | 2 ++
 FormalConjectures/ErdosProblems/621.lean | 2 ++
 FormalConjectures/ErdosProblems/639.lean | 2 ++
 FormalConjectures/ErdosProblems/648.lean | 4 ++--
 FormalConjectures/ErdosProblems/71.lean  | 4 ++++
 12 files changed, 39 insertions(+), 2 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/206.lean b/FormalConjectures/ErdosProblems/206.lean
index 8f991e9ecb..6041897aaf 100644
--- a/FormalConjectures/ErdosProblems/206.lean
+++ b/FormalConjectures/ErdosProblems/206.lean
@@ -21,6 +21,15 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/206](https://www.erdosproblems.com/206)
+- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial
+  number theory*. Monographies de L'Enseignement Mathématique (1980).
+- [Cu22] Curtiss, D. R., *On Kellogg's Diophantine Problem*. Amer. Math. Monthly (1922),
+  380-387.
+- [Er50b] Erdős, Pál, *On a Diophantine equation*. Mat. Lapok (1950), 192-210.
+- [Na23] Nathanson, M., *Underapproximation by Egyptian fractions*. J. Number Theory (2023),
+  208-234.
+- [Ch23b] Chu, H. V., *A threshold for the best two-term underapproximation by Egyptian
+  fractions*. arXiv:2306.12564 (2023).
 - [Ko24b] Kovač, V., *On eventually greedy best underapproximations by Egyptian fractions*.
   arXiv:2406.07218 (2024).
 -/
diff --git a/FormalConjectures/ErdosProblems/209.lean b/FormalConjectures/ErdosProblems/209.lean
index de2edc6b13..9fe7205fb2 100644
--- a/FormalConjectures/ErdosProblems/209.lean
+++ b/FormalConjectures/ErdosProblems/209.lean
@@ -21,6 +21,9 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/209](https://www.erdosproblems.com/209)
+- [Er84] Erdős, P., *Research problems*. Period. Math. Hungar. (1984), 101-103.
+- [ErPu95b] Erdős, Paul and Purdy, George, *Extremal problems in combinatorial geometry*.
+  Handbook of combinatorics, Vol. 1, 2 (1995), 809-874.
 - [FuPa84] Füredi, Z. and Palásti, I., *Arrangements of lines with a large number of triangles*.
   Proc. Amer. Math. Soc. (1984), 561-566.
 - [Es16] Escudero, Juan García, *Gallai triangles in configurations of lines in the projective
diff --git a/FormalConjectures/ErdosProblems/328.lean b/FormalConjectures/ErdosProblems/328.lean
index a55b39cb0f..87c3a234d6 100644
--- a/FormalConjectures/ErdosProblems/328.lean
+++ b/FormalConjectures/ErdosProblems/328.lean
@@ -21,6 +21,10 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/328](https://www.erdosproblems.com/328)
+- [Er80] Erdős, Paul, *A survey of problems in combinatorial number theory*.
+  Ann. Discrete Math. (1980), 89-115.
+- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial
+  number theory*. Monographies de L'Enseignement Mathématique (1980).
 - [Er80e] Erdős, P., *Some applications of Ramsey's theorem to additive number theory*.
   European J. Combin. (1980), 43-46.
 - [NeRo85] J. Nešetřil and V. Rödl, *Two proofs in combinatorial number theory*.
diff --git a/FormalConjectures/ErdosProblems/353.lean b/FormalConjectures/ErdosProblems/353.lean
index 7a6ea2fb20..239b250490 100644
--- a/FormalConjectures/ErdosProblems/353.lean
+++ b/FormalConjectures/ErdosProblems/353.lean
@@ -21,6 +21,8 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/353](https://www.erdosproblems.com/353)
+- [Er83d] Erdős, Paul, *Some combinatorial, geometric and set theoretic problems in measure
+  theory*. Measure Theory, Oberwolfach 1983 (1984), 321-327.
 - [Ko23] Kovač, V., *Coloring and density theorems for configurations of a given volume*.
   arXiv:2309.09973 (2023).
 - [KoPr24] Kovač, V. and B. Predojević, *Polygons of unit area with vertices in sets of infinite
diff --git a/FormalConjectures/ErdosProblems/403.lean b/FormalConjectures/ErdosProblems/403.lean
index fa0b017a9e..e6a5d076ea 100644
--- a/FormalConjectures/ErdosProblems/403.lean
+++ b/FormalConjectures/ErdosProblems/403.lean
@@ -21,6 +21,8 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/403](https://www.erdosproblems.com/403)
+- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial
+  number theory*. Monographies de L'Enseignement Mathématique (1980).
 - [Li76] Lin, S., *On two problems of Erdős concerning sums of distinct factorials*.
   Bell Laboratories internal memorandum (1960).
 -/
diff --git a/FormalConjectures/ErdosProblems/426.lean b/FormalConjectures/ErdosProblems/426.lean
index 692f25f136..a457465a14 100644
--- a/FormalConjectures/ErdosProblems/426.lean
+++ b/FormalConjectures/ErdosProblems/426.lean
@@ -21,6 +21,8 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/426](https://www.erdosproblems.com/426)
+- [Er76b] Erdős, P., *Problems and results in graph theory and combinatorial analysis*.
+  Proceedings of the Fifth British Combinatorial Conference (1976), 169-192.
 - [EnEr72] Entringer, R. C. and Erdős, Paul, *On the number of unique subgraphs of a graph*.
   J. Combinatorial Theory Ser. B (1972), 112-115.
 - [HaSc73] Harary, Frank and Schwenk, Allen J., *On the number of unique subgraphs*.
diff --git a/FormalConjectures/ErdosProblems/464.lean b/FormalConjectures/ErdosProblems/464.lean
index c3d0c32785..b526ab096b 100644
--- a/FormalConjectures/ErdosProblems/464.lean
+++ b/FormalConjectures/ErdosProblems/464.lean
@@ -21,6 +21,11 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/464](https://www.erdosproblems.com/464)
+- [Er75i] Erdős, P., *Répartition modulo $1$*. (1975), iv+258.
+- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial
+  number theory*. Monographies de L'Enseignement Mathématique (1980).
+- [Er82e] Erdős, Paul, *Some of my favourite problems which recently have been solved*.
+  (1982), 59--79.
 - [AkMo04] Akhunzhanov, R. K. and Moshchevitin, N. G., *On the chromatic number of a distance
   graph associated with a lacunary sequence*. Dokl. Akad. Nauk (2004), 295-296.
 - [Du06] Dubickas, Artūras, *On the fractional parts of lacunary sequences*. Math. Scand. (2006),
diff --git a/FormalConjectures/ErdosProblems/512.lean b/FormalConjectures/ErdosProblems/512.lean
index 16926e9217..241db37b0d 100644
--- a/FormalConjectures/ErdosProblems/512.lean
+++ b/FormalConjectures/ErdosProblems/512.lean
@@ -21,6 +21,8 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/512](https://www.erdosproblems.com/512)
+- [Er61] Erdős, Paul, *Some unsolved problems*. Magyar Tud. Akad. Mat. Kutató Int. Közl.
+  (1961), 221-254.
 - [Ko81] Konyagin, S. V., *On the Littlewood problem*. Izv. Akad. Nauk SSSR Ser. Mat. (1981),
   243-265, 463.
 - [MPS81] McGehee, O. Carruth and Pigno, Louis and Smith, Brent, *Hardy's inequality and the
diff --git a/FormalConjectures/ErdosProblems/621.lean b/FormalConjectures/ErdosProblems/621.lean
index 2720bb2386..1891c801e7 100644
--- a/FormalConjectures/ErdosProblems/621.lean
+++ b/FormalConjectures/ErdosProblems/621.lean
@@ -23,6 +23,8 @@ import FormalConjectures.Util.ProblemImports
 - [erdosproblems.com/621](https://www.erdosproblems.com/621)
 - [EGT96] Erdős, Paul and Gallai, Tibor and Tuza, Zsolt, *Covering and independence in triangle
   structures*. Discrete Math. (1996), 89-101.
+- [Er99] Erdős, Paul, *A selection of problems and results in combinatorics*.
+  Combin. Probab. Comput. (1999), 1-6.
 - [NoSu16] S. Norin and Y.-R. Sun, *Triangle-free independent sets vs. cuts*. arXiv:1602.04370
   (2016).
 -/
diff --git a/FormalConjectures/ErdosProblems/639.lean b/FormalConjectures/ErdosProblems/639.lean
index 6d7d263ac1..f8a38c62f3 100644
--- a/FormalConjectures/ErdosProblems/639.lean
+++ b/FormalConjectures/ErdosProblems/639.lean
@@ -21,6 +21,8 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/639](https://www.erdosproblems.com/639)
+- [Er97d] Erdős, Paul, *Some recent problems and results in graph theory*. Discrete Math.
+  (1997), 81-85.
 - [KeSu04] Keevash, Peter and Sudakov, Benny, *On the number of edges not covered by monochromatic
   copies of a fixed graph*. J. Combin. Theory Ser. B (2004), 41-53.
 - [Py86] Pyber, L., *Clique covering of graphs*. Combinatorica (1986), 393-398.
diff --git a/FormalConjectures/ErdosProblems/648.lean b/FormalConjectures/ErdosProblems/648.lean
index bfcf5f22e5..44c4c79807 100644
--- a/FormalConjectures/ErdosProblems/648.lean
+++ b/FormalConjectures/ErdosProblems/648.lean
@@ -21,6 +21,7 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/648](https://www.erdosproblems.com/648)
+- [Er95c] Erdős, Paul, *Some problems in number theory*. Octogon Math. Mag. (1995), 3-5.
 - [Ca25b] S. Cambie, *On Erdős problem #648*. arXiv:2503.22691 (2025).
 -/
 
@@ -59,8 +60,7 @@ The sequence $a_1<a_2<\cdots<a_t$ is packaged as a strictly monotone map `a : Fi
 with $2\leq a_i<n$, the greatest prime factor $P$ is `Nat.maxPrimeFac`, and $g(n)$ is the
 supremum in `ℕ` of the achievable lengths $t$.
 -/
-@[category research solved, AMS 11,
-  formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos648.lean"]
+@[category research solved, AMS 11]
 theorem erdos_648 :
     (fun n => (g n : ℝ)) =Θ[atTop] fun n => Real.sqrt ((n : ℝ) / Real.log (n : ℝ)) := by
   sorry
diff --git a/FormalConjectures/ErdosProblems/71.lean b/FormalConjectures/ErdosProblems/71.lean
index 0d332bd061..8bf00d0334 100644
--- a/FormalConjectures/ErdosProblems/71.lean
+++ b/FormalConjectures/ErdosProblems/71.lean
@@ -24,6 +24,10 @@ import FormalConjectures.Util.ProblemImports
 - [Bo77] Bollobás, Béla, *Cycles modulo $k$*. Bull. London Math. Soc. (1977), 97-98.
 - [Er82e] Erdős, Paul, *Some of my favourite problems which recently have been solved*.
   (1982), 59--79.
+- [Er95] Erdős, Paul, *Some of my favourite problems in number theory, combinatorics, and
+  geometry*. Resenhas (1995), 165-186.
+- [Er97b] Erdős, Paul, *Some old and new problems in various branches of combinatorics*.
+  Discrete Math. (1997), 227-231.
 -/
 
 namespace Erdos71

From f6600f38a3c0dd3401e66d9ec53171bdc5ae898f Mon Sep 17 00:00:00 2001
From: Will Blair <85643015+williamjblair@users.noreply.github.com>
Date: Sun, 5 Jul 2026 12:47:57 -0400
Subject: [PATCH 3/4] Address review: reuse/move geometry defs, tidy 206,
 idiomatic IsLine

- 353: move IsIsoscelesTrapezoid into FormalConjecturesForMathlib/Geometry/2d.lean;
  reuse the existing IsIsosceles; add IsRightAngled there and use it
- 206: use big-operator notation for egyptianSum; inline the single-use ValidEgyptian
- 209: define IsLine via finrank of the direction (mo271's suggestion)
---
 FormalConjectures/ErdosProblems/206.lean     | 10 +++-------
 FormalConjectures/ErdosProblems/209.lean     |  4 ++--
 FormalConjectures/ErdosProblems/353.lean     | 16 ++--------------
 FormalConjecturesForMathlib/Geometry/2d.lean | 17 +++++++++++++++++
 4 files changed, 24 insertions(+), 23 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/206.lean b/FormalConjectures/ErdosProblems/206.lean
index 6041897aaf..253f4123bd 100644
--- a/FormalConjectures/ErdosProblems/206.lean
+++ b/FormalConjectures/ErdosProblems/206.lean
@@ -54,15 +54,11 @@ namespace Erdos206
 
 /-- The Egyptian fraction sum: `∑_{m ∈ S} 1/m` for a finset of natural numbers. -/
 noncomputable def egyptianSum (S : Finset ℕ) : ℝ :=
-  S.sum (fun m => (1 : ℝ) / m)
+  ∑ m ∈ S, (1 : ℝ) / m
 
-/-- All elements of the finset are positive (valid denominators). -/
-def ValidEgyptian (S : Finset ℕ) : Prop :=
-  ∀ m ∈ S, 0 < m
-
-/-- `S` is an Egyptian underapproximation of `x`: valid denominators and sum < x. -/
+/-- `S` is an Egyptian underapproximation of `x`: valid denominators (all positive) and sum < x. -/
 def IsUnderapprox (S : Finset ℕ) (x : ℝ) : Prop :=
-  ValidEgyptian S ∧ egyptianSum S < x
+  (∀ m ∈ S, 0 < m) ∧ egyptianSum S < x
 
 /-- `S` achieves the best `n`-term Egyptian underapproximation of `x`,
 i.e. `egyptianSum S` realises $R_n(x)$. -/
diff --git a/FormalConjectures/ErdosProblems/209.lean b/FormalConjectures/ErdosProblems/209.lean
index 9fe7205fb2..713bc0b207 100644
--- a/FormalConjectures/ErdosProblems/209.lean
+++ b/FormalConjectures/ErdosProblems/209.lean
@@ -34,9 +34,9 @@ open EuclideanGeometry Affine
 
 namespace Erdos209
 
-/-- A line in the plane: the affine span of two distinct points. -/
+/-- A line in the plane: an affine subspace whose direction is one-dimensional. -/
 def IsLine (L : AffineSubspace ℝ ℝ²) : Prop :=
-  ∃ p q : ℝ², p ≠ q ∧ L = affineSpan ℝ {p, q}
+  Module.finrank ℝ L.direction = 1
 
 /-- The number of lines from `A` that pass through the point `p`. -/
 noncomputable def pointMultiplicity (A : Finset (AffineSubspace ℝ ℝ²)) (p : ℝ²) : ℕ :=
diff --git a/FormalConjectures/ErdosProblems/353.lean b/FormalConjectures/ErdosProblems/353.lean
index 239b250490..788fe6035c 100644
--- a/FormalConjectures/ErdosProblems/353.lean
+++ b/FormalConjectures/ErdosProblems/353.lean
@@ -37,18 +37,6 @@ open scoped Real
 
 namespace Erdos353
 
-/--
-`a b c d` are the vertices, in counter-clockwise order, of an isosceles trapezoid:
-they are in strictly convex position, the side `ab` is parallel to the side `cd`
-(the two bases), and the diagonals `ac` and `bd` have equal length. One pair of
-parallel sides together with equal diagonals is the classical characterization of
-an isosceles trapezoid; in particular it rules out non-rectangular parallelograms.
--/
-def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop :=
-  IsCcwConvexPolygon ![a, b, c, d] ∧
-  line[ℝ, a, b] ∥ line[ℝ, c, d] ∧
-  dist a c = dist b d
-
 /--
 Let $A\subseteq \mathbb{R}^2$ be a measurable set with infinite measure. Must $A$ contain the
 vertices of an isosceles trapezoid of area $1$? What about an isosceles triangle, or a
@@ -85,7 +73,7 @@ non-degeneracy hypothesis is needed.
 theorem erdos_353.variants.isosceles_triangle :
     ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
       ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
-        (dist a b = dist a c ∨ dist b a = dist b c ∨ dist c a = dist c b) ∧
+        IsIsosceles a b c ∧
         volume (convexHull ℝ {a, b, c}) = 1 := by
   sorry
 
@@ -104,7 +92,7 @@ non-degeneracy hypothesis is needed.
 theorem erdos_353.variants.right_angled_triangle :
     ∀ A : Set ℝ², MeasurableSet A → volume A = ⊤ →
       ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A,
-        (∠ b a c = π / 2 ∨ ∠ a b c = π / 2 ∨ ∠ b c a = π / 2) ∧
+        IsRightAngled a b c ∧
         volume (convexHull ℝ {a, b, c}) = 1 := by
   sorry
 
diff --git a/FormalConjecturesForMathlib/Geometry/2d.lean b/FormalConjecturesForMathlib/Geometry/2d.lean
index 820f4e3cfd..8b71ef05d4 100644
--- a/FormalConjecturesForMathlib/Geometry/2d.lean
+++ b/FormalConjecturesForMathlib/Geometry/2d.lean
@@ -240,6 +240,23 @@ if no three are collinear and no four lie on a circle. -/
 def InGeneralPosition (X : Finset ℝ²) : Prop :=
   NonTrilinear (SetLike.coe X) ∧ ∀ T ⊆ X, #T = 4 → ¬Cospherical (SetLike.coe T)
 
+/-- `a b c` are the vertices of a right-angled triangle: the (unoriented) angle at one of the
+three vertices equals `π / 2`. -/
+def IsRightAngled (a b c : P) : Prop :=
+  ∠ b a c = π / 2 ∨ ∠ a b c = π / 2 ∨ ∠ b c a = π / 2
+
+/--
+`a b c d` are the vertices, in counter-clockwise order, of an isosceles trapezoid: they are in
+strictly convex position, the side `ab` is parallel to the side `cd` (the two bases), and the
+diagonals `ac` and `bd` have equal length. One pair of parallel sides together with equal
+diagonals is the classical characterization of an isosceles trapezoid; in particular it rules
+out non-rectangular parallelograms.
+-/
+def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop :=
+  IsCcwConvexPolygon ![a, b, c, d] ∧
+  (affineSpan ℝ {a, b}).Parallel (affineSpan ℝ {c, d}) ∧
+  dist a c = dist b d
+
 end EuclideanGeometry
 
 def IsIsosceles {α : Type*} [Dist α] (p q r : α) : Prop :=

From 8f6648ff0fbd771db53859cd436d37a8d6a68a57 Mon Sep 17 00:00:00 2001
From: Will Blair <85643015+williamjblair@users.noreply.github.com>
Date: Sun, 5 Jul 2026 13:09:33 -0400
Subject: [PATCH 4/4] Address review: extract shared defs to ForMathlib (426,
 512)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- 426: move IsUniqueSubgraph and uniqueSubgraphCount into a new
  FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean
  (generalized to any vertex type); add a @[category test] sanity check
- 512: extract the additive character e(x)=e^{2πix} into a shared
  FormalConjecturesForMathlib/Analysis/SpecialFunctions/AdditiveCharacter.lean;
  512 and 987 now reuse it instead of copy-pasting the definition
---
 FormalConjectures/ErdosProblems/426.lean      | 25 ++++--------
 FormalConjectures/ErdosProblems/512.lean      |  3 --
 FormalConjectures/ErdosProblems/987.lean      |  5 ---
 FormalConjecturesForMathlib.lean              |  2 +
 .../SpecialFunctions/AdditiveCharacter.lean   | 24 +++++++++++
 .../SimpleGraph/SubgraphIsomorphism.lean      | 40 +++++++++++++++++++
 6 files changed, 74 insertions(+), 25 deletions(-)
 create mode 100644 FormalConjecturesForMathlib/Analysis/SpecialFunctions/AdditiveCharacter.lean
 create mode 100644 FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean

diff --git a/FormalConjectures/ErdosProblems/426.lean b/FormalConjectures/ErdosProblems/426.lean
index a457465a14..b986f493ca 100644
--- a/FormalConjectures/ErdosProblems/426.lean
+++ b/FormalConjectures/ErdosProblems/426.lean
@@ -33,26 +33,17 @@ import FormalConjectures.Util.ProblemImports
 - [BrCh24] Bradač, D. and Christoph, M., *Unique subgraphs are rare*. arXiv:2410.16233 (2024).
 -/
 
-open Filter
+open Filter SimpleGraph
 
 namespace Erdos426
 
-/--
-`G` is a **unique subgraph** of `H` if there is exactly one subgraph of `H` isomorphic to `G`.
-Subgraphs of `H` are taken in the spanning sense: elements `G' ≤ H` of the lattice
-`SimpleGraph (Fin n)`, i.e. subsets of the edges of `H` (not necessarily induced).
--/
-def IsUniqueSubgraph {n : ℕ} (G H : SimpleGraph (Fin n)) : Prop :=
-  ∃! G' : SimpleGraph (Fin n), G' ≤ H ∧ Nonempty (G.Iso G')
-
-/--
-The number of distinct unique subgraphs of `H`: the number of isomorphism classes of graphs
-that occur exactly once as a subgraph of `H`. Each such class contains exactly one subgraph
-`G ≤ H` (uniqueness forbids a second isomorphic copy), so counting those representatives
-counts the classes.
--/
-noncomputable def uniqueSubgraphCount {n : ℕ} (H : SimpleGraph (Fin n)) : ℕ :=
-  {G : SimpleGraph (Fin n) | G ≤ H ∧ IsUniqueSubgraph G H}.ncard
+/-- Sanity check: the empty graph `⊥` is a unique subgraph of itself. Its only subgraph is `⊥`
+(everything `≤ ⊥` equals `⊥`), which is isomorphic to `⊥` via the identity. -/
+@[category test, AMS 5]
+theorem isUniqueSubgraph_bot_bot {V : Type*} : IsUniqueSubgraph (⊥ : SimpleGraph V) ⊥ := by
+  refine ⟨⊥, ⟨le_refl _, ⟨Iso.refl⟩⟩, ?_⟩
+  rintro G' ⟨hle, -⟩
+  exact le_bot_iff.mp hle
 
 /--
 We say $H$ is a unique subgraph of $G$ if there is exactly one way to find $H$ as a subgraph
diff --git a/FormalConjectures/ErdosProblems/512.lean b/FormalConjectures/ErdosProblems/512.lean
index 241db37b0d..5bb11509c3 100644
--- a/FormalConjectures/ErdosProblems/512.lean
+++ b/FormalConjectures/ErdosProblems/512.lean
@@ -31,9 +31,6 @@ import FormalConjectures.Util.ProblemImports
 
 namespace Erdos512
 
-/-- Shorthand for the additive character $e(x) = e^{2\pi i x}$. -/
-noncomputable def e (x : ℝ) : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)
-
 /--
 Is it true that, if $A\subset \mathbb{Z}$ is a finite set of size $N$, then
 \[\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N,\]
diff --git a/FormalConjectures/ErdosProblems/987.lean b/FormalConjectures/ErdosProblems/987.lean
index f302ac3db6..47be2687e1 100644
--- a/FormalConjectures/ErdosProblems/987.lean
+++ b/FormalConjectures/ErdosProblems/987.lean
@@ -46,11 +46,6 @@ formulation 1-indexing was used. This change does not affect the meaning of the
 In the description of the problem below we remain faithful to the original one.
 -/
 
-/-- Shorthand for the additive character $e(x) = e^{2 \pi i x}$.
-(Matches `Real.fourierChar` / `𝐞` from `Mathlib/Analysis/Complex/Circle.lean`, but
-kept as a local definition for readability across the many sites that use it.) -/
-noncomputable def e (x : ℝ) : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)
-
 /--
 For an infinite sequence $x_1, x_2, \ldots \in (0, 1)$, define
 $$A_k = \limsup_{n \to \infty} \left\lvert \sum_{j \le n} e(k x_j) \right\rvert,$$
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index 236fb37130..37f2bacc90 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -33,6 +33,7 @@ public import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
 public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
 public import FormalConjecturesForMathlib.Analysis.HasGaps
 public import FormalConjecturesForMathlib.Analysis.Real.Cardinality
+public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
 public import FormalConjecturesForMathlib.Combinatorics.AP.Basic
@@ -82,6 +83,7 @@ public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SizeRamsey
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Connectivity
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Matching
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SpanningTree
+public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SubgraphIsomorphism
 public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.UnitDistancePlaneGraph
 public import FormalConjecturesForMathlib.Combinatorics.YoungDiagram
 public import FormalConjecturesForMathlib.Computability.DFA
diff --git a/FormalConjecturesForMathlib/Analysis/SpecialFunctions/AdditiveCharacter.lean b/FormalConjecturesForMathlib/Analysis/SpecialFunctions/AdditiveCharacter.lean
new file mode 100644
index 0000000000..558ed78844
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/SpecialFunctions/AdditiveCharacter.lean
@@ -0,0 +1,24 @@
+/-
+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.
+-/
+module
+
+public import Mathlib.Analysis.SpecialFunctions.Complex.Circle
+
+@[expose] public section
+
+/-- The additive character `e(x) = e ^ (2 * π * i * x)`, a shorthand used across several
+exponential-sum problems. -/
+noncomputable def e (x : ℝ) : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)
diff --git a/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean
new file mode 100644
index 0000000000..c9724c0f88
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/SubgraphIsomorphism.lean
@@ -0,0 +1,40 @@
+/-
+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.
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Maps
+public import Mathlib.Data.Set.Card
+
+@[expose] public section
+
+namespace SimpleGraph
+
+variable {V : Type*}
+
+/-- `G` is a **unique subgraph** of `H` if there is exactly one subgraph of `H` isomorphic to
+`G`. Subgraphs of `H` are taken in the spanning sense: elements `G' ≤ H` of the lattice
+`SimpleGraph V`, i.e. subsets of the edges of `H` (not necessarily induced). -/
+def IsUniqueSubgraph (G H : SimpleGraph V) : Prop :=
+  ∃! G' : SimpleGraph V, G' ≤ H ∧ Nonempty (G.Iso G')
+
+/-- The number of distinct unique subgraphs of `H`: the number of isomorphism classes of graphs
+that occur exactly once as a subgraph of `H`. Each such class contains exactly one subgraph
+`G ≤ H` (uniqueness forbids a second isomorphic copy), so counting those representatives counts
+the classes. -/
+noncomputable def uniqueSubgraphCount (H : SimpleGraph V) : ℕ :=
+  {G : SimpleGraph V | G ≤ H ∧ IsUniqueSubgraph G H}.ncard
+
+end SimpleGraph