This chapter centers on a recent project announcement concerning the Lean proof assistant, reflecting on the speaker's journey through their master's and PhD studies. It discusses the complexities of Lean's type theory, the development of the 'Lean for Lean' project, and comparison with other frameworks like MetaCoq. Additionally, it highlights challenges faced in type checking, definitional equality, and the handling of inductive types within different type theories.