Erdős problem 1026

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

No current result

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

FormalConjectures/ErdosProblems/1026.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1026.leanErdos1026.erdos_10261 lineExact file

1IsGreatest Erdos1026.admissibleConstants sorry

SolvedStatement only, no proof

Reported by these sources. 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