From 964f5b45fd73b3c1fa3d233d195b705dc6570daa Mon Sep 17 00:00:00 2001
From: Seewoo Lee <seewoo5@gmail.com>
Date: Tue, 30 Dec 2025 10:16:27 +0900
Subject: [PATCH 1/5] wip: WithBot N

---
 FormalConjectures/ErdosProblems/683.lean | 38 ++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 FormalConjectures/ErdosProblems/683.lean

diff --git a/FormalConjectures/ErdosProblems/683.lean b/FormalConjectures/ErdosProblems/683.lean
new file mode 100644
index 000000000..037ea2119
--- /dev/null
+++ b/FormalConjectures/ErdosProblems/683.lean
@@ -0,0 +1,38 @@
+/-
+Copyright 2025 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 683
+
+*Reference:* [erdosproblems.com/683](https://www.erdosproblems.com/683)
+-/
+
+namespace Erdos683
+
+/-- Let `P(n, k)` be the largest prime factor of `n choose k`. -/
+def P (n k : ℕ) : ℕ := (n.choose k).primeFactors.max
+
+/--
+There exists $c > 0$ such that $P(n, k) > \min\{n-k+1, k^{1 + c}\}$ for all $0 \le k \le n$.}
+-/
+@[category research open, AMS 11]
+theorem erdos_683 : (∃ c > 0, ∀ n k : ℕ, k ≤ n → P n k > min (n - k + 1) (k ^ (1 + c))) ↔
+    answer(sorry) := by
+  sorry
+
+end Erdos683

From 62d647345fd13e83752fed4a40d9638d2ad95911 Mon Sep 17 00:00:00 2001
From: Seewoo Lee <seewoo5@gmail.com>
Date: Wed, 7 Jan 2026 22:41:40 +0900
Subject: [PATCH 2/5] update

---
 FormalConjectures/ErdosProblems/683.lean | 45 +++++++++++++++++++++---
 1 file changed, 41 insertions(+), 4 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/683.lean b/FormalConjectures/ErdosProblems/683.lean
index 037ea2119..de996a2aa 100644
--- a/FormalConjectures/ErdosProblems/683.lean
+++ b/FormalConjectures/ErdosProblems/683.lean
@@ -19,20 +19,57 @@ import FormalConjectures.Util.ProblemImports
 /-!
 # Erdős Problem 683
 
