Conjectures.io

Number theory

Erdős 126 - isLittleO

Erdős says that f(n)=o(nlog⁡n)f(n) = o(\frac{n}{\log n}) has never been proved.

References

No one has attempted this yet.

Formal statement

Lean type

∀ (f : ℕ → ℕ), Erdos126.IsMaximalAddFactorsCard f → (fun n => ↑(f n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

What you must prove

import FormalConjectures.ErdosProblems.«126»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos126.erdos_126.variants.isLittleO" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/126.lean

Source type SHA-256
sha256:e51da61bab02dff3343888e4508dfbd1cb0dcede06e43085d132d5f8a50b05e1
Task id
fc-379fc029-variants-islittleo-eed5ada43d-formalized-v1
Task commitment
sha256:6f5366a3f6c828b0f37f10cb4d58d48e70d6d544aea38a56eea26f156fbf548a

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.