From f79434a3ad974adc6d80a7e71cbecb8cd9536de7 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 7 Jan 2026 10:22:36 +0100 Subject: [PATCH 1/6] Fix erdos_859 - The LHS of the previous version was a constant function within the asymptotic equivalence. It needs to vary with t. - Fix typing of some constants which were previously inferred as Nat Co-authored-by: Salvatore Mercuri --- FormalConjectures/ErdosProblems/859.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/FormalConjectures/ErdosProblems/859.lean b/FormalConjectures/ErdosProblems/859.lean index f8350345c..f62a33ed4 100644 --- a/FormalConjectures/ErdosProblems/859.lean +++ b/FormalConjectures/ErdosProblems/859.lean @@ -37,9 +37,9 @@ The density `dₜ` of `DivisorSumSet (t : ℕ)` is bounded from below by `1 / lo from above by `1 / log (t) ^ c₄` for some positive constants `c₃` and `c₄`. -/ @[category research solved, AMS 11] -theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > 0) (c₄ > 0) (t₀ : ℕ), ∀ t > t₀, - ∃ dₜ : ℝ, ((DivisorSumSet t).HasDensity dₜ) ∧ - (1 / (Real.log t)^c₃ < dₜ) ∧ (dₜ < 1 / (Real.log t)^c₄) := by +theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ), + ∀ t > t₀, ∃ dₜ : ℝ, ((DivisorSumSet t).HasDensity dₜ) ∧ + (1 / (Real.log t) ^ c₃ < dₜ) ∧ (dₜ < 1 / (Real.log t) ^ c₄) := by sorry @@ -49,8 +49,9 @@ The density `dₜ` of `DivisorSumSet (t : ℕ)` is assymptotically equivalent to for some positive constants `c₁` and `c₂`. -/ @[category research open, AMS 11] -theorem erdos_859 (t : ℕ) : ∃ c₁ > 0, ∃ c₂ > 0, ∃ dₜ : ℝ, ((DivisorSumSet t).HasDensity dₜ) ∧ - (fun (t : ℕ) ↦ dₜ) ~[atTop] (fun t ↦ c₁ / (Real.log t)^c₂ ) := by +theorem erdos_859 : + ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, ((DivisorSumSet t).HasDensity (d t))) ∧ + (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / (Real.log t) ^ c₂) := by sorry /- From 8d32a856df6e3dcc88a715157f2b944087ecbb3f Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 7 Jan 2026 13:47:18 +0100 Subject: [PATCH 2/6] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- FormalConjectures/ErdosProblems/859.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/859.lean b/FormalConjectures/ErdosProblems/859.lean index f62a33ed4..2942610f9 100644 --- a/FormalConjectures/ErdosProblems/859.lean +++ b/FormalConjectures/ErdosProblems/859.lean @@ -51,7 +51,7 @@ for some positive constants `c₁` and `c₂`. @[category research open, AMS 11] theorem erdos_859 : ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, ((DivisorSumSet t).HasDensity (d t))) ∧ - (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / (Real.log t) ^ c₂) := by + (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / Real.log t ^ c₂) := by sorry /- From d91b3ab85c221f649ee3d47853a193c5359c7210 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 7 Jan 2026 13:47:25 +0100 Subject: [PATCH 3/6] Update FormalConjectures/ErdosProblems/859.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- FormalConjectures/ErdosProblems/859.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/859.lean b/FormalConjectures/ErdosProblems/859.lean index 2942610f9..74fea0f41 100644 --- a/FormalConjectures/ErdosProblems/859.lean +++ b/FormalConjectures/ErdosProblems/859.lean @@ -38,7 +38,7 @@ from above by `1 / log (t) ^ c₄` for some positive constants `c₃` and `c₄` -/ @[category research solved, AMS 11] theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ), - ∀ t > t₀, ∃ dₜ : ℝ, ((DivisorSumSet t).HasDensity dₜ) ∧ + ∀\^f t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧ (1 / (Real.log t) ^ c₃ < dₜ) ∧ (dₜ < 1 / (Real.log t) ^ c₄) := by sorry From e68844853270e407eed32aa01633cabd1f2067ef Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 7 Jan 2026 13:47:31 +0100 Subject: [PATCH 4/6] Update FormalConjectures/ErdosProblems/859.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- FormalConjectures/ErdosProblems/859.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/859.lean b/FormalConjectures/ErdosProblems/859.lean index 74fea0f41..eca5277b5 100644 --- a/FormalConjectures/ErdosProblems/859.lean +++ b/FormalConjectures/ErdosProblems/859.lean @@ -39,7 +39,7 @@ from above by `1 / log (t) ^ c₄` for some positive constants `c₃` and `c₄` @[category research solved, AMS 11] theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ), ∀\^f t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧ - (1 / (Real.log t) ^ c₃ < dₜ) ∧ (dₜ < 1 / (Real.log t) ^ c₄) := by + 1 / Real.log t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log t ^ c₄ := by sorry From a42273b83985ca9f699dd33268e0bbc51fcdd076 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 7 Jan 2026 13:47:36 +0100 Subject: [PATCH 5/6] Update FormalConjectures/ErdosProblems/859.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- FormalConjectures/ErdosProblems/859.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/859.lean b/FormalConjectures/ErdosProblems/859.lean index eca5277b5..60fa84892 100644 --- a/FormalConjectures/ErdosProblems/859.lean +++ b/FormalConjectures/ErdosProblems/859.lean @@ -50,7 +50,7 @@ for some positive constants `c₁` and `c₂`. -/ @[category research open, AMS 11] theorem erdos_859 : - ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, ((DivisorSumSet t).HasDensity (d t))) ∧ + ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, (DivisorSumSet t).HasDensity (d t)) ∧ (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / Real.log t ^ c₂) := by sorry From 9ba09d1d64b4c069f31299cb8716236eb704a7f2 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 12 Jan 2026 22:11:28 +0000 Subject: [PATCH 6/6] Apply suggestions from code review --- FormalConjectures/ErdosProblems/859.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/859.lean b/FormalConjectures/ErdosProblems/859.lean index 60fa84892..79c716788 100644 --- a/FormalConjectures/ErdosProblems/859.lean +++ b/FormalConjectures/ErdosProblems/859.lean @@ -38,7 +38,7 @@ from above by `1 / log (t) ^ c₄` for some positive constants `c₃` and `c₄` -/ @[category research solved, AMS 11] theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ), - ∀\^f t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧ + ∀ᶠ t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧ 1 / Real.log t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log t ^ c₄ := by sorry