HN Reader

I have no comments about the result itself, but the process and the AI policy which facilitated it is inspiring and easily transferable to any moderately complicated software engineering problem. Much to learn regardless of the maths.

This case study reveals the future of AI-assisted[1] work, far beyond mathematics.

It relies on a combination of Humans, LLMs ('General Tools'), Domain-Specific Tools, and Deep Research.

It is apparent that the static data encoded within an LLM is not enough; one must re-fetch sources and digest them fresh for the context of the conversation.

In this workflow, AlphaEvolve, Aristotle, and LEAN are the 'PhDs' on the team, while the LLM is the Full Stack Developer that glues them all together.

[1] If one likes pompous terms, this is what 'AGI' will actually look like.

> 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

{-2, 1, -1, 1/2, -1/2, 1/3, -1/3, 1/4, … -1/(k/2)} is a sequence of {k^2+1} distinct real numbers, but the longest increasing or decreasing subsequences are of length 2, not k+1.

What am I missing?

> 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.

Is this an example of the 4 minute mile phenomenon or did the AI proof provide key insights that Chan was able to use in their proof?