Conjectures.io

Number theory

Erdős 889 - general

Let vl(n)=max⁡k≥lv(n,k)v_l(n) = \max_{k\geq l} v(n,k). For every fixed ll, vl(n)→∞v_l(n) \to \infty as n→∞n \to \infty [ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

References

No one has attempted this yet.

Formal statement

Lean type

∀ (l : ℕ), Filter.Tendsto (Erdos889.v_l l) Filter.atTop (nhds ⊤)

What you must prove

import FormalConjectures.ErdosProblems.«889»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos889.erdos_889.variants.general" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/889.lean

Source type SHA-256
sha256:8f1335548b059a3f328c51f1324ae1cdd86ed8a37058a035475e7ea98008add0
Task id
fc-379fc029-variants-general-ef96efe7bd-formalized-v1
Task commitment
sha256:101a6de235338282b69d19ffdbfe51f22e8b330bfd416a5e2a2535e2b015f54b

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.