The project to formalize in Lean the classical Carleson theorem on almost everywhere convergence of Fourier series, and a modern generalization of that theorem to more general metric spaces, has announced a successful completion of its goals: https://leanprover.zulipchat.com/#narrow/channel/442935-Carleson/topic/Project.20Finish/with/529466749 .

It seems that the process, while lengthy, was relatively smooth; there were some technical issues (for instance, whether to work with norms that take values in the non-negative reals, or extended norms that take values in the extended non-negative reals), and some key definitions had to have their formalizations modified at some stage of the process to make certain lemmas formalize properly, but overall no major mathematical issues were uncovered.