Speaking of Lean formalisation of analytic results, the PrimeNumberTheorem+ project has achieved an intermediate goal of a major version of the PNT (called 'Medium PNT' in the graph).

https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html

There are other versions at the edge of the dependency graph, with different types of asymptotics (eg the sum over Möbius function version), but this was a big milestone. 'Weak' PNT had the error term of \(o(x)\), but the Medium PNT has better error term \(O(x \exp (-c(\log x)^{1/10}))\). There was a 'Strong' PNT but it's noted as having been removed from the Blueprint document.