Siamo entusiasti di annunciare una prova Lean di ~25K righe del Teorema dei Numeri Primi (PNT) in forma forte! Questo completa una sfida lanciata da Terry Tao e @AlexKontorovich a gennaio 2024.