Verification run

Run 124

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via github_backfill

succeeded commit e6de9503decf toolchain lean-v4-30-0 prover lean took 38m 41s · finished 2w 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

KB/s], Decompressed: 908
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 219 KB/s], Decompressed: 956
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 558 KB/s], Decompressed: 991
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 891 KB/s], Decompressed: 1028
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 77 KB/s], Decompressed: 1069
Downloaded: 1118 file(s) [attempted 1118/8459 = 13%, 244 KB/s], Decompressed: 1114
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 447 KB/s], Decompressed: 1155
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 269 KB/s], Decompressed: 1196
Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 127 KB/s], Decompressed: 1230
Downloaded: 1278 file(s) [attempted 1278/8459 = 15%, 301 KB/s], Decompressed: 1275
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 774 KB/s], Decompressed: 1312
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 204 KB/s], Decompressed: 1357
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 393 KB/s], Decompressed: 1394
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 651 KB/s], Decompressed: 1432
Downloaded: 1480 file(s) [attempted 1480/8459 = 17%, 1435 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 411 KB/s], Decompressed: 1511
Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 1046 KB/s], Decompressed: 1562
Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 31 KB/s], Decompressed: 1607
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 327 KB/s], Decompressed: 1644
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 350 KB/s], Decompressed: 1678
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 248 KB/s], Decompressed: 1723
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 473 KB/s], Decompressed: 1767
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 322 KB/s], Decompressed: 1805
Downloaded: 1850 file(s) [attempted 1850/8459 = 21%, 732 KB/s], Decompressed: 1843
Downloaded: 1884 file(s) [attempted 1884/8459 = 22%, 680 KB/s], Decompressed: 1877
Downloaded: 1921 file(s) [attempted 1921/8459 = 22%, 458 KB/s], Decompressed: 1887
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 298 KB/s], Decompressed: 1956
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 608 KB/s], Decompressed: 2000
Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 407 KB/s], Decompressed: 2028
Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 238 KB/s], Decompressed: 2072
Downloaded: 2120 file(s) [attempted 2120/8459 = 25%, 40 KB/s], Decompressed: 2110
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 160 KB/s], Decompressed: 2154
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 174 KB/s], Decompressed: 2195
Downloaded: 2236 file(s) [attempted 2236/8459 = 26%, 477 KB/s], Decompressed: 2229
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 652 KB/s], Decompressed: 2257
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 36 KB/s], Decompressed: 2260
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 1865 KB/s], Decompressed: 2355
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 526 KB/s], Decompressed: 2395
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 23 KB/s], Decompressed: 2425
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 427 KB/s], Decompressed: 2466
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 254 KB/s], Decompressed: 2510
Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 52 KB/s], Decompressed: 2544
Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 38 KB/s], Decompressed: 2589
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 865 KB/s], Decompressed: 2626
Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 177 KB/s], Decompressed: 2668
Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 134 KB/s], Decompressed: 2705
Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 228 KB/s], Decompressed: 2750
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 453 KB/s], Decompressed: 2794
Downloaded: 2832 file(s) [attempted 2832/8459 = 33%, 212 KB/s], Decompressed: 2818
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 979 KB/s], Decompressed: 2869
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 220 KB/s], Decompressed: 2904
Downloaded: 2956 file(s) [attempted 2956/8459 = 34%, 143 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 417 KB/s], Decompressed: 2989
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 224 KB/s], Decompressed: 3023
Downloaded: 3084 file(s) [attempted 3084/8459 = 36%, 526 KB/s], Decompressed: 3065
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 158 KB/s], Decompressed: 3109
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 315 KB/s], Decompressed: 3150
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 64 KB/s], Decompressed: 3191
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 1322 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 314 KB/s], Decompressed: 3273
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 349 KB/s], Decompressed: 3314
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 63 KB/s], Decompressed: 3355
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 58 KB/s], Decompressed: 3400
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 61 KB/s], Decompressed: 3424
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 566 KB/s], Decompressed: 3482
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 382 KB/s], Decompressed: 3516
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 402 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 598 KB/s], Decompressed: 3598
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 210 KB/s], Decompressed: 3643
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 29 KB/s], Decompressed: 3681
Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 749 KB/s], Decompressed: 3725
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 606 KB/s], Decompressed: 3763
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 431 KB/s], Decompressed: 3804
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 710 KB/s], Decompressed: 3845
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 406 KB/s], Decompressed: 3886
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 95 KB/s], Decompressed: 3917
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 229 KB/s], Decompressed: 3961
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 161 KB/s], Decompressed: 4002
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 553 KB/s], Decompressed: 4047
Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1271 KB/s], Decompressed: 4088
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 285 KB/s], Decompressed: 4129
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 289 KB/s], Decompressed: 4167
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 213 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 32 KB/s], Decompressed: 4245
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 1048 KB/s], Decompressed: 4286
Downloaded: 4331 file(s) [attempted 4331/8459 = 51%, 61 KB/s], Decompressed: 4327
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 797 KB/s], Decompressed: 4372
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 104 KB/s], Decompressed: 4406
Downloaded: 4454 file(s) [attempted 4454/8459 = 52%, 1892 KB/s], Decompressed: 4447
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 233 KB/s], Decompressed: 4488
Downloaded: 4533 file(s) [attempted 4533/8459 = 53%, 432 KB/s], Decompressed: 4529
Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 493 KB/s], Decompressed: 4574
Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 2198 KB/s], Decompressed: 4611
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 23 KB/s], Decompressed: 4642
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 96 KB/s], Decompressed: 4687
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 93 KB/s], Decompressed: 4724
Downloaded: 4776 file(s) [attempted 4776/8459 = 56%, 1305 KB/s], Decompressed: 4772
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 280 KB/s], Decompressed: 4807
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 169 KB/s], Decompressed: 4844
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 45 KB/s], Decompressed: 4889
Downloaded: 4934 file(s) [attempted 4934/8459 = 58%, 263 KB/s], Decompressed: 4930
Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 72 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 146 KB/s], Decompressed: 5017
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 88 KB/s], Decompressed: 5039
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 319 KB/s], Decompressed: 5094
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 1356 KB/s], Decompressed: 5128
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 433 KB/s], Decompressed: 5173
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 77 KB/s], Decompressed: 5207
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 36 KB/s], Decompressed: 5241
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 718 KB/s], Decompressed: 5286
Downloaded: 5344 file(s) [attempted 5344/8459 = 63%, 270 KB/s], Decompressed: 5340
Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 169 KB/s], Decompressed: 5375
Downloaded: 5426 file(s) [attempted 5426/8459 = 64%, 365 KB/s], Decompressed: 5419
Downloaded: 5467 file(s) [attempted 5467/8459 = 64%, 773 KB/s], Decompressed: 5457
Downloaded: 5505 file(s) [attempted 5505/8459 = 65%, 30 KB/s], Decompressed: 5494
Downloaded: 5546 file(s) [attempted 5546/8459 = 65%, 228 KB/s], Decompressed: 5539
Downloaded: 5584 file(s) [attempted 5584/8459 = 66%, 334 KB/s], Decompressed: 5580
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 295 KB/s], Decompressed: 5621
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 157 KB/s], Decompressed: 5655
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 632 KB/s], Decompressed: 5689
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 195 KB/s], Decompressed: 5734
Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 528 KB/s], Decompressed: 5775
Downloaded: 5816 file(s) [attempted 5816/8459 = 68%, 197 KB/s], Decompressed: 5809
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 595 KB/s], Decompressed: 5850
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 99 KB/s], Decompressed: 5891
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 863 KB/s], Decompressed: 5932
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 206 KB/s], Decompressed: 5977
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 259 KB/s], Decompressed: 6015
Downloaded: 6056 file(s) [attempted 6056/8459 = 71%, 365 KB/s], Decompressed: 6052
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 528 KB/s], Decompressed: 6093
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 144 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 58 KB/s], Decompressed: 6179
Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 490 KB/s], Decompressed: 6189
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 87 KB/s], Decompressed: 6247
Downloaded: 6292 file(s) [attempted 6292/8459 = 74%, 133 KB/s], Decompressed: 6288
Downloaded: 6335 file(s) [attempted 6335/8459 = 74%, 358 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 180 KB/s], Decompressed: 6367
Downloaded: 6408 file(s) [attempted 6408/8459 = 75%, 212 KB/s], Decompressed: 6405
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 243 KB/s], Decompressed: 6446
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 295 KB/s], Decompressed: 6483
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 436 KB/s], Decompressed: 6525
Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 465 KB/s], Decompressed: 6569
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 55 KB/s], Decompressed: 6607
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 455 KB/s], Decompressed: 6641
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 240 KB/s], Decompressed: 6682
Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 115 KB/s], Decompressed: 6723
Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 632 KB/s], Decompressed: 6764
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 482 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 219 KB/s], Decompressed: 6836
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 154 KB/s], Decompressed: 6880
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 301 KB/s], Decompressed: 6922
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 142 KB/s], Decompressed: 6966
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 65 KB/s], Decompressed: 7011
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 323 KB/s], Decompressed: 7045
Downloaded: 7089 file(s) [attempted 7089/8459 = 83%, 1177 KB/s], Decompressed: 7082
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 281 KB/s], Decompressed: 7123
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 169 KB/s], Decompressed: 7168
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 58 KB/s], Decompressed: 7212
Downloaded: 7253 file(s) [attempted 7253/8459 = 85%, 166 KB/s], Decompressed: 7250
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 35 KB/s], Decompressed: 7288
Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 281 KB/s], Decompressed: 7325
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 437 KB/s], Decompressed: 7366
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 164 KB/s], Decompressed: 7411
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 814 KB/s], Decompressed: 7449
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 300 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 222 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 166 KB/s], Decompressed: 7568
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 490 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 468 KB/s], Decompressed: 7654
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 417 KB/s], Decompressed: 7695
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 142 KB/s], Decompressed: 7733
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 112 KB/s], Decompressed: 7777
Downloaded: 7822 file(s) [attempted 7822/8459 = 92%, 691 KB/s], Decompressed: 7808
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 32 KB/s], Decompressed: 7856
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 4062 KB/s], Decompressed: 7897
Downloaded: 7939 file(s) [attempted 7939/8459 = 93%, 87 KB/s], Decompressed: 7928
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 347 KB/s], Decompressed: 7976
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 117 KB/s], Decompressed: 8018
Downloaded: 8056 file(s) [attempted 8056/8459 = 95%, 170 KB/s], Decompressed: 8051
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 514 KB/s], Decompressed: 8092
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 510 KB/s], Decompressed: 8133
Downloaded: 8178 file(s) [attempted 8178/8459 = 96%, 54 KB/s], Decompressed: 8174
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 147 KB/s], Decompressed: 8212
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 324 KB/s], Decompressed: 8253
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 417 KB/s], Decompressed: 8290
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 84 KB/s], Decompressed: 8328
Downloaded: 8377 file(s) [attempted 8377/8459 = 99%, 324 KB/s], Decompressed: 8373
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 253 KB/s], Decompressed: 8410
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 173 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 173 KB/s], Decompressed: 8451


