I will discuss the current progress of formalizing de Rham cohomology in Lean. As this is an ongoing project, I will cover the milestones achieved, the objectives currently within reach, and the specific challenges we have encountered.