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))\cdot(1/\sqrt{n})$ times the total sum. Resolved as $c = 1$ .

Result: Proved
Status: Resolved
AI contribution: AI co-developed
Method: Argument
Field: Combinatorics
Posed by: Paul Erdős
Year posed: 1975
Years open: 50y
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: Lean-verified
Publication: Announced
Significance: 10 / 100
Disclosed cost: —
Wikipedia: 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.

Source

AnnouncementTerence Tao's blog

Erdős Problem #1026: Monotonic Subsequence Sums

What the AI did

Verification

Source

Discussion