$ lake build
exit_code=Some(0) duration_ms=221699
stdout:
ℹ [3539/3551] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3571] 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`
⚠ [3697/3705] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3700/3714] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3761/3776] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3762/3776] 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`
⚠ [3876/3895] 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:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [3878/3895] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4012/4022] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4014/4022] 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`
⚠ [4015/4022] 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:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4017/4022] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
⚠ [4052/4064] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (135s)
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`
⚠ [4057/4071] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (33s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4059/4071] 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`
⚠ [4064/4079] 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`
⚠ [4068/4079] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
⚠ [4083/4093] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
⚠ [4088/4130] 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`
⚠ [4108/4140] 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`
⚠ [4109/4140] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4129/4153] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
⚠ [4133/4153] 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`
⚠ [4143/4153] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
ℹ [4145/4153] 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.
✔ [4152/4153] Built PrimeNumberTheoremAnd (12s)
Build completed successfully (4153 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=222527
stdout:
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.5s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (540ms)
✔ [33/42] Built Cli:c.o (67ms)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3626/3644] 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`
⚠ [3765/3784] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3785/3800] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3840/3858] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3842/3858] 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`
⚠ [3960/3982] 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:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [3963/3982] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4105/4120] 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`
⚠ [4108/4180] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4110/4180] 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:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4114/4180] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
⚠ [4147/4194] 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`
✔ [4173/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (136s)
⚠ [4174/4202] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4178/4202] 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`
⚠ [4181/4203] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
✔ [4191/4226] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (22s)
⚠ [4195/4226] 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`
⚠ [4218/4302] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
⚠ [4228/4302] 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`
⚠ [4244/4320] 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`
⚠ [4271/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4285/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
⚠ [4304/4342] 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`
ℹ [4325/4342] 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.
⚠ [4337/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4340/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (12s)
ℹ [4341/4343] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4343 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=1500668
stdout:
apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":11,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":443085,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":320,"diagnostic_count":113,"duration_ms":36261,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":406289,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":320,"diagnostic_count":113,"duration_ms":13,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2498619,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2498619,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":790,"diagnostic_count":517,"duration_ms":93057,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":412807,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":790,"diagnostic_count":517,"duration_ms":42,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":5590574,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":5590574,"phase":"lean_module_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":30516}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":7145,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"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":64783,"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 b3eb8b46ebc2eec89f6498d884bdaa414bda45f61bff9c1d776a70b947f592f7
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":1397256,"ok":true}

