Verification run

Run 59

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via github_backfill

succeeded commit f2f17085a61b toolchain lean-v4-30-0 prover lean took 58m 49s · finished 4w ago

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

ressed: 5087
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 61 KB/s], Decompressed: 5121
Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 81 KB/s], Decompressed: 5162
Downloaded: 5222 file(s) [attempted 5222/8459 = 61%, 56 KB/s], Decompressed: 5217
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 130 KB/s], Decompressed: 5255
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 395 KB/s], Decompressed: 5293
Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 252 KB/s], Decompressed: 5330
Downloaded: 5381 file(s) [attempted 5381/8459 = 63%, 325 KB/s], Decompressed: 5380
Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 96 KB/s], Decompressed: 5409
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 214 KB/s], Decompressed: 5453
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 1018 KB/s], Decompressed: 5481
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 39 KB/s], Decompressed: 5481
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 336 KB/s], Decompressed: 5484
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 296 KB/s], Decompressed: 5614
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 147 KB/s], Decompressed: 5659
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 638 KB/s], Decompressed: 5689
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 99 KB/s], Decompressed: 5734
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 112 KB/s], Decompressed: 5778
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 108 KB/s], Decompressed: 5816
Downloaded: 5863 file(s) [attempted 5863/8459 = 69%, 168 KB/s], Decompressed: 5854
Downloaded: 5899 file(s) [attempted 5899/8459 = 69%, 47 KB/s], Decompressed: 5895
Downloaded: 5937 file(s) [attempted 5937/8459 = 70%, 61 KB/s], Decompressed: 5932
Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 274 KB/s], Decompressed: 5974
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 102 KB/s], Decompressed: 6015
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 223 KB/s], Decompressed: 6056
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 59 KB/s], Decompressed: 6093
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 228 KB/s], Decompressed: 6128
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 44 KB/s], Decompressed: 6128
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 473 KB/s], Decompressed: 6131
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 942 KB/s], Decompressed: 6251
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 129 KB/s], Decompressed: 6288
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 50 KB/s], Decompressed: 6326
Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 181 KB/s], Decompressed: 6367
Downloaded: 6412 file(s) [attempted 6412/8459 = 75%, 44 KB/s], Decompressed: 6408
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 1294 KB/s], Decompressed: 6436
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 173 KB/s], Decompressed: 6483
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 57 KB/s], Decompressed: 6525
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 149 KB/s], Decompressed: 6566
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 616 KB/s], Decompressed: 6593
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 964 KB/s], Decompressed: 6593
Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 145 KB/s], Decompressed: 6596
Downloaded: 6728 file(s) [attempted 6728/8459 = 79%, 113 KB/s], Decompressed: 6596
Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 124 KB/s], Decompressed: 6596
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 43 KB/s], Decompressed: 6596
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 114 KB/s], Decompressed: 6596
Downloaded: 6887 file(s) [attempted 6887/8459 = 81%, 1967 KB/s], Decompressed: 6596
Downloaded: 6928 file(s) [attempted 6928/8459 = 81%, 253 KB/s], Decompressed: 6596
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 409 KB/s], Decompressed: 6679
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 428 KB/s], Decompressed: 6679
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 99 KB/s], Decompressed: 6679
Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 129 KB/s], Decompressed: 7086
Downloaded: 7134 file(s) [attempted 7134/8459 = 84%, 83 KB/s], Decompressed: 7130
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 292 KB/s], Decompressed: 7171
Downloaded: 7219 file(s) [attempted 7219/8459 = 85%, 193 KB/s], Decompressed: 7216
Downloaded: 7260 file(s) [attempted 7260/8459 = 85%, 1042 KB/s], Decompressed: 7257
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 45 KB/s], Decompressed: 7298
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 312 KB/s], Decompressed: 7336
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 60 KB/s], Decompressed: 7380
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 523 KB/s], Decompressed: 7408
Downloaded: 7460 file(s) [attempted 7460/8459 = 88%, 472 KB/s], Decompressed: 7455
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 170 KB/s], Decompressed: 7496
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 587 KB/s], Decompressed: 7534
Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 109 KB/s], Decompressed: 7575
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 1297 KB/s], Decompressed: 7620
Downloaded: 7661 file(s) [attempted 7661/8459 = 90%, 204 KB/s], Decompressed: 7657
Downloaded: 7697 file(s) [attempted 7697/8459 = 90%, 59 KB/s], Decompressed: 7692
Downloaded: 7735 file(s) [attempted 7735/8459 = 91%, 28 KB/s], Decompressed: 7729
Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 1476 KB/s], Decompressed: 7770
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 420 KB/s], Decompressed: 7811
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 303 KB/s], Decompressed: 7849
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 1222 KB/s], Decompressed: 7887
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 639 KB/s], Decompressed: 7928
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 200 KB/s], Decompressed: 7952
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 327 KB/s], Decompressed: 8006
Downloaded: 8047 file(s) [attempted 8047/8459 = 95%, 370 KB/s], Decompressed: 8041
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 346 KB/s], Decompressed: 8082
Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 875 KB/s], Decompressed: 8119
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 105 KB/s], Decompressed: 8160
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 384 KB/s], Decompressed: 8208
Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 540 KB/s], Decompressed: 8246
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 505 KB/s], Decompressed: 8287
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 1149 KB/s], Decompressed: 8328
Downloaded: 8376 file(s) [attempted 8376/8459 = 99%, 584 KB/s], Decompressed: 8373
Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 225 KB/s], Decompressed: 8417
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 516 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 516 KB/s], Decompressed: 8455


