The story of Erdős problem #1026

Problem 1026 on the Erdős problem web site recently got solved through an interesting combination of existing literature, online collaboration, and AI tools. The purpose of this blog post is to try to tell the story of this collaboration, and also to supply a complete proof.

The original problem of Erdős, posed in 1975, is rather ambiguous. Erdős starts by recalling his famous theorem with Szekeres that says that given a sequence of ${k^2+1}$ distinct real numbers, one can find a subsequence of length ${k+1}$ which is either increasing or decreasing; one cannot improve the ${k^2+1}$ to ${k^2}$ , by considering for instance a sequence of ${k}$ blocks of length ${k}$ , with the numbers in each block decreasing, but the blocks themselves increasing. He also noted a result of Hanani that every sequence of length ${k(k+3)/2}$ can be decomposed into the union of ${k}$ monotone sequences. He then wrote “As far as I know the following question is not yet settled. Let ${x_1,\dots,x_n}$ be a sequence of distinct numbers, determine

$\displaystyle S(x_1,\dots,x_n) = \max \sum_r x_{i_r}$

where the maximum is to be taken over all monotonic sequences ${x_{i_1},\dots,x_{i_m}}$ “.

This problem was added to the Erdős problem site on September 12, 2025, with a note that the problem was rather ambiguous. For any fixed ${n}$ , this is an explicit piecewise linear function of the variables ${x_1,\dots,x_n}$ that could be computed by a simple brute force algorithm, but Erdős was presumably seeking optimal bounds for this quantity under some natural constraint on the ${x_i}$ . The day the problem was posted, Desmond Weisenberg proposed studying the quantity ${c(n)}$ , defined as the largest constant such that

$\displaystyle S(x_1,\dots,x_n) \geq c(n) \sum_{i=1}^n x_i$

for all choices of (distinct) real numbers ${x_1,\dots,x_n}$ . Desmond noted that for this formulation one could assume without loss of generality that the ${x_i}$ were positive, since deleting negative or vanishing ${x_i}$ does not decrease the left-hand side and does not increase the right-hand side. By a limiting argument one could also allow collisions between the ${x_i}$ , so long as one interpreted monotonicity in the weak sense.

Though not stated on the web site, one can formulate this problem in game theoretic terms. Suppose that Alice has a stack of ${N}$ coins for some large ${N}$ . She divides the coins into ${n}$ piles of consisting of ${x_1,\dots,x_n}$ coins each, so that ${\sum_{i=1}^n x_i = N}$ . She then passes the piles to Bob, who is allowed to select a monotone subsequence of the piles (in the weak sense) and keep all the coins in those piles. What is the largest fraction ${c(n)}$ of the coins that Bob can guarantee to keep, regardless of how Alice divides up the coins? (One can work with either a discrete version of this problem where the ${x_i}$ are integers, or a continuous one where the coins can be split fractionally, but in the limit ${N \rightarrow \infty}$ the problems can easily be seen to be equivalent.)

For small ${n}$ , one can work this out by hand. For ${n=1}$ , clearly ${c(1)=1}$ : Alice has to put all the coins into one pile, which Bob simply takes. Similarly ${c(2)=1}$ : regardless of how Alice divides the coins into two piles, the piles will either be increasing or decreasing, so in either case Bob can take both. The first interesting case is ${n=3}$ . Bob can again always take the two largest piles, guaranteeing himself ${2/3}$ of the coins. On the other hand, if Alice almost divides the coins evenly, for instance into piles ${((1/3 + \varepsilon)N, (1/3-2\varepsilon) N, N/3 + \varepsilon)}$ for some small ${\varepsilon>0}$ , then Bob cannot take all three piles as they are non-monotone, and so can only take two of them, allowing Alice to limit the payout fraction to be arbitrarily close to ${2/3}$ . So we conclude that ${c(3)=2/3}$ .

An hour after Desmond’s comment, Stijn Cambie noted (though not in the language I used above) that a similar construction to the one above, in which Alice divides the coins into ${k^2}$ pairs that are almost even, in such a way that the longest monotone sequence is of length ${k}$ , gives the upper bound ${c(k^2) \leq 1/k}$ . It is also easy to see that ${c(n)}$ is a non-increasing function of ${n}$ , so this gives a general bound ${c(n) \leq (1+o(1))/\sqrt{n}}$ . Less than an hour after that, Wouter van Doorn noted that the Hanani result mentioned above gives the lower bound ${c(n) \geq (\frac{1}{\sqrt{2}}-o(1))/\sqrt{n}}$ , and posed the problem of determining the asymptotic limit of ${\sqrt{n} c(n)}$ as ${n \rightarrow \infty}$ , given that this was now known to range between ${1/\sqrt{2}-o(1)}$ and ${1+o(1)}$ . This version was accepted by Thomas Bloom, the moderator of the Erdős problem site, as a valid interpretation of the original problem.

