fix(ErdosProblems): Add formalized lean sources to Erdos Problems

FormalConjectures/ErdosProblems/1043.lean

@@ -18,7 +18,14 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 1043
 
-*Reference:* [erdosproblems.com/1043](https://www.erdosproblems.com/1043)
+*References:*
+- [erdosproblems.com/1043](https://www.erdosproblems.com/1043)
+- [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J.
+  Analyse Math. (1958), 125-148.
+- [Po59] Pommerenke, Ch., On some problems by Erdős, Herzog and Piranian. Michigan Math. J.
+  (1959), 221-225.
+- [Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961),
+  97-115.
 -/
 
 namespace Erdos1043
@@ -38,10 +45,10 @@ onto $\ell$ has measure at most $2$?
 
 Pommerenke [Po61] proved that the answer is no.
 
-[Po61] Pommerenke, Ch., _On metric properties of complex polynomials._ Michigan Math. J. (1961),
-97-115.
+This was formalized in Lean by Alexeev using Aristotle.
 -/
-@[category research solved, AMS 28 30]
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1043.lean", AMS 28 30]
 theorem erdos_1043 :
     answer(False) ↔ ∀ (f : ℂ[X]), f.Monic → f.degree ≥ 1 →
       ∃ (u : ℂ), ‖u‖ = 1 ∧

FormalConjectures/ErdosProblems/1067.lean

@@ -50,8 +50,11 @@ chromatic number $\aleph_1$?
 Komjáth [Ko13] proved that it is consistent that the answer is no. This was improved by
 Soukup [So15], who constructed a counterexample using no extra set-theoretical assumptions. A
 simpler elementary example was given by Bowler and Pitz [BoPi24].
+
+This was formalized in Lean by Alexeev using Aristotle and Aleph Prover.
 -/
-@[category research solved, AMS 5]
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1067.lean", AMS 5]
 theorem erdos_1067 :
     answer(False) ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
       ∃ (H : G.Subgraph), H.coe.chromaticCardinal = ℵ_ 1 ∧ InfinitelyConnected H.coe := by

FormalConjectures/ErdosProblems/1071.lean

@@ -32,9 +32,14 @@ namespace Erdos1071
 def SegmentsDisjoint (seg1 seg2 : ℝ² × ℝ²) : Prop :=
   segment ℝ seg1.1 seg1.2 ∩ segment ℝ seg2.1 seg2.2 ⊆ {seg1.1, seg1.2, seg2.1, seg2.2}
 
-/-- Can a finite set of disjoint unit segments in a unit square be maximal?
-Solved affirmatively by [Da85], who gave an explicit construction. -/
-@[category research solved, AMS 52]
+/--
+Can a finite set of disjoint unit segments in a unit square be maximal?
+Solved affirmatively by [Da85], who gave an explicit construction.
+
+This was formalized in Lean by Alexeev using Aristotle and ChatGPT.
+-/
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos1071.lean", AMS 52]
 theorem erdos_1071a :
     answer(True) ↔ ∃ S : Finset (ℝ² × ℝ²),
       Maximal (fun T : Finset (ℝ² × ℝ²) =>

FormalConjectures/ErdosProblems/189.lean

@@ -45,8 +45,12 @@ Solved (with answer `False`, as formalised below) in:
 Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023
 https://arxiv.org/abs/2309.09973
 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each
-monochromatic region is Lebesgue measurable and has measure zero). -/
-@[category research solved, AMS 5 51]
+monochromatic region is Lebesgue measurable and has measure zero).
+
+This was formalized in Lean by Alexeev and Kovac using Aristotle.
+-/
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos189.lean", AMS 5 51]
 theorem erdos_189 :
     answer(False) ↔ Erdos189For
       (fun a b c d ↦

FormalConjectures/ErdosProblems/198.lean

@@ -19,7 +19,10 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 198
 
-*Reference:* [erdosproblems.com/198](https://www.erdosproblems.com/198)
+*References:*
+- [erdosproblems.com/198](https://www.erdosproblems.com/198)
+- [Ba75] Baumgartner, James E., Partitioning vector spaces. J. Combinatorial Theory Ser. A (1975),
+  231-233.
 -/
 
 open Function Set Nat
@@ -31,9 +34,8 @@ positive integer. Then there is a set $X_k \subseteq V$ such that $X_k$ meets
 every infinite arithmetic progression in $V$ but $X_k$ intersects every
 $k$-element arithmetic progression in at most two points.
 
-At the end of:
- * Baumgartner, James E., Partitioning vector spaces. J. Combinatorial Theory Ser. A (1975), 231-233.
-the author claims that by "slightly modifying the method of [his proof]", one can prove this. -/
+At the end of [Ba75] the author claims that by "slightly modifying the method of [his proof]", one
+can prove this. -/
 @[category research solved, AMS 5]
 lemma baumgartner_strong (V : Type*) [AddCommGroup V] [Module ℚ V] (k : ℕ) :
     ∃ X : Set V,
@@ -50,31 +52,24 @@ lemma baumgartner_headline (V : Type*) [AddCommGroup V] [Module ℚ V] :
   baumgartner_strong V 3
 
 /--
-If $A \subseteq \mathbb{N}$ is a Sidon set then must the complement of $A$ contain an infinite arithmetic
-progression?
+The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to
+the paper [Ba75], which does not state this exactly, but the following simple construction is
+implicit in [Ba75].
 
-Answer "yes" according to remark on page 23 of:
+Let $P_1,P_2,\ldots$ be an enumeration of all countably many infinite arithmetic progressions. We
+choose $a_1$ to be the minimal element of $P_1\cap \mathbb{N}$, and in general choose $a_n$ to be an
+element of $P_n\cap \mathbb{N}$ such that $a_n>2a_{n-1}$. By construction $A=\{a_1 < a_2 < \cdots\}$
+contains at least one element from every infinite arithmetic progression, and is a lacunary set, so
+is certainly Sidon.
 
+AlphaProof has found the following explicit construction: $A = \{ (n+1)!+n : n\geq 0\}$. This is a
+Sidon set, and intersects every arithmetic progression, since for any $a,d\in \mathbb{N}$,
+$(a+d+1)!+(a+d)\in A$, and $d$ divides $(a+d+1)!+d$.
 
-- Erdös and Graham, "Old and new problems and results in combinatorial number theory", 1980.
-
-
-"Baumgartner also proved the conjecture of Erdös that if $A$ is a sequence of positive integers with
-all sums $a + a'$ distinct for $a, a' \in A$ then the complement of $A$ contains an
-infinite A.P."
-
-
-But this seems to be a misprint, since the opposite is true:
-There is a sequence of positive integers with all $a + a'$ distinct for $a, a' \in A$ such that the
-complement of $A$ contains no infinite A.P., i.e. there is a Sidon set $A$ which intersects all
-arithmetic progressions.
-
-So the answer should be "no".
-
-This can be seen, as pointed out by Thomas Bloom [erdosproblems.com/198](https://www.erdosproblems.com/198),
-by an elementary argument.
+This was formalized in Lean by Alexeev using Aristotle.
 -/
-@[category research solved, AMS 5 11]
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos198.lean", AMS 5 11]
 theorem erdos_198 : (∀ A : Set ℕ, IsSidon A → (∃ Y, IsAPOfLength Y ⊤ ∧ Y ⊆ Aᶜ)) ↔
     answer(False) := by
   sorry

FormalConjectures/ErdosProblems/229.lean

@@ -19,24 +19,28 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 229
 
-*Reference:* [erdosproblems.com/229](https://www.erdosproblems.com/229)
+*References:*
+- [erdosproblems.com/229](https://www.erdosproblems.com/229)
+- [BaSc72] Barth, K. F. and Schneider, W. J., On a problem of Erd\H{o}s concerning the zeros of the
+  derivatives of an entire function. Proc. Amer. Math. Soc. (1972), 229--232.
+- [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180.
 -/
 
 namespace Erdos229
 
 /--
 Let $(S_n)_{n \ge 1}$ be a sequence of sets of complex numbers, none of which have a finite
 limit point. Does there exist an entire transcendental function $f(z)$ such that, for all $n \ge 1$, there
-exists some $k_n \ge 0$ such that
-$$
-  f^{(k_n)}(z) = 0 \quad \text{for all } z \in S_n?
-$$
+exists some $k_n \ge 0$ such that $f^{(k_n)}(z) = 0$ for all $z \in S_n$.
+
+This is Problem 2.30 in [Ha74], where it is attributed to Erdős.
 
 Solved in the affirmative by Barth and Schneider [BaSc72].
 
-[BaSc72] Barth, K. F. and Schneider, W. J., _On a problem of Erdős concerning the zeros of_
-_the derivatives of an entire function_. Proc. Amer. Math. Soc. (1972), 229--232. -/
-@[category research solved, AMS 30]
+This was formalized in Lean by Alexeev using Aristotle.
+-/
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos229.lean", AMS 30]
 theorem erdos_229 :
     letI := Polynomial.algebraPi ℂ ℂ ℂ
     answer(True) ↔ ∀ (S : ℕ → Set ℂ), (∀ n, derivedSet (S n) = ∅) →

FormalConjectures/ErdosProblems/275.lean

@@ -35,8 +35,11 @@ necessarily distinct) covers $2^r$ consecutive integers then it covers all integ
 
 This is best possible as the system $2^{i-1}\pmod{2^i}$ shows. This was proved independently by
 Selfridge and Crittenden and Vanden Eynden [CrVE70].
+
+This was formalized in Lean by Alexeev using Aristotle.
 -/
-@[category research solved, AMS 11]
+@[category research formally solved using lean4 at
+"https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos275.lean", AMS 11]
 theorem erdos_275 (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ)
     (H : ∃ k : ℤ, ∀ x ∈ Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD n i]) (x : ℤ) :
     ∃ i, x ≡ a i [ZMOD n i] := by

FormalConjectures/ErdosProblems/298.lean

@@ -19,21 +19,23 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 298
 
-*Reference:* [erdosproblems.com/298](https://www.erdosproblems.com/298)
+*References:*
+- [erdosproblems.com/298](https://www.erdosproblems.com/298)
+- [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).
 -/
 
 namespace Erdos298
 
-/-- Does every set $A \subseteq \mathbb{N}$ of positive density contain some finite $S \subset A$ such that
+/--
+Does every set $A \subseteq \mathbb{N}$ of positive density contain some finite $S \subset A$ such that
 $\sum_{n \in S} \frac{1}{n} = 1$?
 
 The answer is yes, proved by Bloom [Bl21].
 
-[Bl21] Bloom, T. F., _On a density conjecture about unit fractions_. arXiv:2112.03726 (2021).
-
-Note: The solution to this problem has been formalized in Lean 3 by T. Bloom and B. Mehta, see
-https://github.com/b-mehta/unit-fractions -/
-@[category research solved, AMS 11]
+This was formalized in Lean 3 by Bloom and Mehta.
+-/
+@[category research formally solved using other_system at
+"https://github.com/b-mehta/unit-fractions/blob/master/src/final_results.lean", AMS 11]
 theorem erdos_298 : answer(True) ↔ (∀ (A : Set ℕ), 0 ∉ A → A.HasPosDensity →
     ∃ (S : Finset ℕ), ↑S ⊆ A ∧ ∑ n ∈ S, (1 / n : ℚ) = 1) := by
   sorry

FormalConjectures/ErdosProblems/299.lean

@@ -19,7 +19,10 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 299
 
-*Reference:* [erdosproblems.com/299](https://www.erdosproblems.com/299)
+*References:*
+- [erdosproblems.com/298](https://www.erdosproblems.com/298)
+- [erdosproblems.com/299](https://www.erdosproblems.com/299)
+- [Bl21] Bloom, T. F., On a density conjecture about unit fractions. arXiv:2112.03726 (2021).
 -/
 
 open Filter
@@ -29,8 +32,14 @@ namespace Erdos299
 /--
 Is there an infinite sequence $a_1 < a_2 < \dots$ such that $a_{i+1} - a_i = O(1)$ and no finite
 sum of $\frac{1}{a_i}$ is equal to 1?
+
+There does not exist such a sequence, which follows from the positive solution to
+[erdosproblems.com/298] by Bloom [Bl21].
+
+This was formalized in Lean 3 by Bloom and Mehta.
 -/
-@[category research solved, AMS 11 40]
+@[category research formally solved using other_system at
+"https://github.com/b-mehta/unit-fractions/blob/master/src/final_results.lean", AMS 11 40]
 theorem erdos_299 : answer(False) ↔ (∃ (a : ℕ → ℕ),
     StrictMono a ∧ (∀ n, 0 < a n) ∧
     (fun n ↦ (a (n + 1) : ℝ) - a n) =O[atTop] (1 : ℕ → ℝ) ∧
@@ -44,8 +53,6 @@ with sets of positive density, as follows from [Bl21].
 The statement is as follows:
 If $A \subset \mathbb{N}$ has positive upper density (and hence certainly if $A$ has positive
 density) then there is a finite $S \subset A$ such that $\sum_{n \in S} \frac{1}{n} = 1$.
-
-[Bl21] Bloom, T. F., On a density conjecture about unit fractions.
 -/
 @[category research solved, AMS 11 40]
 theorem erdos_299.variants.density : ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity →

FormalConjectures/ErdosProblems/303.lean

@@ -19,21 +19,24 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 303
 
-*Reference:* [erdosproblems.com/303](https://www.erdosproblems.com/303)
+*References:*
+- [erdosproblems.com/303](https://www.erdosproblems.com/303)
+- [BrRo91] Brown, Tom C. and Rödl, Voijtech, Monochromatic solutions to equations with unit
+  fractions. Bull. Austral. Math. Soc. (1991), 387-392.
 -/
 
 namespace Erdos303
 
-/-- Is it true that in any finite colouring of the integers there exists a monochromatic solution
+/--
+Is it true that in any finite colouring of the integers there exists a monochromatic solution
 to $\frac 1 a = \frac 1 b + \frac 1 c$ with distinct $a, b, c$?
 
 This is true, as proved by Brown and Rödl [BrRo91].
 
-[BrRo91] Brown, Tom C. and Rödl, Voijtech,
-_Monochromatic solutions to equations with unit fractions_.
-Bull. Austral. Math. Soc. (1991), 387-392.
+This was formalized in Lean by Yuan using Seed-Prover.
 -/
-@[category research solved, AMS 5 11]
+@[category research formally solved using lean4 at
+"https://www.erdosproblems.com/forum/thread/303", AMS 5 11]
 theorem erdos_303 :
     answer(True) ↔
     -- For any finite colouring of the integers

FormalConjectures/ErdosProblems/316.lean

@@ -19,20 +19,27 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 316
 
-*Reference:* [erdosproblems.com/316](https://www.erdosproblems.com/316)
+*References:*
+- [erdosproblems.com/316](https://www.erdosproblems.com/316)
+- [Sa97] Sándor, Csaba, On a problem of Erdős. J. Number Theory (1997), 203-210.
 -/
 
 namespace Erdos316
 
-/-- Is it true that if $A \subseteq \mathbb{N}\setminus\{1\}$ is a finite set with
+/--
+Is it true that if $A \subseteq \mathbb{N}\setminus\{1\}$ is a finite set with
 $\sum_{n \in A} \frac{1}{n} < 2$ then there is a partition $A=A_1 \sqcup A_2$
 such that $\sum_{n \in A_i} \frac{1}{n} < 1$ for $i=1,2$?
 
 This is not true in general, as shown by Sándor [Sa97].
 
-[Sa97] S\'{A}ndor, Csaba, _On a problem of Erdős_. J. Number Theory (1997), 203-210.
+The minimal counterexample is $\{2,3,4,5,6,7,10,11,13,14,15\}$, found by Tom Stobart.
+
+This was formalized in Lean by Mehta.
 -/
-@[category research solved, AMS 5 11]
+@[category research formally solved using lean4 at
+"https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/316.lean",
+AMS 5 11]
 theorem erdos_316 : answer(False) ↔ ∀ A : Finset ℕ, 0 ∉ A → 1 ∉ A →
     ∑ n ∈ A, (1 / n : ℚ) < 2 → ∃ (A₁ A₂ : Finset ℕ),
       Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧
@@ -46,7 +53,7 @@ theorem erdos_316 : answer(False) ↔ ∀ A : Finset ℕ, 0 ∉ A → 1 ∉ A 
     exact this ▸ h B (by simp [hA]) hlt
   decide +kernel
 
-/-- It is not true if `A` is a multiset (easier) -/
+/-- This is not true if $A$ is a multiset, for example $2,3,3,5,5,5,5$. -/
 @[category high_school, AMS 5 11]
 lemma erdos_316.variants.multiset : ∃ A : Multiset ℕ, 0 ∉ A ∧ 1 ∉ A ∧
     (A.map ((1 : ℚ) / ·)).sum < 2 ∧ ∀ (A₁ A₂ : Multiset ℕ),
@@ -63,9 +70,12 @@ lemma erdos_316.variants.multiset : ∃ A : Multiset ℕ, 0 ∉ A ∧ 1 ∉ A 
     exact this ▸ h B (by simp [hBC])
   decide +kernel
 
-/-- More generally, Sándor shows that for any $n \ge 2$ there exists a finite set
-$A \subseteq \mathbb{N}\setminus\{1\}$ with $\sum_{k \in A} \frac{1}{k} < n$, and no
-partition into $n$ parts each of which has $\sum_{n \in A_i} \frac{1}{n} < 1$. -/
+/--
+This is not true in general, as shown by Sándor [Sa97], who observed that the proper divisors of
+$120$ form a counterexample. More generally, Sándor shows that for any $n\geq 2$ there exists a
+finite set $A\subseteq \mathbb{N}\backslash\{1\}$ with $\sum_{k\in A}\frac{1}{k} < n$ and no
+partition into $n$ parts each of which has $\sum_{k\in A_i}\frac{1}{k}<1$.
+-/
 @[category research solved, AMS 5 11]
 theorem erdos_316.variants.generalized (n : ℕ) (hn : 2 ≤ n) : ∃ A : Finset ℕ,
     A.Nonempty ∧ 0 ∉ A ∧ 1 ∉ A ∧ ∑ k ∈ A, (1 / k : ℚ) < n ∧ ∀ P : Finpartition A,

FormalConjectures/ErdosProblems/331.lean

@@ -37,8 +37,11 @@ Ruzsa has observed that there is a simple counterexample: take $A$ to be the set
 binary representation has only non-zero digits in even places, and $B$ similarly but with non-zero
 digits only in odd places. It is easy to see $A$ and $B$ both grow like $\gg N^{1/2}$ and yet for
 any $n\geq 1$ there is exactly one solution to $n=a+b$ with $a\in A$ and $b\in B$.
+
+This was formalized in Lean by van Doorn using Aristotle.
 -/
-@[category research solved, AMS 11]
+@[category research formally solved using lean4 at
+"https://github.com/Woett/Lean-files/blob/main/ErdosProblem%23331.lean", AMS 11]
 theorem erdos_331 :
     answer(False) ↔
       ∀ A B : Set ℕ,