Erdős problem 459 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

459.lean

Retained formal statement1 of 2

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

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

FormalConjectures/ErdosProblems/459.leanErdos459.erdos_4591 lineExact file

1∀ {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.

Sources

Search problems.science