The next day, Stijn computed the first few values of ${c(n)}$ exactly:

$\displaystyle 1, 1, 2/3, 1/2, 1/2, 3/7, 2/5, 3/8, 1/3.$

While the general pattern was not yet clear, this was enough for Stijn to conjecture that ${c(k^2)=1/k}$ , which would also impliy that ${\sqrt{n} c(n) \rightarrow 1}$ as ${n \rightarrow \infty}$ . Stijn also described the extremizing sequences for this range of ${n}$ , but did not continue the calculation further (a naive computation would take runtime exponential in ${n}$ , due to the large number of possible subsequences to consider).

The problem then lay dormant for almost two months, until December 7, 2025, in which Boris Alexeev, as part of a systematic sweep of the Erdős problems using the AI tool Aristotle, was able to get this tool to autonomously solve this conjecture ${c(k^2)=1/k}$ in the proof assistant language Lean. The proof converted the problem to a rectangle-packing problem.

This was one further addition to a recent sequence of examples where an Erdős problem had been automatically solved in one fashion or another by an AI tool. Like the previous cases, the proof was not particularly novel. Within an hour, Koishi Chan gave an alternate proof deriving the required bound ${c(k^2) \geq 1/k}$ from the original Erdős-Szekeres theorem by a standard “blow-up” argument which we can give here in the Alice-Bob formulation. Take a large ${M}$ , and replace each pile of ${x_i}$ coins with ${(1+o(1)) M^2 x_i^2}$ new piles, each of size ${(1+o(1)) x_i}$ , chosen so that the longest monotone subsequence in this collection is ${(1+o(1)) M x_i}$ . Among all the new piles, the longest monotone subsequence has length ${(1+o(1)) M S(x_1,\dots,x_n)}$ . Applying Erdős-Szekeres, one concludes the bound

$\displaystyle M S(x_1,\dots,x_n) \geq (1-o(1)) (\sum_{i=1}{k^2} M^2 x_i^2){1/2}$

and on canceling the ${M}$ ‘s, sending ${M \rightarrow \infty}$ , and applying Cauchy-Schwarz, one obtains ${c(k^2) \geq 1/k}$ (in fact the argument gives ${c(n) \geq 1/\sqrt{n}}$ for all ${n}$ ).

Once this proof was found, it was natural to try to see if it had already appeared in the literature. AI deep research tools have successfully located such prior literature in the past, but in this case they did not succeed, and a more “old-fashioned” Google Scholar job turned up some relevant references: a 2016 paper by Tidor, Wang and Yang contained this precise result, citing an earlier paper of Wagner as inspiration for applying “blowup” to the Erdős-Szekeres theorem.

But the story does not end there! Upon reading the above story the next day, I realized that the problem of estimating ${c(n)}$ was a suitable task for AlphaEvolve, which I have used recently as mentioned in this previous post. Specifically, one could task to obtain upper bounds on ${c(n)}$ by directing it to produce real numbers (or integers) ${x_1,\dots,x_n}$ summing up to a fixed sum (I chose ${10^6}$ ) with a small a value of ${S(x_1,\dots,x_n)}$ as possible. After an hour of run time, AlphaEvolve produced the following upper bounds on ${c(n)}$ for ${1 \leq n \leq 16}$ , with some intriguingly structured potential extremizing solutions:

The scores, divided by ${10^6}$ were pretty obviously trying to approximate rational numbers. There were a variety of ways (including modern AI) to extract the actual rational numbers they were close to, but I searched for a dedicated tool and found this useful little web page of John Cook that did the job:

$\displaystyle 1, 1, 2/3, 1/2, 1/2, 3/7, 2/5, 3/8, 1/3, 1/3, 4/13, 3/10, 4/14, 3/11, 4/15, 1/4.$

I could not immediately see the pattern here, but after some trial and error in which I tried to align numerators and denominators, I eventually organized this sequence into a more suggestive form:

$\displaystyle 1$

$\displaystyle 1/1, 2/3, 1/2$

$\displaystyle 2/4, 3/7, 2/5, 3/8, 2/6$

$\displaystyle 3/9, 4/13, 3/10, 4/14, 3/11, 4/15, 3/12.$

which suggested a somewhat complicated but predictable conjecture for the values of the sequence ${c(n)}$ . On posting this, Boris found a clean formulation of the conjecture, namely that

$\displaystyle c(k^2 + 2a + 1) = \frac{k}{k^2+a} \ \ \ \ \ (1)$

whenever ${k \geq 1}$ and ${-k \leq a \leq k}$ . After a bit of effort, he also produced an explicit upper bound construction:

