Number theory

Erdős 385 - part i

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

References

erdosproblems.com/385

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, n < Erdos385.F n

What you must prove

import FormalConjectures.ErdosProblems.«385»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos385.erdos_385.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/385.lean

Source type SHA-256: sha256:e0a15490e63d4ef5f148aac31e5734af8e484c8c66e63270c3eeb400885c8839
Task id: fc-379fc029-parts-i-f199e388e7-formalized-v1
Task commitment: sha256:4625ebfe5b6e2abc11da48b3aec7a3cd9bd364f4c357d255abe784e53180cc3a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.