-*Reference:* [erdosproblems.com/683](https://www.erdosproblems.com/683)
+*References:*
+- [erdosproblems.com/683](https://www.erdosproblems.com/683)
+- [Er34] Erdős, Paul, A Theorem of Sylvester and Schur. J. London Math. Soc. (1934), 282--288.
+- [Er55d] Erdős, P., On consecutive integers. Nieuw Arch. Wisk. (3) (1955), 124--128.
+- [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.
 -/
 
 namespace Erdos683
 
-/-- Let `P(n, k)` be the largest prime factor of `n choose k`. -/
-def P (n k : ℕ) : ℕ := (n.choose k).primeFactors.max
+def withBotToNat : WithBot ℕ → ℕ
+| ⊥       => 0
+| (n : ℕ) => n
+
+/--
+Let $P(n, k)$ be the largest prime factor of $\binom{n}{k}$.
+Note that `(n.choose k).primeFactors.max` returns a `WithBot ℕ` to account for the empty set case,
+so we convert it to `ℕ` with `withBotToNat`. Note that we will only consider the case where
+$0 < k < n$, so $\binom{n}{k}$ is always greater than 0 and thus has at least one prime factor.
+-/
+def P (n k : ℕ) : ℕ := withBotToNat (n.choose k).primeFactors.max
 
 /--
 There exists $c > 0$ such that $P(n, k) > \min\{n-k+1, k^{1 + c}\}$ for all $0 \le k \le n$.}
 -/
 @[category research open, AMS 11]
-theorem erdos_683 : (∃ c > 0, ∀ n k : ℕ, k ≤ n → P n k > min (n - k + 1) (k ^ (1 + c))) ↔
+theorem erdos_683 : (∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k < n → P n k > min (n - k + 1) (k ^ (1 + c))) ↔
     answer(sorry) := by
   sorry
 
+/--
+Sylvester and Schur [Er34] proved that $P(n, k) > k$ for $k \le n/2$.
+-/
+@[category research solved, AMS 11]
+theorem erdos_683.variant.sylvester_schur :
+    ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 → P n k > k := by
+  sorry
+
+/--
+Erdos [Er55d] improved this to $P(n, k) \gg k \log k $ for $k \le n/2$.
+-/
+@[category research solved, AMS 11]
+theorem erdos_683.variant.erdos_log :
+    ∃ C > 0, ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 → P n k ≥ C * k * Real.log k := by
+  sorry
+
+/--
+Standard heuristics suggest that $P(n, k) > e^{c\sqrt{k}}$ for some constant $c > 0$.
+-/
+@[category research open, AMS 11]
+theorem erdos_683.variant.exp_sqrt :
+    ∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 → P n k > Real.exp (c * Real.sqrt k) := by
+  sorry
+
 end Erdos683

From 002f9268c252621989cf9c4cad212ad027b8e4b9 Mon Sep 17 00:00:00 2001
From: Seewoo Lee <seewoo5@gmail.com>
Date: Wed, 7 Jan 2026 22:44:04 +0900
Subject: [PATCH 3/5] >= to >

---
 FormalConjectures/ErdosProblems/683.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FormalConjectures/ErdosProblems/683.lean b/FormalConjectures/ErdosProblems/683.lean
index de996a2aa..ee37369f4 100644
--- a/FormalConjectures/ErdosProblems/683.lean
+++ b/FormalConjectures/ErdosProblems/683.lean
@@ -61,7 +61,7 @@ Erdos [Er55d] improved this to $P(n, k) \gg k \log k $ for $k \le n/2$.
 -/
 @[category research solved, AMS 11]
 theorem erdos_683.variant.erdos_log :
-    ∃ C > 0, ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 → P n k ≥ C * k * Real.log k := by
+    ∃ C > 0, ∀ n k : ℕ, 0 < k ∧ k ≤ n / 2 → P n k > C * k * Real.log k := by
   sorry
 
 /--

From 05b323b55e959eb9bbb7fcc0c91a36d9b2796b83 Mon Sep 17 00:00:00 2001
From: Seewoo Lee <seewoo5@gmail.com>
Date: Wed, 7 Jan 2026 22:44:48 +0900
Subject: [PATCH 4/5] fix docstring

---
 FormalConjectures/ErdosProblems/683.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FormalConjectures/ErdosProblems/683.lean b/FormalConjectures/ErdosProblems/683.lean
index ee37369f4..9c630544f 100644
--- a/FormalConjectures/ErdosProblems/683.lean
+++ b/FormalConjectures/ErdosProblems/683.lean
@@ -36,7 +36,7 @@ def withBotToNat : WithBot ℕ → ℕ
 Let $P(n, k)$ be the largest prime factor of $\binom{n}{k}$.
 Note that `(n.choose k).primeFactors.max` returns a `WithBot ℕ` to account for the empty set case,
 so we convert it to `ℕ` with `withBotToNat`. Note that we will only consider the case where
-$0 < k < n$, so $\binom{n}{k}$ is always greater than 0 and thus has at least one prime factor.
+$0 < k < n$, so $\binom{n}{k}$ is always greater than 1 and thus has at least one prime factor.
 -/
 def P (n k : ℕ) : ℕ := withBotToNat (n.choose k).primeFactors.max
 

From 484f2df5ac42c787d0ec9aa01276a5db843e0757 Mon Sep 17 00:00:00 2001
From: Seewoo Lee <seewoo5@gmail.com>
Date: Thu, 8 Jan 2026 19:31:27 +0900
Subject: [PATCH 5/5] address comments

---
 FormalConjectures/ErdosProblems/683.lean | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/FormalConjectures/ErdosProblems/683.lean b/FormalConjectures/ErdosProblems/683.lean
index 9c630544f..9006699a5 100644
--- a/FormalConjectures/ErdosProblems/683.lean
+++ b/FormalConjectures/ErdosProblems/683.lean
@@ -28,24 +28,17 @@ import FormalConjectures.Util.ProblemImports
 
 namespace Erdos683
 
-def withBotToNat : WithBot ℕ → ℕ
-| ⊥       => 0
-| (n : ℕ) => n
-
 /--
 Let $P(n, k)$ be the largest prime factor of $\binom{n}{k}$.
-Note that `(n.choose k).primeFactors.max` returns a `WithBot ℕ` to account for the empty set case,
-so we convert it to `ℕ` with `withBotToNat`. Note that we will only consider the case where
-$0 < k < n$, so $\binom{n}{k}$ is always greater than 1 and thus has at least one prime factor.
 -/
-def P (n k : ℕ) : ℕ := withBotToNat (n.choose k).primeFactors.max
+def P (n k : ℕ) : ℕ := (n.choose k).primeFactors.sup id
 
 /--
 There exists $c > 0$ such that $P(n, k) > \min\{n-k+1, k^{1 + c}\}$ for all $0 \le k \le n$.}
 -/
 @[category research open, AMS 11]
-theorem erdos_683 : (∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k < n → P n k > min (n - k + 1) (k ^ (1 + c))) ↔
-    answer(sorry) := by
+theorem erdos_683 : answer(sorry) ↔
+    (∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k < n → P n k > min (n - k + 1) (k ^ (1 + c))) := by
   sorry
 
 /--