Skip to content

Erdős problem 459

Let f(u)f(u) be the largest vv such that no m∈(u,v)m\in (u,v) is composed entirely of primes dividing uvuv. Estimate f(u)f(u).

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

459.lean

Retained formal statement1 of 2

Let f(u)f(u) be the largest vv such that no m∈(u,v)m\in (u,v) is composed entirely of primes dividing uvuv. Estimate f(u)f(u).

The estimate u+2≤f(u)≤u2u + 2 \le f(u) \le u^2 holds for every u≥2u \ge 2. The upper bound is attained when uu is prime, and the lower bound when u=2k−2u = 2^k - 2 with k≥2k \ge 2; Cambie further showed that f(n)=(1+o(1))nf(n) = (1 + o(1))n for almost all nn.

FormalConjectures/ErdosProblems/459.leanErdos459.erdos_4591 lineExact file
∀ {u : ℕ}, 2 ≤ u → u + 2 ≤ Erdos459.f u ∧ Erdos459.f u ≤ u ^ 2
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.