Skip to content

Erdős problem 1095

Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that g(k)≥exp⁡(cklog⁡k)g(k)\geq\exp(c\frac{k}{\log k}) for some constant c>0c>0.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1095.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1095.leanErdos1095.erdos_1095.variants.log_equivalent1 lineExact file
Asymptotics.IsEquivalent Filter.atTop (fun k => Real.log ↑(Erdos1095.g k)) fun k => ↑k / Real.log ↑k
OpenStatement only, no proof

Proof manifests naming this Problem

  • PLBY Lean proofsErdosProblems.Erdos1095b

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI building on literature

    Erdős AI contributions wiki · 30 Dec, 2025

    Machine
    Aristotle
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 13 Mar, 2026

    Machine
    Claude Opus 4.6, Gemini 3.1 Pro, GPT-5.4 Pro
    People
    shtuka
    Open the source record

  • Formalization

    Erdős AI contributions wiki · 20 Jun, 2026

    Machine
    Aristotle
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page