Number theory

Erdős 680 - part i

Is it true that, for all sufficiently large

n

, there exists some

k

such that

p(n+k)>k^2+1,

where

p(m)

denotes the least prime factor of

m

References

erdosproblems.com/680

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k, k ≠ 0 ∧ (n + k).minFac > k ^ 2 + 1

What you must prove

import FormalConjectures.ErdosProblems.«680»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos680.erdos_680.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/680.lean

Source type SHA-256: sha256:a292ac9e35cbfe36e6d320deb79800e71407341bea0c39a3973fce08db16a7c4
Task id: fc-379fc029-parts-i-02a08df32d-formalized-v1
Task commitment: sha256:7bffab2ea16be513505d7b946818c374bc01d817b3dbd810497a9298beaad169

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.