From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
The paper critiques current AI for Mathematics (AI4Math) systems that solve isolated problems like competitions. It argues these systems must evolve into research agents capable of discovering new theorems in complex, open mathematical fields by building knowledge graphs and collaborating with humans.