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

Adding formalized lean sources.

There's a few exceptions that I've caught:
1) 303 was actually written in lean3 and the only category annotation is
`lean4`. Maybe we add a `lean3` annotation?
2) The URL for 303 is actually way too long, even for URL shorteners
because it's using live.looken.cn. I'm leaving this out for now until we
figure how we want to reference it.

Also took the liberty to fix up some of the docstrings and references.

Closes #2334
Closes #2335
Closes #2336
Closes #2337
Closes #2338
Closes #2339
Closes #2340
Closes #2341
Closes #2342
Closes #2343 
Closes #2344 
Closes #2345
Closes #2346 
Closes #2347 
Closes #2348 
Closes #2349 
Closes #2350 
Closes #2351
Closes #2352 
Closes #2353 
Closes #2354
Closes #2355

Author: danielchin

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