$ lake build
exit_code=Some(0) duration_ms=1150713
stdout:
✔ [3460/3468] Built PrimeNumberTheoremAnd.ZetaBounds (93s)
ℹ [3473/3481] Built PrimeNumberTheoremAnd.MediumPNT (31s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3496/3504] Built PrimeNumberTheoremAnd.StrongPNT (15s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3500/3505] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.8s)
✔ [3631/3641] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (8.9s)
⚠ [3634/3646] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3639/3646] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3703/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (45s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3705/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (3.0s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3707/3710] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.8s)
✔ [3809/3820] Built PrimeNumberTheoremAnd.IEANTN.LogTables (9.1s)
⚠ [3810/3820] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3813/3822] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.8s)
✔ [3815/3822] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.4s)
⚠ [3816/3823] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [3820/3824] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (11s)
✔ [3823/3827] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (9.1s)
⚠ [3945/3955] Built PrimeNumberTheoremAnd.IEANTN.Buthe (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [3947/3958] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (18s)
⚠ [3949/3958] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (6.2s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [3950/3958] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (97s)
⚠ [3951/3958] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (72s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3954/3963] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (38s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [3955/3963] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3956/3963] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [3960/3963] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (33s)
⚠ [3962/3968] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (58s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [3967/3975] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (62s)
✔ [3970/3982] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (3.4s)
⚠ [3971/3982] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [3972/3982] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (10s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2766:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2816:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2872:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2934:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2969:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2999:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3163:8: declaration uses `sorry`
✔ [3974/3982] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (16s)
⚠ [3976/3982] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (46s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [3979/3983] Built PrimeNumberTheoremAnd.IEANTN.Dusart (43s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [3982/3985] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (54s)
✔ [3999/4010] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (62s)
⚠ [4002/4021] Built PrimeNumberTheoremAnd.IEANTN.Mertens (15s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4003/4021] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (16s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
✔ [4004/4021] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (12s)
⚠ [4006/4021] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (6.7s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4007/4021] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4009/4021] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (3.3s)
⚠ [4014/4035] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (11s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4015/4035] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.8s)
✔ [4017/4035] Built PrimeNumberTheoremAnd.IEANTN.Lcm (28s)
⚠ [4019/4046] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (7.7s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4023/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (2.7s)
✔ [4026/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (2.7s)
ℹ [4030/4046] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (18s)
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4032/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.1s)
✔ [4033/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (2.1s)
✔ [4037/4046] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (2.3s)
✔ [4040/4046] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (56s)
✔ [4044/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (2.2s)
✔ [4045/4046] Built PrimeNumberTheoremAnd (3.8s)
Build completed successfully (4046 jobs).

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ lake build :blueprint
exit_code=Some(0) duration_ms=939294
stdout:
✔ [14/35] Built Batteries.Lean.NameMapAttribute:c.o (817ms)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (539ms)
✔ [33/35] Built Cli:c.o (86ms)
✔ [3492/3507] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (73s)
ℹ [3505/3511] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3507/3513] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (60s)
⚠ [3531/3547] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3536/3548] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3542/3552] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.9s)
⚠ [3681/3702] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3685/3702] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.5s)
⚠ [3691/3702] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3754/3764] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3756/3765] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (27s)
⚠ [3757/3765] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3759/3765] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.5s)
✔ [3762/3775] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.1s)
✔ [3865/3886] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (4.8s)
⚠ [3867/3886] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3870/3887] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.6s)
⚠ [3871/3887] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [3876/3889] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3877/3889] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.3s)
✔ [3886/3891] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (11s)
✔ [3888/3900] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.9s)
⚠ [4008/4023] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4012/4030] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.5s)
⚠ [4015/4032] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4016/4032] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (6.4s)
⚠ [4017/4032] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [4021/4033] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
⚠ [4022/4033] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
✔ [4023/4034] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (5.6s)
✔ [4025/4036] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (108s)
⚠ [4026/4036] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [4028/4036] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [4029/4036] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (60s)
⚠ [4033/4037] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [4034/4042] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (9.0s)
✔ [4035/4042] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (52s)
✔ [4044/4063] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.8s)
✔ [4045/4063] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.6s)
⚠ [4046/4063] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [4047/4064] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2766:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2816:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2872:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2934:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2969:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2999:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3163:8: declaration uses `sorry`
✔ [4049/4065] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (17s)
✔ [4051/4065] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.5s)
⚠ [4052/4065] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
⚠ [4054/4065] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4058/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (19s)
✔ [4059/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (21s)
✔ [4061/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4064/4069] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4084/4110] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4085/4110] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4088/4124] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
✔ [4089/4124] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4090/4124] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4091/4124] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (35s)
⚠ [4094/4124] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
⚠ [4102/4124] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
✔ [4103/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (16s)
⚠ [4104/4154] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4105/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (17s)
✔ [4107/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (30s)
✔ [4112/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.0s)
✔ [4121/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.8s)
✔ [4122/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4123/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (4.2s)
ℹ [4124/4169] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4141/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.6s)
✔ [4144/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.6s)
✔ [4149/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.1s)
✔ [4152/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.3s)
✔ [4153/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (2.2s)
✔ [4155/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.5s)
✔ [4158/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4165/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (2.3s)
✔ [4167/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (4.3s)
ℹ [4168/4170] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (81ms)
info: Blueprint indexing
Build completed successfully (4170 jobs).

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes


$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
exit_code=Some(0) duration_ms=987732
stdout:
apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":264,"diagnostic_count":80,"duration_ms":27531,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":264,"dependency_count":1080,"diagnostic_count":90,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":886790,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":264,"dependency_count":1080,"diagnostic_count":90,"duration_ms":252,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":2370291,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":16,"ok":true,"payload_bytes":2370291,"phase":"lean_json_write"}

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":7098}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":262,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":50005,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache f53cb0c960be59836d3b9e9d22459cdf3d4ed23e5a0511074cca895dbac7a473
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":929428,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 993 ms · created 6/16/2026, 11:35:03 PM

git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-499-source

Cloning into '/var/lib/apodeixis/repos/job-499-source'...

git_checkout exit 128 duration 4 ms · created 6/16/2026, 11:35:03 PM

git checkout f2f17085a61bb64b3a174339adbea59e9af85928

fatal: reference is not a tree: f2f17085a61bb64b3a174339adbea59e9af85928

git_checkout exit 0 duration 774 ms · created 6/16/2026, 11:35:03 PM

git fetch --depth 1 origin f2f17085a61bb64b3a174339adbea59e9af85928

From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
 * branch            f2f17085a61bb64b3a174339adbea59e9af85928 -> FETCH_HEAD

git_checkout exit 0 duration 78 ms · created 6/16/2026, 11:35:03 PM

git checkout f2f17085a61bb64b3a174339adbea59e9af85928 (after fetch)

Note: switching to 'f2f17085a61bb64b3a174339adbea59e9af85928'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at f2f1708 feat(CH2): prove `lemma_5_1_c` and `lemma_5_1_d` (#1507)

lake_cache exit 0 duration 57s · created 6/16/2026, 11:35:03 PM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 1 KB/s], Decompressed: 12
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 13 KB/s], Decompressed: 38
Downloaded: 73 file(s) [attempted 73/8459 = 0%, 28 KB/s], Decompressed: 70
Downloaded: 103 file(s) [attempted 103/8459 = 1%, 57 KB/s], Decompressed: 100
Downloaded: 135 file(s) [attempted 135/8459 = 1%, 519 KB/s], Decompressed: 127
Downloaded: 172 file(s) [attempted 172/8459 = 2%, 148 KB/s], Decompressed: 169
Downloaded: 206 file(s) [attempted 206/8459 = 2%, 295 KB/s], Decompressed: 199
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 128 KB/s], Decompressed: 206
Downloaded: 285 file(s) [attempted 285/8459 = 3%, 21 KB/s], Decompressed: 282
Downloaded: 326 file(s) [attempted 326/8459 = 3%, 105 KB/s], Decompressed: 312
Downloaded: 360 file(s) [attempted 360/8459 = 4%, 84 KB/s], Decompressed: 353
Downloaded: 395 file(s) [attempted 395/8459 = 4%, 190 KB/s], Decompressed: 391
Downloaded: 439 file(s) [attempted 439/8459 = 5%, 413 KB/s], Decompressed: 436
Downloaded: 484 file(s) [attempted 484/8459 = 5%, 379 KB/s], Decompressed: 480
Downloaded: 526 file(s) [attempted 526/8459 = 6%, 603 KB/s], Decompressed: 521
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 52 KB/s], Decompressed: 549
Downloaded: 593 file(s) [attempted 593/8459 = 7%, 869 KB/s], Decompressed: 590
Downloaded: 638 file(s) [attempted 638/8459 = 7%, 291 KB/s], Decompressed: 634
Downloaded: 679 file(s) [attempted 679/8459 = 8%, 104 KB/s], Decompressed: 669
Downloaded: 720 file(s) [attempted 720/8459 = 8%, 119 KB/s], Decompressed: 717
Downloaded: 762 file(s) [attempted 762/8459 = 9%, 768 KB/s], Decompressed: 751
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 294 KB/s], Decompressed: 792
Downloaded: 841 file(s) [attempted 841/8459 = 9%, 211 KB/s], Decompressed: 836
Downloaded: 874 file(s) [attempted 874/8459 = 10%, 266 KB/s], Decompressed: 867
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 541 KB/s], Decompressed: 908
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 228 KB/s], Decompressed: 956
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 154 KB/s], Decompressed: 991
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 44 KB/s], Decompressed: 1038
Downloaded: 1088 file(s) [attempted 1088/8459 = 12%, 407 KB/s], Decompressed: 1076
Downloaded: 1123 file(s) [attempted 1123/8459 = 13%, 146 KB/s], Decompressed: 1117
Downloaded: 1160 file(s) [attempted 1160/8459 = 13%, 439 KB/s], Decompressed: 1155
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 308 KB/s], Decompressed: 1196
Downloaded: 1244 file(s) [attempted 1244/8459 = 14%, 144 KB/s], Decompressed: 1240
Downloaded: 1285 file(s) [attempted 1285/8459 = 15%, 143 KB/s], Decompressed: 1278
Downloaded: 1327 file(s) [attempted 1327/8459 = 15%, 383 KB/s], Decompressed: 1319
Downloaded: 1364 file(s) [attempted 1364/8459 = 16%, 306 KB/s], Decompressed: 1360
Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 62 KB/s], Decompressed: 1394
Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 127 KB/s], Decompressed: 1439
Downloaded: 1488 file(s) [attempted 1488/8459 = 17%, 64 KB/s], Decompressed: 1483
Downloaded: 1531 file(s) [attempted 1531/8459 = 18%, 127 KB/s], Decompressed: 1524
Downloaded: 1568 file(s) [attempted 1568/8459 = 18%, 217 KB/s], Decompressed: 1562
Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 317 KB/s], Decompressed: 1593
Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 201 KB/s], Decompressed: 1641
Downloaded: 1689 file(s) [attempted 1689/8459 = 19%, 37 KB/s], Decompressed: 1685
Downloaded: 1733 file(s) [attempted 1733/8459 = 20%, 442 KB/s], Decompressed: 1730
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 145 KB/s], Decompressed: 1771
Downloaded: 1814 file(s) [attempted 1814/8459 = 21%, 590 KB/s], Decompressed: 1805
Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 85 KB/s], Decompressed: 1843
Downloaded: 1891 file(s) [attempted 1891/8459 = 22%, 812 KB/s], Decompressed: 1887
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 281 KB/s], Decompressed: 1928
Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 39 KB/s], Decompressed: 1969
Downloaded: 2014 file(s) [attempted 2014/8459 = 23%, 303 KB/s], Decompressed: 2010
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 92 KB/s], Decompressed: 2045
Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 128 KB/s], Decompressed: 2089
Downloaded: 2134 file(s) [attempted 2134/8459 = 25%, 727 KB/s], Decompressed: 2130
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 197 KB/s], Decompressed: 2171
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 113 KB/s], Decompressed: 2212
Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 48 KB/s], Decompressed: 2247
Downloaded: 2294 file(s) [attempted 2294/8459 = 27%, 27 KB/s], Decompressed: 2291
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 48 KB/s], Decompressed: 2332
Downloaded: 2377 file(s) [attempted 2377/8459 = 28%, 1032 KB/s], Decompressed: 2366
Downloaded: 2414 file(s) [attempted 2414/8459 = 28%, 455 KB/s], Decompressed: 2411
Downloaded: 2449 file(s) [attempted 2449/8459 = 28%, 373 KB/s], Decompressed: 2445
Downloaded: 2490 file(s) [attempted 2490/8459 = 29%, 295 KB/s], Decompressed: 2486
Downloaded: 2532 file(s) [attempted 2532/8459 = 29%, 589 KB/s], Decompressed: 2527
Downloaded: 2575 file(s) [attempted 2575/8459 = 30%, 166 KB/s], Decompressed: 2572
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 61 KB/s], Decompressed: 2609
Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 1297 KB/s], Decompressed: 2633
Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 133 KB/s], Decompressed: 2661
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 138 KB/s], Decompressed: 2688
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 70 KB/s], Decompressed: 2729
Downloaded: 2780 file(s) [attempted 2780/8459 = 32%, 155 KB/s], Decompressed: 2774
Downloaded: 2822 file(s) [attempted 2822/8459 = 33%, 94 KB/s], Decompressed: 2796
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 764 KB/s], Decompressed: 2849
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 30 KB/s], Decompressed: 2887
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 670 KB/s], Decompressed: 2931
Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 24 KB/s], Decompressed: 2979
Downloaded: 3023 file(s) [attempted 3023/8459 = 35%, 142 KB/s], Decompressed: 3006
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 30 KB/s], Decompressed: 3044
Downloaded: 3092 file(s) [attempted 3092/8459 = 36%, 384 KB/s], Decompressed: 3088
Downloaded: 3136 file(s) [attempted 3136/8459 = 37%, 546 KB/s], Decompressed: 3133
Downloaded: 3181 file(s) [attempted 3181/8459 = 37%, 343 KB/s], Decompressed: 3177
Downloaded: 3225 file(s) [attempted 3225/8459 = 38%, 139 KB/s], Decompressed: 3215
Downloaded: 3260 file(s) [attempted 3260/8459 = 38%, 138 KB/s], Decompressed: 3256
Downloaded: 3298 file(s) [attempted 3298/8459 = 38%, 529 KB/s], Decompressed: 3290
Downloaded: 3339 file(s) [attempted 3339/8459 = 39%, 1347 KB/s], Decompressed: 3337
Downloaded: 3379 file(s) [attempted 3379/8459 = 39%, 375 KB/s], Decompressed: 3375
Downloaded: 3417 file(s) [attempted 3417/8459 = 40%, 343 KB/s], Decompressed: 3410
Downloaded: 3458 file(s) [attempted 3458/8459 = 40%, 688 KB/s], Decompressed: 3455
Downloaded: 3493 file(s) [attempted 3493/8459 = 41%, 1027 KB/s], Decompressed: 3489
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 25 KB/s], Decompressed: 3533
Downloaded: 3574 file(s) [attempted 3574/8459 = 42%, 73 KB/s], Decompressed: 3568
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 37 KB/s], Decompressed: 3605
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 122 KB/s], Decompressed: 3650
Downloaded: 3693 file(s) [attempted 3693/8459 = 43%, 54 KB/s], Decompressed: 3684
Downloaded: 3732 file(s) [attempted 3732/8459 = 44%, 334 KB/s], Decompressed: 3722
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 36 KB/s], Decompressed: 3766
Downloaded: 3811 file(s) [attempted 3811/8459 = 45%, 133 KB/s], Decompressed: 3800
Downloaded: 3852 file(s) [attempted 3852/8459 = 45%, 105 KB/s], Decompressed: 3848
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 40 KB/s], Decompressed: 3886
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 369 KB/s], Decompressed: 3900
Downloaded: 3968 file(s) [attempted 3968/8459 = 46%, 99 KB/s], Decompressed: 3900
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 309 KB/s], Decompressed: 4006
Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 550 KB/s], Decompressed: 4043
Downloaded: 4088 file(s) [attempted 4088/8459 = 48%, 51 KB/s], Decompressed: 4081
Downloaded: 4123 file(s) [attempted 4123/8459 = 48%, 1158 KB/s], Decompressed: 4119
Downloaded: 4163 file(s) [attempted 4163/8459 = 49%, 57 KB/s], Decompressed: 4160
Downloaded: 4204 file(s) [attempted 4204/8459 = 49%, 589 KB/s], Decompressed: 4197
Downloaded: 4242 file(s) [attempted 4242/8459 = 50%, 509 KB/s], Decompressed: 4238
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 331 KB/s], Decompressed: 4273
Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 61 KB/s], Decompressed: 4310
Downloaded: 4359 file(s) [attempted 4359/8459 = 51%, 298 KB/s], Decompressed: 4355
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 493 KB/s], Decompressed: 4389
Downloaded: 4433 file(s) [attempted 4433/8459 = 52%, 710 KB/s], Decompressed: 4423
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 52 KB/s], Decompressed: 4464
Downloaded: 4516 file(s) [attempted 4516/8459 = 53%, 106 KB/s], Decompressed: 4512
Downloaded: 4563 file(s) [attempted 4563/8459 = 53%, 113 KB/s], Decompressed: 4553
Downloaded: 4598 file(s) [attempted 4598/8459 = 54%, 549 KB/s], Decompressed: 4584
Downloaded: 4635 file(s) [attempted 4635/8459 = 54%, 133 KB/s], Decompressed: 4584
Downloaded: 4676 file(s) [attempted 4676/8459 = 55%, 539 KB/s], Decompressed: 4591
Downloaded: 4720 file(s) [attempted 4720/8459 = 55%, 124 KB/s], Decompressed: 4714
Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 377 KB/s], Decompressed: 4762
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 414 KB/s], Decompressed: 4807
Downloaded: 4861 file(s) [attempted 4861/8459 = 57%, 135 KB/s], Decompressed: 4854
Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 237 KB/s], Decompressed: 4895
Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 167 KB/s], Decompressed: 4931
Downloaded: 4974 file(s) [attempted 4974/8459 = 58%, 74 KB/s], Decompressed: 4967
Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 98 KB/s], Decompressed: 5012
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 51 KB/s], Decompressed: 5046
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 140 KB/s], Decompressed: 5087
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 61 KB/s], Decompressed: 5121
Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 81 KB/s], Decompressed: 5162
Downloaded: 5222 file(s) [attempted 5222/8459 = 61%, 56 KB/s], Decompressed: 5217
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 130 KB/s], Decompressed: 5255
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 395 KB/s], Decompressed: 5293
Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 252 KB/s], Decompressed: 5330
Downloaded: 5381 file(s) [attempted 5381/8459 = 63%, 325 KB/s], Decompressed: 5380
Downloaded: 5423 file(s) [attempted 5423/8459 = 64%, 96 KB/s], Decompressed: 5409
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 214 KB/s], Decompressed: 5453
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 1018 KB/s], Decompressed: 5481
Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 39 KB/s], Decompressed: 5481
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 336 KB/s], Decompressed: 5484
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 296 KB/s], Decompressed: 5614
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 147 KB/s], Decompressed: 5659
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 638 KB/s], Decompressed: 5689
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 99 KB/s], Decompressed: 5734
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 112 KB/s], Decompressed: 5778
Downloaded: 5823 file(s) [attempted 5823/8459 = 68%, 108 KB/s], Decompressed: 5816
Downloaded: 5863 file(s) [attempted 5863/8459 = 69%, 168 KB/s], Decompressed: 5854
Downloaded: 5899 file(s) [attempted 5899/8459 = 69%, 47 KB/s], Decompressed: 5895
Downloaded: 5937 file(s) [attempted 5937/8459 = 70%, 61 KB/s], Decompressed: 5932
Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 274 KB/s], Decompressed: 5974
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 102 KB/s], Decompressed: 6015
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 223 KB/s], Decompressed: 6056
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 59 KB/s], Decompressed: 6093
Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 228 KB/s], Decompressed: 6128
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 44 KB/s], Decompressed: 6128
Downloaded: 6217 file(s) [attempted 6217/8459 = 73%, 473 KB/s], Decompressed: 6131
Downloaded: 6254 file(s) [attempted 6254/8459 = 73%, 942 KB/s], Decompressed: 6251
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 129 KB/s], Decompressed: 6288
Downloaded: 6329 file(s) [attempted 6329/8459 = 74%, 50 KB/s], Decompressed: 6326
Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 181 KB/s], Decompressed: 6367
Downloaded: 6412 file(s) [attempted 6412/8459 = 75%, 44 KB/s], Decompressed: 6408
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 1294 KB/s], Decompressed: 6436
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 173 KB/s], Decompressed: 6483
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 57 KB/s], Decompressed: 6525
Downloaded: 6569 file(s) [attempted 6569/8459 = 77%, 149 KB/s], Decompressed: 6566
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 616 KB/s], Decompressed: 6593
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 964 KB/s], Decompressed: 6593
Downloaded: 6689 file(s) [attempted 6689/8459 = 79%, 145 KB/s], Decompressed: 6596
Downloaded: 6728 file(s) [attempted 6728/8459 = 79%, 113 KB/s], Decompressed: 6596
Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 124 KB/s], Decompressed: 6596
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 43 KB/s], Decompressed: 6596
Downloaded: 6850 file(s) [attempted 6850/8459 = 80%, 114 KB/s], Decompressed: 6596
Downloaded: 6887 file(s) [attempted 6887/8459 = 81%, 1967 KB/s], Decompressed: 6596
Downloaded: 6928 file(s) [attempted 6928/8459 = 81%, 253 KB/s], Decompressed: 6596
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 409 KB/s], Decompressed: 6679
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 428 KB/s], Decompressed: 6679
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 99 KB/s], Decompressed: 6679
Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 129 KB/s], Decompressed: 7086
Downloaded: 7134 file(s) [attempted 7134/8459 = 84%, 83 KB/s], Decompressed: 7130
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 292 KB/s], Decompressed: 7171
Downloaded: 7219 file(s) [attempted 7219/8459 = 85%, 193 KB/s], Decompressed: 7216
Downloaded: 7260 file(s) [attempted 7260/8459 = 85%, 1042 KB/s], Decompressed: 7257
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 45 KB/s], Decompressed: 7298
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 312 KB/s], Decompressed: 7336
Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 60 KB/s], Decompressed: 7380
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 523 KB/s], Decompressed: 7408
Downloaded: 7460 file(s) [attempted 7460/8459 = 88%, 472 KB/s], Decompressed: 7455
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 170 KB/s], Decompressed: 7496
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 587 KB/s], Decompressed: 7534
Downloaded: 7582 file(s) [attempted 7582/8459 = 89%, 109 KB/s], Decompressed: 7575
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 1297 KB/s], Decompressed: 7620
Downloaded: 7661 file(s) [attempted 7661/8459 = 90%, 204 KB/s], Decompressed: 7657
Downloaded: 7697 file(s) [attempted 7697/8459 = 90%, 59 KB/s], Decompressed: 7692
Downloaded: 7735 file(s) [attempted 7735/8459 = 91%, 28 KB/s], Decompressed: 7729
Downloaded: 7777 file(s) [attempted 7777/8459 = 91%, 1476 KB/s], Decompressed: 7770
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 420 KB/s], Decompressed: 7811
Downloaded: 7852 file(s) [attempted 7852/8459 = 92%, 303 KB/s], Decompressed: 7849
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 1222 KB/s], Decompressed: 7887
Downloaded: 7931 file(s) [attempted 7931/8459 = 93%, 639 KB/s], Decompressed: 7928
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 200 KB/s], Decompressed: 7952
Downloaded: 8013 file(s) [attempted 8013/8459 = 94%, 327 KB/s], Decompressed: 8006
Downloaded: 8047 file(s) [attempted 8047/8459 = 95%, 370 KB/s], Decompressed: 8041
Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 346 KB/s], Decompressed: 8082
Downloaded: 8130 file(s) [attempted 8130/8459 = 96%, 875 KB/s], Decompressed: 8119
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 105 KB/s], Decompressed: 8160
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 384 KB/s], Decompressed: 8208
Downloaded: 8253 file(s) [attempted 8253/8459 = 97%, 540 KB/s], Decompressed: 8246
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 505 KB/s], Decompressed: 8287
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 1149 KB/s], Decompressed: 8328
Downloaded: 8376 file(s) [attempted 8376/8459 = 99%, 584 KB/s], Decompressed: 8373
Downloaded: 8420 file(s) [attempted 8420/8459 = 99%, 225 KB/s], Decompressed: 8417
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 516 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 516 KB/s], Decompressed: 8455

