A new #Lean formalization project led by Alex Kontorovich and myself has just been announced to formalize the proof of the prime number theorem, as well as much of the attendant supporting machinery in complex analysis and analytic number theory, with the plan to then go onward and establish further results such as the Chebotarev density theorem. The repository for the project (including the blueprint) is at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd , and discussion will take place at this Zulip stream: https://leanprover.zulipchat.com/#narrow/stream/423402-PrimeNumberTheorem.2B
