Skip to content

Erdős problem 90

Conjectured upper bound on how many pairs among nn points in the plane can be exactly one unit apart.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/90.lean

Formal Conjectures

FormalConjectures/ErdosProblems/90.leanErdos90.erdos_904 linesExact file
False ↔  ∃ O,    ∃ (_ : O =O[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)),      (fun n => ↑(Erdos90.maxUnitDistances n)) =ᶠ[Filter.atTop] fun n => ↑n ^ (1 + O n)
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:90

Reported activity

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

  • AI standalone

    Erdős AI contributions wiki · 26 May, 2026

    Machine
    Claude Mythos
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 21 May-9 Jun, 2026

    Machine
    GPT-5.5 Pro
    People
    Ingo Althöfer, Michael Emmerich, Paata Ivanisvili, Tomasz Kania, leloy, mlewko, Eric Naslund, norxornor, Will Sawin, Carl Schildkraut, spiderduckpig, Tseng
    Open the source record

  • Formalization

    Erdős AI contributions wiki · 28 May-12 Jun, 2026

    Machine
    Aleph Prover
    Open the source record

  • AI standalone

    Erdős AI contributions wiki · 20 May, 2026

    Machine
    OpenAI internal model
    Open the source record

  • construction

    VibeMathed

    Machine
    OpenAI frontier model (specific version not disclosed)
    People
    Noga Alon, Thomas Bloom, Timothy Gowers, Daniel Litt, Will Sawin, Jacob Tsimerman, Melanie Matchett Wood
    Reported outcome
    resolved
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page