Proposition 1 If ${k \geq 1}$ and ${-k \leq a \leq k}$ , then ${c(k^2+2a+1) \leq \frac{k}{k^2+a}}$ .

Proof: Consider a sequence ${x_1,\dots,x_{k^2+2a+1}}$ of numbers clustered around the “red number” ${|a|}$ and “blue number” ${|a+1|}$ , consisting of ${|a|}$ blocks of ${k-|a|}$ “blue” numbers, followed by ${|a+1|}$ blocks of ${|a+1|}$ “red” numbers, and then ${k-|a|}$ further blocks of ${k}$ “blue” numbers, where all blocks are slightly increasing within each block, but the blue blocks are decreasing between each other, and the red blocks are decreasing between each other. The total number of elements is indeed

$\displaystyle |a| \times (k-|a|) + |a+1| \times |a+1| + (k-|a|) \times k = k^2 + 2a + 1$

and the total sum is close to

$\displaystyle |a| \times (k-|a|) \times |a+1| + |a+1| \times |a+1| \times |a| + (k-|a|) \times k \times |a+1| = (k^2 + a) |a+1|.$

With this setup, one can check that any monotone sequence consists either of at most ${|a+1|}$ red elements and at most ${k-|a|}$ blue elements, or no red elements and at most ${k}$ blue element, in either case giving a monotone sum that is bounded by either

$\displaystyle |a+1| \times |a| + (k-|a|) \times |a+1| = k |a+1|$

$\displaystyle 0 + k \times |a+1| = k |a+1|,$

giving the claim. $\Box$

Shortly afterwards, Lawrence Wu clarified the connection between this problem and a square packing problem, which was also due to Erdős (Problem 16). Let ${f(n)}$ be the least number such that, whenever one packs ${n}$ squares of sidelength ${d_1,\dots,d_n}$ into a square of sidelength ${D}$ , with all sides parallel to the coordinate axes, one has

$\displaystyle \sum_{i=1}^n d_i \leq f(n) D.$

Proposition 2 For any ${n}$ , one has

$\displaystyle c(n) \geq \frac{1}{f(n)}.$

Proof: Given ${x_1,\dots,x_n}$ and ${1 \leq i \leq n}$ , let ${S_i}$ be the maximal sum over all increasing subsequences ending in ${x_i}$ , and ${T_i}$ be the maximal sum over all decreasing subsequences ending in ${x_i}$ . For ${i < j}$ , we have either ${S_j \geq S_i + x_j}$ (if ${x_j \geq x_i}$ ) or ${T_j \geq T_i + x_j}$ (if ${x_j \leq x_i}$ ). In particular, the squares ${(S_i-x_i, T_i-x_i)}$ and ${(S_j-x_j, T_j-x_j)}$ are disjoint. These squares pack into the square ${[0, S(x_1,\dots,x_n)]^2}$ , so by definition of ${f}$ , we have

$\displaystyle \sum_{i=1}^n x_i \leq f(n) S(x_1,\dots,x_n),$

and the claim follows. $\Box$

This idea of using packing to prove Erdős-Szekeres type results goes back to a 1959 paper of Seidenberg.

At this point, Lawrence performed another AI deep research search, this time successfully locating a paper from just last year by Baek, Koizumi, and Ueoro, where they show that

Theorem 3 For any ${k \geq 1}$ , one has

$\displaystyle f(k^2+1) \leq k$

which, when combined with a previous argument of Praton, implies

Theorem 4 For any ${k \geq 1}$ and ${c \in {\bf Z}}$ with ${k^2+2c+1 \geq 1}$ , one has

$\displaystyle f(k^2+2c+1) \leq k + \frac{c}{k}.$

This proves the conjecture!

There just remained the issue of putting everything together. I did feed all of the above information into a large language model, which was able to produce a coherent proof of (1) assuming the results of Baek-Koizumi-Ueoro and Praton. Of course, LLM outputs are prone to hallucination, so it would be preferable to formalize that argument in Lean, but this looks quite doable with current tools, and I expect this to be accomplished shortly. But I was also able to reproduce the arguments of Baek-Koizumi-Ueoro and Praton, which I include below for completeness.

Proof: (Proof of Theorem 3) We can normalize ${D=k}$ . It then suffices to show that if we pack the length ${k}$ torus ${({\bf Z}/k{\bf Z})^2}$ by ${k+1}$ axis-parallel squares of sidelength ${d_1,\dots,d_n}$ , then

$\displaystyle \sum_{i=1}^{k^2+1} d_i \leq k^2.$

Pick ${x_0, y_0 \in {\bf R}/k{\bf Z}}$ . Then we have a ${k \times k}$ grid

$\displaystyle (x_0 + {\bf Z}) \times (y_0 + {\bf Z}) \pmod k{\bf Z}^2$

