The Science paper reports that AlphaProof Nexus autonomously resolved nine of 353 open Erdős problems, including two that had been open for 56 years. It also reports 44 proofs among 492 open conjectures from the Online Encyclopedia of Integer Sequences.
The mechanism is: An LLM proposes proof material, and Lean checks formal proof steps as part of an iterative search loop. The why_now is: the paper supplies evidence beyond contest-style demonstrations: it describes deployment against open research problems across several mathematical areas. The authors further report that a basic agent alternating generation and Lean verification replicated the Erdős successes. That makes the verifier part of the operating method, not a decorative audit after free-form generation.
The first implication is: research agents should be assessed through inspectable artifacts and verification procedures, not only claimed answers or benchmark scores. The evidence boundary is: the source reports results on selected problems and does not establish general autonomous mathematical competence. The first watch condition is: whether independent researchers can inspect, rerun, and extend the formal proof artifacts across the reported problem set. The result supports a useful direction for scientific agents, while leaving reproducibility and breadth as the next questions.