Stored Lean workspace build cache
Stored Lean semantic extraction cache

Command runs

git_clone exit 0 duration 866 ms · created 7/2/2026, 1:44:46 PM

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

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

git_checkout exit 128 duration 2 ms · created 7/2/2026, 1:44:46 PM

git checkout e6de9503decfd946ff9fb72d8324db8c4653fa40

fatal: reference is not a tree: e6de9503decfd946ff9fb72d8324db8c4653fa40

git_checkout exit 0 duration 929 ms · created 7/2/2026, 1:44:46 PM

git fetch --depth 1 origin e6de9503decfd946ff9fb72d8324db8c4653fa40

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

git_checkout exit 0 duration 56 ms · created 7/2/2026, 1:44:46 PM

git checkout e6de9503decfd946ff9fb72d8324db8c4653fa40 (after fetch)

Note: switching to 'e6de9503decfd946ff9fb72d8324db8c4653fa40'.

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 e6de950 CH2: bound the C∞ integral in Proposition 5.2 (prop_5_2_b, #1458) (#1557)

lake_cache exit 0 duration 1m 2s · created 7/2/2026, 1:44:46 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%, 10 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 3 KB/s], Decompressed: 9
Downloaded: 35 file(s) [attempted 35/8459 = 0%, 16 KB/s], Decompressed: 32
Downloaded: 65 file(s) [attempted 65/8459 = 0%, 339 KB/s], Decompressed: 58
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 193 KB/s], Decompressed: 86
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 330 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 95 KB/s], Decompressed: 151
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 126 KB/s], Decompressed: 172
Downloaded: 234 file(s) [attempted 234/8459 = 2%, 86 KB/s], Decompressed: 213
Downloaded: 278 file(s) [attempted 278/8459 = 3%, 453 KB/s], Decompressed: 258
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 494 KB/s], Decompressed: 302
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 23 KB/s], Decompressed: 350
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 1087 KB/s], Decompressed: 381
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 538 KB/s], Decompressed: 429
Downloaded: 473 file(s) [attempted 473/8459 = 5%, 2803 KB/s], Decompressed: 466
Downloaded: 510 file(s) [attempted 510/8459 = 6%, 591 KB/s], Decompressed: 504
Downloaded: 545 file(s) [attempted 545/8459 = 6%, 173 KB/s], Decompressed: 542
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 378 KB/s], Decompressed: 573
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 153 KB/s], Decompressed: 621
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 58 KB/s], Decompressed: 665
Downloaded: 710 file(s) [attempted 710/8459 = 8%, 28 KB/s], Decompressed: 703
Downloaded: 751 file(s) [attempted 751/8459 = 8%, 62 KB/s], Decompressed: 741
Downloaded: 792 file(s) [attempted 792/8459 = 9%, 212 KB/s], Decompressed: 785
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 208 KB/s], Decompressed: 823
Downloaded: 871 file(s) [attempted 871/8459 = 10%, 40 KB/s], Decompressed: 864
Downloaded: 915 file(s) [attempted 915/8459 = 10%, 549 KB/s], Decompressed: 908
Downloaded: 960 file(s) [attempted 960/8459 = 11%, 219 KB/s], Decompressed: 956
Downloaded: 1001 file(s) [attempted 1001/8459 = 11%, 558 KB/s], Decompressed: 991
Downloaded: 1042 file(s) [attempted 1042/8459 = 12%, 891 KB/s], Decompressed: 1028
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 77 KB/s], Decompressed: 1069
Downloaded: 1118 file(s) [attempted 1118/8459 = 13%, 244 KB/s], Decompressed: 1114
Downloaded: 1158 file(s) [attempted 1158/8459 = 13%, 447 KB/s], Decompressed: 1155
Downloaded: 1199 file(s) [attempted 1199/8459 = 14%, 269 KB/s], Decompressed: 1196
Downloaded: 1237 file(s) [attempted 1237/8459 = 14%, 127 KB/s], Decompressed: 1230
Downloaded: 1278 file(s) [attempted 1278/8459 = 15%, 301 KB/s], Decompressed: 1275
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 774 KB/s], Decompressed: 1312
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 204 KB/s], Decompressed: 1357
Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 393 KB/s], Decompressed: 1394
Downloaded: 1435 file(s) [attempted 1435/8459 = 16%, 651 KB/s], Decompressed: 1432
Downloaded: 1480 file(s) [attempted 1480/8459 = 17%, 1435 KB/s], Decompressed: 1477
Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 411 KB/s], Decompressed: 1511
Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 1046 KB/s], Decompressed: 1562
Downloaded: 1610 file(s) [attempted 1610/8459 = 19%, 31 KB/s], Decompressed: 1607
Downloaded: 1648 file(s) [attempted 1648/8459 = 19%, 327 KB/s], Decompressed: 1644
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 350 KB/s], Decompressed: 1678
Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 248 KB/s], Decompressed: 1723
Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 473 KB/s], Decompressed: 1767
Downloaded: 1812 file(s) [attempted 1812/8459 = 21%, 322 KB/s], Decompressed: 1805
Downloaded: 1850 file(s) [attempted 1850/8459 = 21%, 732 KB/s], Decompressed: 1843
Downloaded: 1884 file(s) [attempted 1884/8459 = 22%, 680 KB/s], Decompressed: 1877
Downloaded: 1921 file(s) [attempted 1921/8459 = 22%, 458 KB/s], Decompressed: 1887
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 298 KB/s], Decompressed: 1956
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 608 KB/s], Decompressed: 2000
Downloaded: 2038 file(s) [attempted 2038/8459 = 24%, 407 KB/s], Decompressed: 2028
Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 238 KB/s], Decompressed: 2072
Downloaded: 2120 file(s) [attempted 2120/8459 = 25%, 40 KB/s], Decompressed: 2110
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 160 KB/s], Decompressed: 2154
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 174 KB/s], Decompressed: 2195
Downloaded: 2236 file(s) [attempted 2236/8459 = 26%, 477 KB/s], Decompressed: 2229
Downloaded: 2274 file(s) [attempted 2274/8459 = 26%, 652 KB/s], Decompressed: 2257
Downloaded: 2315 file(s) [attempted 2315/8459 = 27%, 36 KB/s], Decompressed: 2260
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 1865 KB/s], Decompressed: 2355
Downloaded: 2397 file(s) [attempted 2397/8459 = 28%, 526 KB/s], Decompressed: 2395
Downloaded: 2431 file(s) [attempted 2431/8459 = 28%, 23 KB/s], Decompressed: 2425
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 427 KB/s], Decompressed: 2466
Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 254 KB/s], Decompressed: 2510
Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 52 KB/s], Decompressed: 2544
Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 38 KB/s], Decompressed: 2589
Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 865 KB/s], Decompressed: 2626
Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 177 KB/s], Decompressed: 2668
Downloaded: 2712 file(s) [attempted 2712/8459 = 32%, 134 KB/s], Decompressed: 2705
Downloaded: 2757 file(s) [attempted 2757/8459 = 32%, 228 KB/s], Decompressed: 2750
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 453 KB/s], Decompressed: 2794
Downloaded: 2832 file(s) [attempted 2832/8459 = 33%, 212 KB/s], Decompressed: 2818
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 979 KB/s], Decompressed: 2869
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 220 KB/s], Decompressed: 2904
Downloaded: 2956 file(s) [attempted 2956/8459 = 34%, 143 KB/s], Decompressed: 2952
Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 417 KB/s], Decompressed: 2989
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 224 KB/s], Decompressed: 3023
Downloaded: 3084 file(s) [attempted 3084/8459 = 36%, 526 KB/s], Decompressed: 3065
Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 158 KB/s], Decompressed: 3109
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 315 KB/s], Decompressed: 3150
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 64 KB/s], Decompressed: 3191
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 1322 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 314 KB/s], Decompressed: 3273
Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 349 KB/s], Decompressed: 3314
Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 63 KB/s], Decompressed: 3355
Downloaded: 3403 file(s) [attempted 3403/8459 = 40%, 58 KB/s], Decompressed: 3400
Downloaded: 3448 file(s) [attempted 3448/8459 = 40%, 61 KB/s], Decompressed: 3424
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 566 KB/s], Decompressed: 3482
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 382 KB/s], Decompressed: 3516
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 402 KB/s], Decompressed: 3561
Downloaded: 3605 file(s) [attempted 3605/8459 = 42%, 598 KB/s], Decompressed: 3598
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 210 KB/s], Decompressed: 3643
Downloaded: 3687 file(s) [attempted 3687/8459 = 43%, 29 KB/s], Decompressed: 3681
Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 749 KB/s], Decompressed: 3725
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 606 KB/s], Decompressed: 3763
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 431 KB/s], Decompressed: 3804
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 710 KB/s], Decompressed: 3845
Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 406 KB/s], Decompressed: 3886
Downloaded: 3927 file(s) [attempted 3927/8459 = 46%, 95 KB/s], Decompressed: 3917
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 229 KB/s], Decompressed: 3961
Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 161 KB/s], Decompressed: 4002
Downloaded: 4050 file(s) [attempted 4050/8459 = 47%, 553 KB/s], Decompressed: 4047
Downloaded: 4091 file(s) [attempted 4091/8459 = 48%, 1271 KB/s], Decompressed: 4088
Downloaded: 4132 file(s) [attempted 4132/8459 = 48%, 285 KB/s], Decompressed: 4129
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 289 KB/s], Decompressed: 4167
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 213 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 32 KB/s], Decompressed: 4245
Downloaded: 4293 file(s) [attempted 4293/8459 = 50%, 1048 KB/s], Decompressed: 4286
Downloaded: 4331 file(s) [attempted 4331/8459 = 51%, 61 KB/s], Decompressed: 4327
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 797 KB/s], Decompressed: 4372
Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 104 KB/s], Decompressed: 4406
Downloaded: 4454 file(s) [attempted 4454/8459 = 52%, 1892 KB/s], Decompressed: 4447
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 233 KB/s], Decompressed: 4488
Downloaded: 4533 file(s) [attempted 4533/8459 = 53%, 432 KB/s], Decompressed: 4529
Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 493 KB/s], Decompressed: 4574
Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 2198 KB/s], Decompressed: 4611
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 23 KB/s], Decompressed: 4642
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 96 KB/s], Decompressed: 4687
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 93 KB/s], Decompressed: 4724
Downloaded: 4776 file(s) [attempted 4776/8459 = 56%, 1305 KB/s], Decompressed: 4772
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 280 KB/s], Decompressed: 4807
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 169 KB/s], Decompressed: 4844
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 45 KB/s], Decompressed: 4889
Downloaded: 4934 file(s) [attempted 4934/8459 = 58%, 263 KB/s], Decompressed: 4930
Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 72 KB/s], Decompressed: 4974
Downloaded: 5022 file(s) [attempted 5022/8459 = 59%, 146 KB/s], Decompressed: 5017
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 88 KB/s], Decompressed: 5039
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 319 KB/s], Decompressed: 5094
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 1356 KB/s], Decompressed: 5128
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 433 KB/s], Decompressed: 5173
Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 77 KB/s], Decompressed: 5207
Downloaded: 5258 file(s) [attempted 5258/8459 = 62%, 36 KB/s], Decompressed: 5241
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 718 KB/s], Decompressed: 5286
Downloaded: 5344 file(s) [attempted 5344/8459 = 63%, 270 KB/s], Decompressed: 5340
Downloaded: 5385 file(s) [attempted 5385/8459 = 63%, 169 KB/s], Decompressed: 5375
Downloaded: 5426 file(s) [attempted 5426/8459 = 64%, 365 KB/s], Decompressed: 5419
Downloaded: 5467 file(s) [attempted 5467/8459 = 64%, 773 KB/s], Decompressed: 5457
Downloaded: 5505 file(s) [attempted 5505/8459 = 65%, 30 KB/s], Decompressed: 5494
Downloaded: 5546 file(s) [attempted 5546/8459 = 65%, 228 KB/s], Decompressed: 5539
Downloaded: 5584 file(s) [attempted 5584/8459 = 66%, 334 KB/s], Decompressed: 5580
Downloaded: 5624 file(s) [attempted 5624/8459 = 66%, 295 KB/s], Decompressed: 5621
Downloaded: 5659 file(s) [attempted 5659/8459 = 66%, 157 KB/s], Decompressed: 5655
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 632 KB/s], Decompressed: 5689
Downloaded: 5737 file(s) [attempted 5737/8459 = 67%, 195 KB/s], Decompressed: 5734
Downloaded: 5778 file(s) [attempted 5778/8459 = 68%, 528 KB/s], Decompressed: 5775
Downloaded: 5816 file(s) [attempted 5816/8459 = 68%, 197 KB/s], Decompressed: 5809
Downloaded: 5854 file(s) [attempted 5854/8459 = 69%, 595 KB/s], Decompressed: 5850
Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 99 KB/s], Decompressed: 5891
Downloaded: 5936 file(s) [attempted 5936/8459 = 70%, 863 KB/s], Decompressed: 5932
Downloaded: 5980 file(s) [attempted 5980/8459 = 70%, 206 KB/s], Decompressed: 5977
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 259 KB/s], Decompressed: 6015
Downloaded: 6056 file(s) [attempted 6056/8459 = 71%, 365 KB/s], Decompressed: 6052
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 528 KB/s], Decompressed: 6093
Downloaded: 6138 file(s) [attempted 6138/8459 = 72%, 144 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 58 KB/s], Decompressed: 6179
Downloaded: 6213 file(s) [attempted 6213/8459 = 73%, 490 KB/s], Decompressed: 6189
Downloaded: 6251 file(s) [attempted 6251/8459 = 73%, 87 KB/s], Decompressed: 6247
Downloaded: 6292 file(s) [attempted 6292/8459 = 74%, 133 KB/s], Decompressed: 6288
Downloaded: 6335 file(s) [attempted 6335/8459 = 74%, 358 KB/s], Decompressed: 6329
Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 180 KB/s], Decompressed: 6367
Downloaded: 6408 file(s) [attempted 6408/8459 = 75%, 212 KB/s], Decompressed: 6405
Downloaded: 6449 file(s) [attempted 6449/8459 = 76%, 243 KB/s], Decompressed: 6446
Downloaded: 6487 file(s) [attempted 6487/8459 = 76%, 295 KB/s], Decompressed: 6483
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 436 KB/s], Decompressed: 6525
Downloaded: 6572 file(s) [attempted 6572/8459 = 77%, 465 KB/s], Decompressed: 6569
Downloaded: 6610 file(s) [attempted 6610/8459 = 78%, 55 KB/s], Decompressed: 6607
Downloaded: 6651 file(s) [attempted 6651/8459 = 78%, 455 KB/s], Decompressed: 6641
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 240 KB/s], Decompressed: 6682
Downloaded: 6727 file(s) [attempted 6727/8459 = 79%, 115 KB/s], Decompressed: 6723
Downloaded: 6768 file(s) [attempted 6768/8459 = 80%, 632 KB/s], Decompressed: 6764
Downloaded: 6809 file(s) [attempted 6809/8459 = 80%, 482 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 219 KB/s], Decompressed: 6836
Downloaded: 6884 file(s) [attempted 6884/8459 = 81%, 154 KB/s], Decompressed: 6880
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 301 KB/s], Decompressed: 6922
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 142 KB/s], Decompressed: 6966
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 65 KB/s], Decompressed: 7011
Downloaded: 7048 file(s) [attempted 7048/8459 = 83%, 323 KB/s], Decompressed: 7045
Downloaded: 7089 file(s) [attempted 7089/8459 = 83%, 1177 KB/s], Decompressed: 7082
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 281 KB/s], Decompressed: 7123
Downloaded: 7171 file(s) [attempted 7171/8459 = 84%, 169 KB/s], Decompressed: 7168
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 58 KB/s], Decompressed: 7212
Downloaded: 7253 file(s) [attempted 7253/8459 = 85%, 166 KB/s], Decompressed: 7250
Downloaded: 7295 file(s) [attempted 7295/8459 = 86%, 35 KB/s], Decompressed: 7288
Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 281 KB/s], Decompressed: 7325
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 437 KB/s], Decompressed: 7366
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 164 KB/s], Decompressed: 7411
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 814 KB/s], Decompressed: 7449
Downloaded: 7496 file(s) [attempted 7496/8459 = 88%, 300 KB/s], Decompressed: 7490
Downloaded: 7534 file(s) [attempted 7534/8459 = 89%, 222 KB/s], Decompressed: 7531
Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 166 KB/s], Decompressed: 7568
Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 490 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8459 = 90%, 468 KB/s], Decompressed: 7654
Downloaded: 7702 file(s) [attempted 7702/8459 = 91%, 417 KB/s], Decompressed: 7695
Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 142 KB/s], Decompressed: 7733
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 112 KB/s], Decompressed: 7777
Downloaded: 7822 file(s) [attempted 7822/8459 = 92%, 691 KB/s], Decompressed: 7808
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 32 KB/s], Decompressed: 7856
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 4062 KB/s], Decompressed: 7897
Downloaded: 7939 file(s) [attempted 7939/8459 = 93%, 87 KB/s], Decompressed: 7928
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 347 KB/s], Decompressed: 7976
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 117 KB/s], Decompressed: 8018
Downloaded: 8056 file(s) [attempted 8056/8459 = 95%, 170 KB/s], Decompressed: 8051
Downloaded: 8095 file(s) [attempted 8095/8459 = 95%, 514 KB/s], Decompressed: 8092
Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 510 KB/s], Decompressed: 8133
Downloaded: 8178 file(s) [attempted 8178/8459 = 96%, 54 KB/s], Decompressed: 8174
Downloaded: 8219 file(s) [attempted 8219/8459 = 97%, 147 KB/s], Decompressed: 8212
Downloaded: 8256 file(s) [attempted 8256/8459 = 97%, 324 KB/s], Decompressed: 8253
Downloaded: 8294 file(s) [attempted 8294/8459 = 98%, 417 KB/s], Decompressed: 8290
Downloaded: 8335 file(s) [attempted 8335/8459 = 98%, 84 KB/s], Decompressed: 8328
Downloaded: 8377 file(s) [attempted 8377/8459 = 99%, 324 KB/s], Decompressed: 8373
Downloaded: 8417 file(s) [attempted 8417/8459 = 99%, 253 KB/s], Decompressed: 8410
Downloaded: 8451 file(s) [attempted 8451/8459 = 99%, 173 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 173 KB/s], Decompressed: 8451