inside the torus. The ${i^{th}}$ square, when restricted to this grid, becomes a discrete rectangle ${A_{i,x_0} \times B_{i,y_0}}$ for some finite sets ${A_{i,x_0}, B_{i,y_0}}$ with

$\displaystyle |# A_{i,x_0} -# B_{i,y_0}| \leq 1. \ \ \ \ \ (2)$

By the packing condition, we have

$\displaystyle \sum_{i=1}^{k^2+1} # A_{i,x_0} # B_{i,y_0} \leq k^2.$

From (2) we have

$\displaystyle (# A_{i,x_0} - 1) (# B_{i,y_0} - 1) \geq 0$

hence

$\displaystyle # A_{i,x_0} # B_{i,y_0} \geq # A_{i,x_0} + # B_{i,y_0} - 1.$

Inserting this bound and rearranging, we conclude that

$\displaystyle \sum_{i=1}{k^2+1} # A_{i,x_0} + \sum_{i=1}{k^2+1} # B_{i,y_0} \leq 2k^2 + 1.$

Taking the supremum over ${x_0,y_0}$ we conclude that

$\displaystyle \sup_{x_0} \sum_{i=1}{k^2+1} # A_{i,x_0} + \sup_{y_0} \sum_{i=1}{k^2+1} # B_{i,y_0} \leq 2k^2 + 1$

so by the pigeonhole principle one of the summands is at most ${k^2}$ . Let’s say it is the former, thus

$\displaystyle \sup_{x_0} \sum_{i=1}^{k^2+1} # A_{i,x_0} \leq k^2.$

In particular, the average value of ${\sum_{i=1}^{k^2+1} # A_{i,x_0}}$ is at most ${k^2}$ . But this can be computed to be ${\sum_{i=1}^{k^2+1} d_i}$ , giving the claim. Similarly if it is the other sum. $\Box$

Proof: (Proof of Theorem 4) We write ${c = \epsilon |c|}$ with ${\epsilon = \pm 1}$ . We can rescale so that the square one is packing into is ${[0,k]^2}$ . Thus, we pack ${k^2+2\varepsilon |c|+1}$ squares of sidelength ${d_1,\dots,d_{k^2+2\varepsilon |c|+1}}$ into ${[0,k]^2}$ , and our task is to show that

$\displaystyle \sum_{i=1}^{k^2+2\varepsilon|c|+1} d_i \leq k^2 + \varepsilon |c|.$

We pick a large natural number ${N}$ (in particular, larger than ${k}$ ), and consider the three nested squares

$\displaystyle [0,k]^2 \subset [0,N]^2 \subset [0,N + |c| \frac{N}{N-\varepsilon}]^2.$

We can pack ${[0,N]^2 \backslash [0,k]^2}$ by ${N^2-k^2}$ unit squares. We can similarly pack

$\displaystyle [0,N + |c| \frac{N}{N-\varepsilon}]^2 \backslash [0,N]^2$

$\displaystyle [0, \frac{N}{N-\varepsilon} (N+|c|-\varepsilon)]^2 \backslash [0, \frac{N}{N-\varepsilon} (N-\varepsilon)]^2$

into ${(N+|c|-\varepsilon)^2 - (N-\varepsilon)^2}$ squares of sidelength ${\frac{N}{N-\varepsilon}}$ . All in all, this produces

$\displaystyle k^2+2\varepsilon |c|+1 + N^2-k^2 + (N+|c|-\varepsilon)^2 - (N-\varepsilon)^2 = (N+|c|)^2 + 1$

squares, of total length

$\displaystyle (\sum_{i=1}^{k^2+2\varepsilon |c|+1} d_i) +(N^2-k^2) + ((N+|c|-\varepsilon)^2 - (N-\varepsilon)^2) \frac{N}{N-\varepsilon}.$

Applying Theorem 3, we conclude that

$\displaystyle (\sum_{i=1}^{k^2+2\varepsilon |c|+1} d_i) +(N^2-k^2)$

$\displaystyle + ((N+|c|-\varepsilon)^2 - (N-\varepsilon)^2) \frac{N}{N-\varepsilon} \leq (N+|c|) (N + |c| \frac{N}{N-\varepsilon}).$

The right-hand side is

$\displaystyle N^2 + 2|c| N + |c|^2 + \varepsilon |c| + O(1/N)$

and the left-hand side similarly evaluates to

$\displaystyle (\sum_{i=1}^{k^2+2c+1} d_i) + N^2 -k^2 + 2|c| N + |c|^2 + O(1/N)$

and so we simplify to

$\displaystyle \sum_{i=1}^{k^2+2\varepsilon |c|+1} d_i \leq k^2 + \varepsilon |c| + O(1/N).$

Sending ${N \rightarrow \infty}$ , we obtain the claim. $\Box$

Similar Posts