Skip to content

Erdős problem 400

Start work

Erdős and Graham write that it is easy to show that gk(n)≪klog⁡ng_k(n) \ll_k \log n always, but the best possible constant is unknown.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/400.lean

Formal Conjectures

FormalConjectures/ErdosProblems/400.leanErdos400.erdos_400.parts.i5 linesExact file
True ↔  ∀ k ≥ 2,    ∃ c,      Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x =>        c * ↑x * Real.log ↑x
OpenStatement only, no proof

Reported activity

Reported by these sources. Not reviewed here.

  • AI collaborating with humans

    Erdős AI contributions wiki · 22 Jun, 2026

    Machine
    GPT
    People
    Eric Li
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry