Erdős Problem #1026 — Monotonic Subsequence Sums
Erdős problem #1026 · erdosproblems.com/1026
For a sequence of n distinct reals, determine the largest constant c such that some monotonic subsequence always has sum exceeding (c−o(1))·(1/√n)·(total sum). Resolved as c = 1.
- Result
- Proved
- Field
- Combinatorics
- Posed by
- Paul Erdős
- Year posed
- 1971
- Years open
- 54y
- Solved
- 2025-12-08
- Model
- Aristotle, with GPT, Gemini and AlphaEvolve also contributing
- Vendor
- Harmonic / OpenAI / Google DeepMind
- Collaborators
- Boris Alexeev, Stijn Cambie, Terence Tao, Lawrence Wu
- Verification
- Expert-verified
- Notability
- No dedicated article
What the AI did
Multiple AI systems contributed within an ordinary human mathematical collaboration rather than one model solving it outright; Aristotle produced and formally verified the winning proof in Lean, pinning down the sharp constant c = 1.
Verification
Formally verified in Lean. Documented firsthand by Terence Tao on his blog as a case study in AI-assisted collaboration, not an AI-alone result.