Erdős problem 459

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

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

459.lean

Retained formal statement2 of 2

The upper bound $f u ≤ u ^ 2$ is attained exactly when u is prime: $f p = p ^ 2$ .

FormalConjectures/ErdosProblems/459.leanErdos459.erdos_459.variants.upper_tight1 lineExact file

1∀ {p : ℕ}, Nat.Prime p → Erdos459.f p = p ^ 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.