SOLVED LEANdatabase updated 2025-12-12
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The set of sums \(\sum x_{i_r}\), where \(x_{i_1},\ldots,x_{i_r}\) ranges over the monotonic subsequences of the sequence \(x_1,\ldots,x_n\).
The set of constants \(c\) such that, for all sequences of \(n\) distinct positive real numbers \(x_1,\ldots,x_n\), \[ \max\left(\sum x_{i_r}\right) > (c-o(1))\frac{1}{\sqrt{n}}\sum x_i \] (where the maximum is taken over all monotonic subsequences). The source reduces to positive sequences. With signed sequences the condition is not a vanishing error term: for \(\varepsilon > |c|\) and \(x_i = -i\) the right-hand side is positive while every subsequence sum is nonpositive, so no constant would be admissi
Let \(x_1,\ldots,x_n\) be a sequence of distinct real numbers. Determine \[ \max\left(\sum x_{i_r}\right), \] where the maximum is taken over all monotonic subsequences. This is as Erdős posed the problem in [Er71], which is rather ambiguous. Discussion between several users in the comments section has led to the following precise possible question, as posed by van Doorn: What is the largest constant \(c\) such that, for all sequences of \(n\) real numbers \(x_1,\ldots,x_n\), \[ \max\left(\sum x_{i_r}\right) > (c-o(1))\frac{1}{\sqrt{n}}\sum x_i \] (where again the maximum is taken over all monotonic subsequences)? Cambie makes the stronger conjecture that if \(x_1,\ldots,x_{k^2}\) are distinct positive real numbers with \(\sum x_i=1\) then there is always a monotonic subsequence with sum at least \(1/k\). This stronger conjecture appears to have been first proved by Tidor, Wang, and Yang [TWY16], and is also implicit in work of Wagner [Wa17]. A proof was given and formalised by Aristotle (see the comments), with an alternative proof provided by Chan. In particular, this shows that \(c=1\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/1026.
NOBODY HAS SENT US AN ATTEMPT YET
If you take a run at this one — with your own AI subscription or without — the guide says how,
and the submission form gets you an honest read of what you found.