1. FormalConjectures
  2. ErdosProblems
  3. «385»
/- 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 FormalConjecturesUtil

Erdős Problem 385

Reference: erdosproblems.com/385

namespace Erdos385 open Filter

Let $F(n) := \max{m + p(m) \mid \textrm{$m < n$ composite}}}$ where $p(m)$ is the least prime divisor of $m$.

noncomputable def F (n : ℕ) : ℕ := sSup {m + m.minFac | (m < n) (_ : m.Composite)}

Note that trivially $F(n) \leq n + \sqrt{n}$.

@[category test, AMS 11] theorem trivial_ub (n : ℕ) : F n ≤ n + √n := n:ℕ⊢ ↑(F n) ≤ ↑n + √↑n have hkey : F n ≤ n + n.sqrt := n:ℕ⊢ ↑(F n) ≤ ↑n + √↑n n:ℕ⊢ n + n.sqrt ∈ upperBounds {x | ∃ m < n, ∃ (_ : m.Composite), m + m.minFac = x} n:ℕm:ℕhm:m < nhcomp:m.Composite⊢ m + m.minFac ≤ n + n.sqrt have h1 : 0 < m := n:ℕ⊢ ↑(F n) ≤ ↑n + √↑n n:ℕm:ℕhm:m < nhcomp:m.Compositethis:1 < m := hcomp.left⊢ 0 < m; All goals completed! 🐙 n:ℕm:ℕhm:m < nhcomp:m.Compositeh1:0 < m := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp ahsq:m.minFac ^ 2 ≤ m := Nat.minFac_sq_le_self h1 hcomp.right⊢ m + m.minFac ≤ n + n.sqrt have hmf : m.minFac ≤ m.sqrt := Nat.le_sqrt.mpr (n:ℕm:ℕhm:m < nhcomp:m.Compositeh1:0 < m := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp ahsq:m.minFac ^ 2 ≤ m := Nat.minFac_sq_le_self h1 hcomp.right⊢ m.minFac * m.minFac ≤ m n:ℕm:ℕhm:m < nhcomp:m.Compositeh1:0 < m := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp ahsq:m.minFac ^ 2 ≤ m := Nat.minFac_sq_le_self h1 hcomp.right⊢ m.minFac ^ 2 ≤ m; All goals completed! 🐙) n:ℕm:ℕhm:m < nhcomp:m.Compositeh1:0 < m := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp ahsq:m.minFac ^ 2 ≤ m := Nat.minFac_sq_le_self h1 hcomp.righthmf:m.minFac ≤ m.sqrt := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq)hmn:m.sqrt ≤ n.sqrt := Nat.sqrt_le_sqrt (LT.lt.le hm)⊢ m + m.minFac ≤ n + n.sqrt All goals completed! 🐙 calc (F n : ℝ) ≤ ((n + n.sqrt : ℕ) : ℝ) := n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ ↑(F n) ≤ ↑(n + n.sqrt) All goals completed! 🐙 _ = n + (n.sqrt : ℝ) := n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ ↑(n + n.sqrt) = ↑n + ↑n.sqrt n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ ↑n + ↑n.sqrt = ↑n + ↑n.sqrt; All goals completed! 🐙 _ ≤ n + √n := n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ ↑n + ↑n.sqrt ≤ ↑n + √↑n n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ ↑n.sqrt ≤ √↑n n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ √↑(n.sqrt ^ 2) ≤ √↑n exact Real.sqrt_le_sqrt (n:ℕhkey:F n ≤ n + n.sqrt := csSup_le' fun ⦃x⦄ a => Exists.casesOn a fun m h => And.casesOn h fun hm right => Exists.casesOn right fun hcomp h => h ▸ have h1 := have this := hcomp.left; Decidable.byContradiction fun a => trivial_ub._proof_1 n m hcomp a; have hsq := Nat.minFac_sq_le_self h1 hcomp.right; have hmf := Nat.le_sqrt.mpr (Eq.mpr (id (congrArg (fun _a => _a ≤ m) (Eq.symm (sq m.minFac)))) hsq); have hmn := Nat.sqrt_le_sqrt (LT.lt.le hm); Decidable.byContradiction fun a => trivial_ub._proof_2 n m hm hmf hmn a⊢ ↑(n.sqrt ^ 2) ≤ ↑n All goals completed! 🐙)

Let $F(n) := \max{m + p(m) \mid \textrm{$m < n$ composite}}}$ where $p(m)$ is the least prime divisor of $m$. Is it true that $F(n)>n$ for all sufficiently large $n$?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_385.parts.i : answer(sorry) ↔ ∀ᶠ n in atTop, n < F n := ⊢ True ↔ ∀ᶠ (n : ℕ) in atTop, n < F n All goals completed! 🐙

Let $F(n) := \max{m + p(m) \mid \textrm{$m < n$ composite}}}$ where $p(m)$ is the least prime divisor of $m$. Does $F(n) - n \to \infty$ as $n\to\infty$?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_385.parts.ii : answer(sorry) ↔ atTop.Tendsto (fun n ↦ F n - n) atTop := ⊢ True ↔ Tendsto (fun n => F n - n) atTop atTop All goals completed! 🐙

A question of Erdős, Eggleton, and Selfridge, who write that in fact it is possible that this quantity is always at least $n+(1-o(1))\sqrt{n}$

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_385.variants.lb : answer(sorry) ↔ ∃ (e : ℕ → ℝ) (he : e =o[atTop] (1 : ℕ → ℝ)), ∀ n, n + (1 - e n) * √n ≤ F n := sorry end Erdos385