Generative AI is rapidly transforming the landscape of mathematical research by solving many open mathematical problems. I will talk about these advances from the perspective of formalized mathematics. Many of these AI solutions come with an AI-generated formalization in Lean. These might not help to understand the mathematical argument, but do provide some guarantees about the correctness of the proof. I will discuss to what extent we can trust Lean formalizations and what there is left to check and my perspectives on autoformalization.