---

Claim. In the problem's precise Statement, $c=1$, and the least ratio is known exactly for every length. For a sequence $x$ of $n$ distinct positive reals let $M(x)$ be the largest sum of a monotone subsequence, and let $c(n)$ be the infimum of $M(x)/\sum_ix_i$ over all such sequences. Then

$$c(n)=\frac{k}{k^2+a}\qquad\text{for }n=k^2+2a+1,\ -k<a\le k,\ k\ge2,$$

every $n\ge3$ other than $n=4$ being written this way for exactly one such pair $(k,a)$. In particular $c(k^2)=1/k$: $k^2$ distinct positive reals summing to $1$ have a monotone subsequence of sum at least $1/k$, and this is sharp in the limit. Since $c(n)\sqrt n\to1$, the largest constant $c$ with $M(x)>(c-o(1))\,n^{-1/2}\sum_ix_i$ for all sequences is $1$, and the problem's assumption that the $x_i$ be distinct and positive loses nothing, as negative or zero terms can be dropped. The values agree with the exact ratios computed in the site's thread for $n\le9$, verified there to $n\le11$, and with the pattern Terence Tao found in the thread with the tool AlphaEvolve from examples for $n$ up to $16$.

Submission note. Posted to the site's forum by Boris Alexeev on 7 December 2025:

Aristotle from Harmonic proved a formalization of Stijn Cambie's 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$", which in my understanding is considered the main problem. In particular, this proves "$c=1$". Type-check it online!

The proof is cool! It's a partitioned-rectangle, weighted generalization of Erdős-Szekeres. It's morally the same as the blowup proof below, but more geometrically evocative (!).

Update: KoishiChan's blowup proof below appears in Section 3 of 1-color-avoiding paths, special tournaments, and incidence geometry (2016) by Jonathan Tidor, Victor Y. Wang, Ben Yang, where it is further referenced as implicit in Large subgraphs in rainbow-triangle free colorings by Adam Zsolt Wagner. LLMs did not succeed in finding these references; instead, they were found using Google Scholar, armed with the information of these proofs. The references also link back to a clear statement of Erdős's problem.

(The site has been updated to address this comment.)

Posted to the site's forum by Boris Alexeev on 12 December 2025:

The solution to this problem has been formalized in Lean. Type-check it online!

To be clear, this is for general $n$, not necessarily square. The result is that $c(n) = \frac{k}{k^2+a}$ if $n=k^2+2a+1$ for $-k < a \le k$.

Aristotle auto-formalized this proof. (I wrote the final statement.) Aristotle encountered significant difficulty with the proof, mostly with the explicit construction. There were multiple issues, including annoying limit/$\varepsilon$ issues, as well as the written proof being incorrect for negative $a$. Nonetheless, the proof was successfully completed entirely by Aristotle. The human proof was fixed (both by hand before Aristotle and also by Aristotle independently); hopefully the formal proof offers some more assurance that the result is airtight.

The resulting formal proof is terrible, partially as an artifact of stitching together many Aristotle runs. (For example, $c$ is defined three times, twice by Aristotle and once more by me.) It could definitely be cleaned up significantly. It takes my laptop over half an hour to verify.

(The site has been updated to address this comment.)

The proof. The lower bound $c(n)\ge k/(k^2+a)$ turns the sequence into a packing of axis-parallel squares, in the manner of Seidenberg's 1959 proof of the Erdős–Szekeres theorem: with $S_i$ and $T_i$ the largest sums of an increasing and of a decreasing subsequence ending at $x_i$, the squares $[S_i-x_i,S_i]\times[T_i-x_i,T_i]$ have pairwise disjoint interiors and lie in $[0,M(x)]^2$, so a bound on the total side length of $n$ axis-parallel squares packed in a unit square bounds $\sum x_i$ in terms of $M(x)$. That bound is the axis-parallel case of Erdős's square-packing problem, Problem 106, proved by Baek, Koizumi and Ueoro [BKU24] with an embedding argument of Praton; the Lean file proves the needed form itself (baek_koizumi_ueoro), so the claim rests on no other page of this corpus. The upper bound $c(n)\le k/(k^2+a)$ is Alexeev's construction of $n$ numbers clustered at two values, arranged in blocks so that every monotone subsequence takes few terms from each cluster; for $n=k^2$ it is the construction posted by Stijn Cambie in the thread in September 2025, which gave $c\le1$. The thread records the collaboration: Tao's numerical table and conjectured pattern, Alexeev's closed form and construction, Lawrence Wu's identification of the packing problem and of [BKU24], and Tao's blog post of 8 December 2025 with a complete informal proof.

Claimant. Boris Alexeev, who posted on the site's thread on 7 December 2025 a Lean proof of the $k^2$ statement and on 12 December 2025 the general theorem, both generated by the AI system Aristotle (Harmonic), as the posts and the file's header say; the header names Alexeev, Aristotle, Koishi Chan, Terence Tao, AlphaEvolve (Google DeepMind) and Lawrence Wu as the collaboration behind the solution, with the prior literature of Baek, Koizumi and Ueoro, Praton and Wagner. The $k^2$ statement had been proved in 2016 by Tidor, Wang and Yang (their claim page), as the thread found the next day; the exact value of $c(n)$ for every $n$ is new here.

Acceptance. Reviewed: Thomas Bloom, the site's curator, labels the problem SOLVED (LEAN), names Aristotle's Lean proof of the finite form and Chan's second proof in the remarks, and states the answer $c=1$; the curator is independent of the claimant. The site's remark, last edited on 8 December 2025, credits the $k^2$ statement and the answer $c=1$; the exact value of $c(n)$ for every $n$, posted on 12 December 2025, is later than the remark and rests on the Lean file and Tao's account alone. Not refereed: no manuscript beyond the thread posts, the Lean file and Tao's blog post exists. No formalized evidence: this corpus has not built the file.

Formalization. The Lean file among the links declares itself a formalization of a solution to Problem 1026, says that Aristotle generated all of its formal proofs, and names Lean 4.24.0 with the matching Mathlib. Its theorem exists_monotone_subseq_sum_ge is the $k^2$ statement, its theorem c_opt_eq_k_div_sq_add_a the exact value above for $n=k^2+1+2a$ with $k>1$ and $-k<a\le k$, for the infimum c_opt of the ratio over sequences of $n$ distinct positive reals, and its construction theorems give the matching upper bounds. The file contains no sorry and no axiom declaration and ends without an axiom print; Alexeev's post says the kernel check takes their laptop over half an hour and that the file, stitched from several Aristotle runs, defines $c$ three times. The link is pinned to the commit of 31 March 2026; the file was added on 7 December 2025 and received the general theorem on 12 December 2025. The formal-conjectures statement file for the problem, as of its commit of 18 September 2026, marks it solved and, on its weighted-variant statement, points at the same file of the same repository under a later toolchain folder (v4.29.1), unpinned; a statement file is not a formalization.