興奮地宣佈一個大約25K行的Lean形式的素數定理（PNT）強形式的證明！ 這完成了Terry Tao和@AlexKontorovich在2024年1月提出的挑戰。