Formalizing mathematics involves translating mathematical statements from natural language into a precise formal language that computers can understand. As modern mathematics becomes deeper and more complex, the importance of formalization has grown significantly. In this talk, I will introduce the concept of formalization, explore its significance, and highlight current successful and ongoing projects in the field.