Skip to content

Erdős problem 459

Start work

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).

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/459.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:459
  • PLBY Lean proofsErdosProblems.Erdos459

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry