The story of Erdős problem #1026

Erdős problem #1026 was recently solved through a collaborative effort combining human mathematicians, AI tools, and existing literature. The problem involved finding optimal bounds for weighted monotone subsequences in sequences of real numbers. The solution emerged through multiple contributions: initial problem formulation and small-case calculations by researchers, autonomous proof generation by the Aristotle AI tool in Lean, discovery of a simpler "blow-up" argument, numerical optimization using AlphaEvolve to conjecture exact formulas, and AI-assisted literature searches that connected the problem to recent square-packing results. The final proof established that the optimal bound follows a specific piecewise linear pattern approximating the square root function, building on work by Baek-Koizumi-Ueoro and Praton.