AI finds simpler proof of decades-old math open problem

Scott Armstrong@scottnarmstrong

Astra found a short proof that the variance of the passage time in first-passage percolation scales sublinearly in the distance (by a strict power, exponent 1-\epsilon).

This was an open problem for many years (decades) and mentioned by Kesten in 1993.

Recently it was proved by Basu-Sidoravicius-Sly (2023) in two dimensions in a rotationally invariance continuum FPP model. Their proof is about 200 pages in total, and @ahmedbourabee1 and I decided to lean formalize it to understand it better. Some of their arguments turned out to be not ready for formalization (or at least we couldn't formalize them) and so we launched some agents to try to find workarounds.

Eventually, after a lot of interaction with the agents, this led to the discovery of a new mechanism which makes the induction in the scales argument work - giving us a different and dramatically simpler argument - which is valid in every dimension as well as on the lattice (under some curvature and regularity assumptions on the limiting shape).

We think this is an instance of "AIs giving us new and better understanding of a previously proved theorem" and of human-AI interaction (as we tested, this is not N-shottable by Astra for small N).