We can’t predict what will happen in AI for math, but we can prepare. Assuming steady progress in capabilities, we could soon see AI that can autoformalize entire mathematical arguments or papers, and AI which can solve previously open mathematical problems. How do we prepare, including recording and benchmark such capabilities? In this talk I will outline my thoughts on why autoformalization is more relevant than ever and propose two specific ways can measure progress. One is a benchmark of easy-to-check autoformalizations of proofs. The other is a public repository of formalized open problems.