ErdosProblems: add 71, 206, 209, 328, 353, 403, 426, 464, 512, 621, 639, 648 (#3998 sync)

FormalConjectures/ErdosProblems/206.lean

@@ -0,0 +1,98 @@
+/-
+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)
+- [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).
+-/
+
+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 ℕ) : ℝ :=
+  ∑ m ∈ S, (1 : ℝ) / m
+
+/-- `S` is an Egyptian underapproximation of `x`: valid denominators (all positive) and sum < x. -/
+def IsUnderapprox (S : Finset ℕ) (x : ℝ) : Prop :=
+  (∀ 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)$. -/
+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

FormalConjectures/ErdosProblems/209.lean

@@ -0,0 +1,74 @@
+/-
+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)
+- [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
+  plane*. C. R. Math. Acad. Sci. Paris (2016), 551-554.
+-/
+
+open EuclideanGeometry Affine
+
+namespace Erdos209
+
+/-- A line in the plane: an affine subspace whose direction is one-dimensional. -/
+def IsLine (L : AffineSubspace ℝ ℝ²) : Prop :=
+  Module.finrank ℝ L.direction = 1
+
+/-- 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

FormalConjectures/ErdosProblems/328.lean

@@ -0,0 +1,61 @@
+/-
+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)
+- [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*.
+  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

FormalConjectures/ErdosProblems/353.lean

@@ -0,0 +1,129 @@
+/-
+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)
+- [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
+  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
+
+/--
+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,
+        IsIsosceles a b c ∧
+        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,
+        IsRightAngled a b c ∧
+        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