Animado para anunciar uma prova Lean de ~ 25K linhas do Teorema dos Números Primos (PNT) em forma forte! Isso completa um desafio definido por Terry Tao e @AlexKontorovich em janeiro de 2024.