The article discusses the importance of formalizing mathematics through the use of proof assistants like Lean, highlighting benefits beyond just error detection. It draws a parallel to TypeScript, emphasizing how formalization can enhance mathematical tools, facilitate analysis of mathematical trends, and improve collaboration through better documentation and version control. The author expresses a personal passion for engaging with mathematics and computer science through this formalization process.