Erdős Problem #1026
4 days ago
- #Erdős problems
- #collaborative problem solving
- #AI in mathematics
- Problem 1026 on the Erdős problem website was recently solved through a combination of existing literature, online collaboration, and AI tools.
- The problem, posed by Erdős in 1975, involves determining the maximum sum over monotonic subsequences of a sequence of distinct real numbers.
- Desmond Weisenberg proposed studying the quantity f(n), defined as the largest constant such that the sum of any monotonic subsequence is at least f(n) times the total sum of the sequence.
- Stijn Cambie and Wouter van Doorn contributed upper and lower bounds for f(n), leading to the conjecture that f(n) = 2/(√n + 1).
- Boris Alexeev used the AI tool Aristotle to autonomously solve the conjecture in Lean, converting the problem to a rectangle-packing problem.
- Koishi Chan provided an alternate proof using the Erdős-Szekeres theorem, and subsequent literature searches found prior results by Tidor, Wang, and Yang.
- AlphaEvolve was used to generate upper bounds for f(n), revealing a pattern that matched the conjecture.
- Lawrence Wu connected the problem to a square packing problem (Erdős Problem 106), which was recently solved by Baek, Koizumi, and Ueoro.
- The final proof combined results from Baek-Koizumi-Ueoro and Praton, confirming the conjecture f(n) = 2/(√n + 1).
- The solution highlights the importance of diverse collaboration, including human intuition, literature, and AI tools.