lean_checker exit 0 duration 3m 42s · created 7/2/2026, 1:44:46 PM

lake build

ℹ [3539/3551] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3571] 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`
⚠ [3697/3705] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3700/3714] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3761/3776] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3762/3776] 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`
⚠ [3876/3895] 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:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [3878/3895] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4012/4022] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4014/4022] 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`
⚠ [4015/4022] 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:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4017/4022] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
⚠ [4052/4064] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (135s)
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`
⚠ [4057/4071] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (33s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4059/4071] 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`
⚠ [4064/4079] 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`
⚠ [4068/4079] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
⚠ [4083/4093] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
⚠ [4088/4130] 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`
⚠ [4108/4140] 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`
⚠ [4109/4140] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4129/4153] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
⚠ [4133/4153] 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`
⚠ [4143/4153] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
ℹ [4145/4153] 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.
✔ [4152/4153] Built PrimeNumberTheoremAnd (12s)
Build completed successfully (4153 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 3m 43s · created 7/2/2026, 1:44:46 PM

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.5s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (540ms)
✔ [33/42] Built Cli:c.o (67ms)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3626/3644] 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`
⚠ [3765/3784] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3785/3800] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3840/3858] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3842/3858] 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`
⚠ [3960/3982] 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:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [3963/3982] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4105/4120] 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`
⚠ [4108/4180] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4110/4180] 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:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4114/4180] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
⚠ [4147/4194] 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`
✔ [4173/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (136s)
⚠ [4174/4202] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4178/4202] 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`
⚠ [4181/4203] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
✔ [4191/4226] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (22s)
⚠ [4195/4226] 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`
⚠ [4218/4302] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
⚠ [4228/4302] 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`
⚠ [4244/4320] 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`
⚠ [4271/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4285/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
⚠ [4304/4342] 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`
ℹ [4325/4342] 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.
⚠ [4337/4342] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4340/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (12s)
ℹ [4341/4343] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4343 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 25m 1s · created 7/2/2026, 1:44:46 PM

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":11,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":443085,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":320,"diagnostic_count":113,"duration_ms":36261,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":406289,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":320,"diagnostic_count":113,"duration_ms":13,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2498619,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2498619,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":790,"diagnostic_count":517,"duration_ms":93057,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":412807,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":790,"diagnostic_count":517,"duration_ms":42,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":5590574,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":5590574,"phase":"lean_module_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":30516}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":7145,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"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":64783,"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 b3eb8b46ebc2eec89f6498d884bdaa414bda45f61bff9c1d776a70b947f592f7
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":1397256,"ok":true}