Formalizing mathematics involves translating mathematical statements from natural language into a precise formal language that computers can interpret. As modern mathematics becomes deeper and more complex, the importance of formalization has grown significantly. In this talk, I will provide a brief introduction to the concept of formalization, discuss its significance, and explore how formalization and AI interact with each other.