Skip to content

Erdős problem 1026

For a sequence of nn distinct reals, determine the largest constant cc such that some monotonic subsequence always has sum exceeding (c−o(1))⋅(1/n)(c-o(1))\cdot(1/\sqrt{n}) times the total sum. Resolved as c=1c = 1.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1026.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1026.leanErdos1026.erdos_10261 lineExact file
IsGreatest Erdos1026.admissibleConstants sorry
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1026
  • PLBY Lean proofsErdosProblems.Erdos1026

Reported activity

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

  • AI alongside literature

    Erdős AI contributions wiki · 7 Dec, 2025

    Machine
    Aristotle
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 8 Dec, 2025

    Machine
    AlphaEvolve, Aristotle, Gemini, GPT
    People
    Boris Alexeev, Stijn Cambie, Terence Tao, Lawrence Wu
    Open the source record

  • argument

    VibeMathed

    Machine
    Aristotle, with GPT, Gemini and AlphaEvolve also contributing
    People
    Boris Alexeev, Stijn Cambie, Terence Tao, Lawrence Wu
    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