AI proof-search agent resolves nine open Erdős problems, verified in Lean