Mathematicians Scott Armstrong and Ahmed Bourabee used the AI agent Astra to discover a simplified proof for a mathematical problem concerning how the variance of passage time in first-passage percolation scales sublinearly in the distance. The new argument identifies a mechanism that allows the proof to be valid in every dimension and on the lattice, provided certain regularity and curvature assumptions on the limiting shape are met.
The researchers were originally attempting to use the Lean formalization language to verify a 200 page proof published in 2023 by Basu, Sidoravicius, and Sly, which only applied to 2D models. The broader problem had remained open for decades since it was first mentioned by Harry Kesten in 1993. Armstrong stated that the simplified proof emerged from human-AI interaction after the agent was used to find workarounds for sections of the original proof that resisted formalization.