lean_checker exit 0 duration 19m 11s · created 6/16/2026, 11:35:03 PM

lake build

✔ [3460/3468] Built PrimeNumberTheoremAnd.ZetaBounds (93s)
ℹ [3473/3481] Built PrimeNumberTheoremAnd.MediumPNT (31s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3496/3504] Built PrimeNumberTheoremAnd.StrongPNT (15s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3500/3505] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.8s)
✔ [3631/3641] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (8.9s)
⚠ [3634/3646] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3639/3646] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3703/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (45s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3705/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (3.0s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3707/3710] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.8s)
✔ [3809/3820] Built PrimeNumberTheoremAnd.IEANTN.LogTables (9.1s)
⚠ [3810/3820] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3813/3822] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.8s)
✔ [3815/3822] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (3.4s)
⚠ [3816/3823] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [3820/3824] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (11s)
✔ [3823/3827] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (9.1s)
⚠ [3945/3955] Built PrimeNumberTheoremAnd.IEANTN.Buthe (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [3947/3958] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (18s)
⚠ [3949/3958] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (6.2s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [3950/3958] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (97s)
⚠ [3951/3958] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (72s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3954/3963] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (38s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [3955/3963] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3956/3963] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [3960/3963] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (33s)
⚠ [3962/3968] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (58s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [3967/3975] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (62s)
✔ [3970/3982] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (3.4s)
⚠ [3971/3982] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [3972/3982] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (10s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2766:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2816:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2872:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2934:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2969:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2999:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3163:8: declaration uses `sorry`
✔ [3974/3982] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (16s)
⚠ [3976/3982] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (46s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [3979/3983] Built PrimeNumberTheoremAnd.IEANTN.Dusart (43s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [3982/3985] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (54s)
✔ [3999/4010] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (62s)
⚠ [4002/4021] Built PrimeNumberTheoremAnd.IEANTN.Mertens (15s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4003/4021] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (16s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
✔ [4004/4021] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (12s)
⚠ [4006/4021] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (6.7s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4007/4021] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4009/4021] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (3.3s)
⚠ [4014/4035] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (11s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4015/4035] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.8s)
✔ [4017/4035] Built PrimeNumberTheoremAnd.IEANTN.Lcm (28s)
⚠ [4019/4046] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (7.7s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4023/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (2.7s)
✔ [4026/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (2.7s)
ℹ [4030/4046] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (18s)
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4032/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.1s)
✔ [4033/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (2.1s)
✔ [4037/4046] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (2.3s)
✔ [4040/4046] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (56s)
✔ [4044/4046] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (2.2s)
✔ [4045/4046] Built PrimeNumberTheoremAnd (3.8s)
Build completed successfully (4046 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

blueprint_build exit 0 duration 15m 39s · created 6/16/2026, 11:35:03 PM

lake build :blueprint

✔ [14/35] Built Batteries.Lean.NameMapAttribute:c.o (817ms)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (539ms)
✔ [33/35] Built Cli:c.o (86ms)
✔ [3492/3507] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (73s)
ℹ [3505/3511] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3507/3513] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (60s)
⚠ [3531/3547] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3536/3548] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3542/3552] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.9s)
⚠ [3681/3702] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3685/3702] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.5s)
⚠ [3691/3702] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3754/3764] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3756/3765] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (27s)
⚠ [3757/3765] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3759/3765] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.5s)
✔ [3762/3775] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.1s)
✔ [3865/3886] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (4.8s)
⚠ [3867/3886] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3870/3887] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.6s)
⚠ [3871/3887] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [3876/3889] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3877/3889] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.3s)
✔ [3886/3891] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (11s)
✔ [3888/3900] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.9s)
⚠ [4008/4023] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4012/4030] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.5s)
⚠ [4015/4032] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4016/4032] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (6.4s)
⚠ [4017/4032] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [4021/4033] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
⚠ [4022/4033] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
✔ [4023/4034] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (5.6s)
✔ [4025/4036] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (108s)
⚠ [4026/4036] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [4028/4036] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [4029/4036] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (60s)
⚠ [4033/4037] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [4034/4042] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (9.0s)
✔ [4035/4042] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (52s)
✔ [4044/4063] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.8s)
✔ [4045/4063] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.6s)
⚠ [4046/4063] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [4047/4064] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2766:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2816:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2872:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2934:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2969:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2999:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3163:8: declaration uses `sorry`
✔ [4049/4065] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (17s)
✔ [4051/4065] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.5s)
⚠ [4052/4065] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
⚠ [4054/4065] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4058/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (19s)
✔ [4059/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (21s)
✔ [4061/4067] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4064/4069] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4084/4110] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4085/4110] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4088/4124] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
✔ [4089/4124] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4090/4124] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4091/4124] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (35s)
⚠ [4094/4124] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
⚠ [4102/4124] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
✔ [4103/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (16s)
⚠ [4104/4154] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4105/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (17s)
✔ [4107/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (30s)
✔ [4112/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.0s)
✔ [4121/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.8s)
✔ [4122/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4123/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (4.2s)
ℹ [4124/4169] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4141/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.6s)
✔ [4144/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.6s)
✔ [4149/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.1s)
✔ [4152/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.3s)
✔ [4153/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (2.2s)
✔ [4155/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.5s)
✔ [4158/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4165/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (2.3s)
✔ [4167/4169] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (4.3s)
ℹ [4168/4170] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (81ms)
info: Blueprint indexing
Build completed successfully (4170 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 16m 28s · created 6/16/2026, 11:35:03 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)

apx-semantic-phase	{"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":264,"diagnostic_count":80,"duration_ms":27531,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase	{"declaration_count":264,"dependency_count":1080,"diagnostic_count":90,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase	{"duration_ms":886790,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase	{"declaration_count":264,"dependency_count":1080,"diagnostic_count":90,"duration_ms":252,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase	{"duration_ms":1,"ok":true,"payload_bytes":2370291,"phase":"lean_json_serialize"}
apx-semantic-phase	{"duration_ms":16,"ok":true,"payload_bytes":2370291,"phase":"lean_json_write"}

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"core_compile","duration_ms":7098}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":262,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"runner_compile","duration_ms":50005,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache f53cb0c960be59836d3b9e9d22459cdf3d4ed23e5a0511074cca895dbac7a473
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase	{"phase":"lean_import_env_extract_write","duration_ms":929428,"ok":true}