This chapter chronicles the speaker's career transition and academic journey, highlighting the pivotal proof workshop in 2017 that initiated the development of MathLib for the Lean proof assistant. It emphasizes the collaborative nature of the project, detailing the transition from Lean 3 to Lean 4 and the significant effort required for code porting. Additionally, the chapter discusses the importance of maintaining code quality and readability while navigating the complexities of formal proofs and mathematical translations across different systems.