Recent advances in artificial intelligence are rapidly changing how mathematics is done. Systems can now generate conjectures, proof sketches, and even complete arguments at a scale and speed that was not possible before. This shift challenges a long-standing assumption: that the main difficulty in mathematics lies in finding proofs. Instead, as proof generation becomes easier, verification becomes the central bottleneck. How can we trust results produced by increasingly powerful AI systems?

In this talk, I will argue that formal verification provides a natural answer to this challenge, by representing proofs in a fully machine-checkable form where every logical step is explicitly justified. I will introduce Lean 4, a modern proof assistant based on dependent type theory, and explain how it treats propositions as types and proofs as programs, allowing verification to reduce to type checking. I will highlight recent developments showing that formalization is becoming significantly faster, and that it is starting to reach the level of mainstream research mathematics. Finally, I will briefly discuss an early-stage initiative to build a formalization library for computational economics, with the goal of bringing game theory, mechanism design, and social choice into a machine-verifiable framework.