Verification run
Run 115
succeeded commit
c4bbfd41218a toolchain lean-v4-30-0 prover lean took 31m 33s · finished 3w 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
23%, 334 KB/s], Decompressed: 2014
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 321 KB/s], Decompressed: 2052
Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 69 KB/s], Decompressed: 2089
Downloaded: 2132 file(s) [attempted 2132/8459 = 25%, 904 KB/s], Decompressed: 2123
Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 270 KB/s], Decompressed: 2164
Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 694 KB/s], Decompressed: 2199
Downloaded: 2244 file(s) [attempted 2244/8459 = 26%, 183 KB/s], Decompressed: 2240
Downloaded: 2285 file(s) [attempted 2285/8459 = 27%, 724 KB/s], Decompressed: 2281
Downloaded: 2324 file(s) [attempted 2324/8459 = 27%, 224 KB/s], Decompressed: 2318
Downloaded: 2365 file(s) [attempted 2365/8459 = 27%, 103 KB/s], Decompressed: 2353
Downloaded: 2395 file(s) [attempted 2395/8459 = 28%, 319 KB/s], Decompressed: 2390
Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 187 KB/s], Decompressed: 2431
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 43 KB/s], Decompressed: 2472
Downloaded: 2519 file(s) [attempted 2519/8459 = 29%, 221 KB/s], Decompressed: 2514
Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 209 KB/s], Decompressed: 2555
Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 37 KB/s], Decompressed: 2589
Downloaded: 2638 file(s) [attempted 2638/8459 = 31%, 91 KB/s], Decompressed: 2630
Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 399 KB/s], Decompressed: 2671
Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 237 KB/s], Decompressed: 2705
Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 200 KB/s], Decompressed: 2750
Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 1786 KB/s], Decompressed: 2787
Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 2145 KB/s], Decompressed: 2833
Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 22 KB/s], Decompressed: 2869
Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 662 KB/s], Decompressed: 2907
Downloaded: 2950 file(s) [attempted 2950/8459 = 34%, 223 KB/s], Decompressed: 2941
Downloaded: 2989 file(s) [attempted 2989/8459 = 35%, 307 KB/s], Decompressed: 2986
Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 426 KB/s], Decompressed: 3027
Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 361 KB/s], Decompressed: 3068
Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 670 KB/s], Decompressed: 3106
Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 51 KB/s], Decompressed: 3143
Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 229 KB/s], Decompressed: 3188
Downloaded: 3230 file(s) [attempted 3230/8459 = 38%, 404 KB/s], Decompressed: 3225
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 252 KB/s], Decompressed: 3266
Downloaded: 3304 file(s) [attempted 3304/8459 = 39%, 640 KB/s], Decompressed: 3297
Downloaded: 3345 file(s) [attempted 3345/8459 = 39%, 1365 KB/s], Decompressed: 3342
Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 611 KB/s], Decompressed: 3380
Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 226 KB/s], Decompressed: 3424
Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 290 KB/s], Decompressed: 3465
Downloaded: 3503 file(s) [attempted 3503/8459 = 41%, 221 KB/s], Decompressed: 3468
Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 326 KB/s], Decompressed: 3468
Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 189 KB/s], Decompressed: 3468
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 201 KB/s], Decompressed: 3468
Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 378 KB/s], Decompressed: 3468
Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 1396 KB/s], Decompressed: 3468
Downloaded: 3681 file(s) [attempted 3681/8459 = 43%, 29 KB/s], Decompressed: 3475
Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 135 KB/s], Decompressed: 3715
Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 869 KB/s], Decompressed: 3746
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 54 KB/s], Decompressed: 3787
Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 100 KB/s], Decompressed: 3824
Downloaded: 3866 file(s) [attempted 3866/8459 = 45%, 343 KB/s], Decompressed: 3862
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 51 KB/s], Decompressed: 3903
Downloaded: 3942 file(s) [attempted 3942/8459 = 46%, 224 KB/s], Decompressed: 3937
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 322 KB/s], Decompressed: 3982
Downloaded: 4024 file(s) [attempted 4024/8459 = 47%, 487 KB/s], Decompressed: 4016
Downloaded: 4058 file(s) [attempted 4058/8459 = 47%, 1874 KB/s], Decompressed: 4050
Downloaded: 4096 file(s) [attempted 4096/8459 = 48%, 788 KB/s], Decompressed: 4091
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 55 KB/s], Decompressed: 4132
Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 452 KB/s], Decompressed: 4180
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 151 KB/s], Decompressed: 4225
Downloaded: 4266 file(s) [attempted 4266/8459 = 50%, 70 KB/s], Decompressed: 4262
Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 660 KB/s], Decompressed: 4297
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 62 KB/s], Decompressed: 4334
Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 836 KB/s], Decompressed: 4379
Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 112 KB/s], Decompressed: 4427
Downloaded: 4465 file(s) [attempted 4465/8459 = 52%, 134 KB/s], Decompressed: 4457
Downloaded: 4500 file(s) [attempted 4500/8459 = 53%, 175 KB/s], Decompressed: 4495
Downloaded: 4540 file(s) [attempted 4540/8459 = 53%, 22 KB/s], Decompressed: 4533
Downloaded: 4579 file(s) [attempted 4579/8459 = 54%, 494 KB/s], Decompressed: 4574
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 205 KB/s], Decompressed: 4611
Downloaded: 4654 file(s) [attempted 4654/8459 = 55%, 35 KB/s], Decompressed: 4649
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 336 KB/s], Decompressed: 4687
Downloaded: 4735 file(s) [attempted 4735/8459 = 55%, 539 KB/s], Decompressed: 4728
Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 468 KB/s], Decompressed: 4769
Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 233 KB/s], Decompressed: 4807
Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 61 KB/s], Decompressed: 4851
Downloaded: 4889 file(s) [attempted 4889/8459 = 57%, 124 KB/s], Decompressed: 4885
Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 507 KB/s], Decompressed: 4926
Downloaded: 4971 file(s) [attempted 4971/8459 = 58%, 161 KB/s], Decompressed: 4964
Downloaded: 5013 file(s) [attempted 5013/8459 = 59%, 86 KB/s], Decompressed: 5008
Downloaded: 5047 file(s) [attempted 5047/8459 = 59%, 491 KB/s], Decompressed: 5039
Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 227 KB/s], Decompressed: 5080
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 300 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 394 KB/s], Decompressed: 5159
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 93 KB/s], Decompressed: 5193
Downloaded: 5240 file(s) [attempted 5240/8459 = 61%, 1585 KB/s], Decompressed: 5231
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 256 KB/s], Decompressed: 5269
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 451 KB/s], Decompressed: 5313
Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 169 KB/s], Decompressed: 5351
Downloaded: 5392 file(s) [attempted 5392/8459 = 63%, 68 KB/s], Decompressed: 5388
Downloaded: 5430 file(s) [attempted 5430/8459 = 64%, 187 KB/s], Decompressed: 5426
Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 23 KB/s], Decompressed: 5467
Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 342 KB/s], Decompressed: 5501
Downloaded: 5550 file(s) [attempted 5550/8459 = 65%, 215 KB/s], Decompressed: 5542
Downloaded: 5587 file(s) [attempted 5587/8459 = 66%, 149 KB/s], Decompressed: 5573
Downloaded: 5628 file(s) [attempted 5628/8459 = 66%, 1097 KB/s], Decompressed: 5624
Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 2235 KB/s], Decompressed: 5666
Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 575 KB/s], Decompressed: 5703
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 246 KB/s], Decompressed: 5737
Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 294 KB/s], Decompressed: 5778
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 364 KB/s], Decompressed: 5823
Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 166 KB/s], Decompressed: 5864
Downloaded: 5908 file(s) [attempted 5908/8459 = 69%, 448 KB/s], Decompressed: 5898
Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 102 KB/s], Decompressed: 5943
Downloaded: 5986 file(s) [attempted 5986/8459 = 70%, 1518 KB/s], Decompressed: 5981
Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 279 KB/s], Decompressed: 6018
Downloaded: 6064 file(s) [attempted 6064/8459 = 71%, 982 KB/s], Decompressed: 6060
Downloaded: 6098 file(s) [attempted 6098/8459 = 72%, 1773 KB/s], Decompressed: 6093
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 223 KB/s], Decompressed: 6134
Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 465 KB/s], Decompressed: 6176
Downloaded: 6220 file(s) [attempted 6220/8459 = 73%, 460 KB/s], Decompressed: 6217
Downloaded: 6263 file(s) [attempted 6263/8459 = 74%, 325 KB/s], Decompressed: 6254
Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 787 KB/s], Decompressed: 6292
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 798 KB/s], Decompressed: 6329
Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 499 KB/s], Decompressed: 6364
Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 47 KB/s], Decompressed: 6412
Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 262 KB/s], Decompressed: 6453
Downloaded: 6495 file(s) [attempted 6495/8459 = 76%, 693 KB/s], Decompressed: 6487
Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 85 KB/s], Decompressed: 6531
Downloaded: 6577 file(s) [attempted 6577/8459 = 77%, 391 KB/s], Decompressed: 6572
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 849 KB/s], Decompressed: 6610
Downloaded: 6656 file(s) [attempted 6656/8459 = 78%, 133 KB/s], Decompressed: 6651
Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 263 KB/s], Decompressed: 6682
Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 1000 KB/s], Decompressed: 6723
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 66 KB/s], Decompressed: 6768
Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 230 KB/s], Decompressed: 6812
Downloaded: 6864 file(s) [attempted 6864/8459 = 81%, 197 KB/s], Decompressed: 6860
Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 433 KB/s], Decompressed: 6898
Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 441 KB/s], Decompressed: 6935
Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 534 KB/s], Decompressed: 6973
Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 246 KB/s], Decompressed: 7021
Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 144 KB/s], Decompressed: 7065
Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 576 KB/s], Decompressed: 7103
Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1600 KB/s], Decompressed: 7137
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 102 KB/s], Decompressed: 7175
Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 277 KB/s], Decompressed: 7219
Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 595 KB/s], Decompressed: 7257
Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 83 KB/s], Decompressed: 7298
Downloaded: 7341 file(s) [attempted 7341/8459 = 86%, 973 KB/s], Decompressed: 7332
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 189 KB/s], Decompressed: 7377
Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 23 KB/s], Decompressed: 7418
Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 70 KB/s], Decompressed: 7455
Downloaded: 7503 file(s) [attempted 7503/8459 = 88%, 446 KB/s], Decompressed: 7500
Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 2075 KB/s], Decompressed: 7538
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 150 KB/s], Decompressed: 7575
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 469 KB/s], Decompressed: 7616
Downloaded: 7665 file(s) [attempted 7665/8459 = 90%, 95 KB/s], Decompressed: 7661
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 89 KB/s], Decompressed: 7702
Downloaded: 7740 file(s) [attempted 7740/8459 = 91%, 757 KB/s], Decompressed: 7736
Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 144 KB/s], Decompressed: 7781
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 758 KB/s], Decompressed: 7815
Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 432 KB/s], Decompressed: 7852
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 234 KB/s], Decompressed: 7897
Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 86 KB/s], Decompressed: 7938
Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 661 KB/s], Decompressed: 7969
Downloaded: 8017 file(s) [attempted 8017/8459 = 94%, 186 KB/s], Decompressed: 8013
Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 477 KB/s], Decompressed: 8056
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 101 KB/s], Decompressed: 8089
Downloaded: 8129 file(s) [attempted 8129/8459 = 96%, 153 KB/s], Decompressed: 8123
Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 756 KB/s], Decompressed: 8167
Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 426 KB/s], Decompressed: 8205
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 310 KB/s], Decompressed: 8246
Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 462 KB/s], Decompressed: 8284
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 309 KB/s], Decompressed: 8325
Downloaded: 8370 file(s) [attempted 8370/8459 = 98%, 292 KB/s], Decompressed: 8362
Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 137 KB/s], Decompressed: 8403
Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 178 KB/s], Decompressed: 8441
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 178 KB/s], Decompressed: 8455
$ lake build
exit_code=Some(0) duration_ms=184242
stdout:
ℹ [3472/3493] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3488/3507] 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`
⚠ [3635/3661] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3640/3661] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3702/3721] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3703/3721] 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`
⚠ [3810/3837] 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`
⚠ [3812/3837] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3944/3952] 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`
⚠ [3947/3984] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3949/3984] 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:786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:839:8: declaration uses `sorry`
⚠ [3951/3984] 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`
⚠ [3954/3984] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3955/3984] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [3956/3984] Built LeanCert.Engine.FinSumDyadic (67s)
✔ [3958/3986] Built LeanCert.Engine.WitnessSum (2.7s)
✔ [3959/3987] Built LeanCert.Engine.ReflectiveSum (4.4s)
✔ [3961/3990] Built LeanCert.Examples.BKLNW_a2_reflective (23s)
⚠ [3977/3990] 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`
⚠ [3996/4017] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
⚠ [3999/4017] 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`
⚠ [4000/4017] 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`
⚠ [4005/4017] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4022/4037] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (22s)
⚠ [4028/4048] 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`
⚠ [4030/4048] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4033/4048] 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`
⚠ [4040/4057] 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`
⚠ [4041/4057] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4042/4057] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (9.5s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:90:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:109:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1143:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1272:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1505:8: declaration uses `sorry`
ℹ [4049/4085] 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.
✔ [4139/4140] Built PrimeNumberTheoremAnd (14s)
Build completed successfully (4140 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=79031
stdout:
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (532ms)
✔ [33/57] Built Cli:c.o (65ms)
ℹ [3505/3531] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3522/3547] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3669/3694] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3692/3707] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3754/3774] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3756/3774] 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`
⚠ [3867/3889] 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`
⚠ [3870/3889] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [4011/4084] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4015/4084] 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`
⚠ [4017/4084] 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:786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:839:8: declaration uses `sorry`
⚠ [4021/4084] 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`
⚠ [4025/4084] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [4026/4084] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
⚠ [4057/4090] 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`
⚠ [4087/4114] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
⚠ [4095/4114] 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`
⚠ [4097/4114] 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`
⚠ [4101/4114] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4126/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (4.0s)
⚠ [4133/4174] 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`
⚠ [4137/4174] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4141/4174] 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`
⚠ [4147/4185] 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`
⚠ [4149/4185] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:90:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:109:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1143:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1272:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1505:8: declaration uses `sorry`
✔ [4153/4188] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (21s)
⚠ [4165/4240] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4170/4240] 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.
✔ [4324/4326] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.0s)
ℹ [4325/4327] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (57ms)
info: Blueprint indexing
Build completed successfully (4327 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=1219978
stdout:
apx-semantic-phase {"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":14,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":423602,"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":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":123,"diagnostic_count":45,"duration_ms":10526,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":367085,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":123,"diagnostic_count":45,"duration_ms":21,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.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":1326648,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1326648,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":158,"diagnostic_count":44,"duration_ms":13565,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":378576,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":158,"diagnostic_count":44,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.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":827226,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":827226,"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":5807}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":8438,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":15,"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":6350,"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 4549027b77760e1404ed67d6aaed72896eb4a3738c27b5ed555044a59351fcf5
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":1198426,"ok":true}
Stored Lean workspace build cache
Stored Lean semantic extraction cache
Command runs
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-755-source
Cloning into '/var/lib/apodeixis/repos/job-755-source'...
git_checkout exit 128
git checkout c4bbfd41218a50e91d44828b4b41f73e46c232d5
fatal: reference is not a tree: c4bbfd41218a50e91d44828b4b41f73e46c232d5
git_checkout exit 0
git fetch --depth 1 origin c4bbfd41218a50e91d44828b4b41f73e46c232d5
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd * branch c4bbfd41218a50e91d44828b4b41f73e46c232d5 -> FETCH_HEAD
git_checkout exit 0
git checkout c4bbfd41218a50e91d44828b4b41f73e46c232d5 (after fetch)
Note: switching to 'c4bbfd41218a50e91d44828b4b41f73e46c232d5'. 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 c4bbfd4 Kadiri: prove summable_lap_re_at_zeros from the decay bound and Backlund counting (#1477) (#1522)
lake_cache exit 0
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: 16 file(s) [attempted 16/8459 = 0%, 2 KB/s], Decompressed: 15 Downloaded: 40 file(s) [attempted 40/8459 = 0%, 17 KB/s], Decompressed: 38 Downloaded: 68 file(s) [attempted 68/8459 = 0%, 47 KB/s], Decompressed: 64 Downloaded: 100 file(s) [attempted 100/8459 = 1%, 514 KB/s], Decompressed: 96 Downloaded: 134 file(s) [attempted 134/8459 = 1%, 353 KB/s], Decompressed: 127 Downloaded: 175 file(s) [attempted 175/8459 = 2%, 272 KB/s], Decompressed: 172 Downloaded: 208 file(s) [attempted 208/8459 = 2%, 47 KB/s], Decompressed: 203 Downloaded: 242 file(s) [attempted 242/8459 = 2%, 154 KB/s], Decompressed: 237 Downloaded: 282 file(s) [attempted 282/8459 = 3%, 184 KB/s], Decompressed: 275 Downloaded: 319 file(s) [attempted 319/8459 = 3%, 195 KB/s], Decompressed: 312 Downloaded: 359 file(s) [attempted 359/8459 = 4%, 935 KB/s], Decompressed: 353 Downloaded: 391 file(s) [attempted 391/8459 = 4%, 54 KB/s], Decompressed: 384 Downloaded: 431 file(s) [attempted 431/8459 = 5%, 28 KB/s], Decompressed: 425 Downloaded: 466 file(s) [attempted 466/8459 = 5%, 162 KB/s], Decompressed: 463 Downloaded: 508 file(s) [attempted 508/8459 = 6%, 122 KB/s], Decompressed: 504 Downloaded: 549 file(s) [attempted 549/8459 = 6%, 1255 KB/s], Decompressed: 542 Downloaded: 588 file(s) [attempted 588/8459 = 6%, 360 KB/s], Decompressed: 580 Downloaded: 627 file(s) [attempted 627/8459 = 7%, 344 KB/s], Decompressed: 624 Downloaded: 666 file(s) [attempted 666/8459 = 7%, 61 KB/s], Decompressed: 662 Downloaded: 704 file(s) [attempted 704/8459 = 8%, 234 KB/s], Decompressed: 699 Downloaded: 747 file(s) [attempted 747/8459 = 8%, 226 KB/s], Decompressed: 744 Downloaded: 788 file(s) [attempted 788/8459 = 9%, 100 KB/s], Decompressed: 778 Downloaded: 826 file(s) [attempted 826/8459 = 9%, 519 KB/s], Decompressed: 823 Downloaded: 864 file(s) [attempted 864/8459 = 10%, 559 KB/s], Decompressed: 860 Downloaded: 905 file(s) [attempted 905/8459 = 10%, 46 KB/s], Decompressed: 898 Downloaded: 949 file(s) [attempted 949/8459 = 11%, 180 KB/s], Decompressed: 946 Downloaded: 994 file(s) [attempted 994/8459 = 11%, 150 KB/s], Decompressed: 987 Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 151 KB/s], Decompressed: 1021 Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 39 KB/s], Decompressed: 1052 Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 357 KB/s], Decompressed: 1107 Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 356 KB/s], Decompressed: 1145 Downloaded: 1192 file(s) [attempted 1192/8459 = 14%, 112 KB/s], Decompressed: 1189 Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 275 KB/s], Decompressed: 1223 Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 58 KB/s], Decompressed: 1264 Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 431 KB/s], Decompressed: 1299 Downloaded: 1350 file(s) [attempted 1350/8459 = 15%, 132 KB/s], Decompressed: 1343 Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 442 KB/s], Decompressed: 1384 Downloaded: 1425 file(s) [attempted 1425/8459 = 16%, 642 KB/s], Decompressed: 1418 Downloaded: 1466 file(s) [attempted 1466/8459 = 17%, 186 KB/s], Decompressed: 1463 Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 243 KB/s], Decompressed: 1511 Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 346 KB/s], Decompressed: 1545 Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 180 KB/s], Decompressed: 1589 Downloaded: 1634 file(s) [attempted 1634/8459 = 19%, 1027 KB/s], Decompressed: 1627 Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 119 KB/s], Decompressed: 1668 Downloaded: 1713 file(s) [attempted 1713/8459 = 20%, 210 KB/s], Decompressed: 1709 Downloaded: 1754 file(s) [attempted 1754/8459 = 20%, 956 KB/s], Decompressed: 1747 Downloaded: 1791 file(s) [attempted 1791/8459 = 21%, 918 KB/s], Decompressed: 1785 Downloaded: 1832 file(s) [attempted 1832/8459 = 21%, 1026 KB/s], Decompressed: 1829 Downloaded: 1870 file(s) [attempted 1870/8459 = 22%, 272 KB/s], Decompressed: 1863 Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 236 KB/s], Decompressed: 1904 Downloaded: 1942 file(s) [attempted 1942/8459 = 22%, 157 KB/s], Decompressed: 1939 Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 116 KB/s], Decompressed: 1976 Downloaded: 2018 file(s) [attempted 2018/8459 = 23%, 334 KB/s], Decompressed: 2014 Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 321 KB/s], Decompressed: 2052 Downloaded: 2093 file(s) [attempted 2093/8459 = 24%, 69 KB/s], Decompressed: 2089 Downloaded: 2132 file(s) [attempted 2132/8459 = 25%, 904 KB/s], Decompressed: 2123 Downloaded: 2168 file(s) [attempted 2168/8459 = 25%, 270 KB/s], Decompressed: 2164 Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 694 KB/s], Decompressed: 2199 Downloaded: 2244 file(s) [attempted 2244/8459 = 26%, 183 KB/s], Decompressed: 2240 Downloaded: 2285 file(s) [attempted 2285/8459 = 27%, 724 KB/s], Decompressed: 2281 Downloaded: 2324 file(s) [attempted 2324/8459 = 27%, 224 KB/s], Decompressed: 2318 Downloaded: 2365 file(s) [attempted 2365/8459 = 27%, 103 KB/s], Decompressed: 2353 Downloaded: 2395 file(s) [attempted 2395/8459 = 28%, 319 KB/s], Decompressed: 2390 Downloaded: 2438 file(s) [attempted 2438/8459 = 28%, 187 KB/s], Decompressed: 2431 Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 43 KB/s], Decompressed: 2472 Downloaded: 2519 file(s) [attempted 2519/8459 = 29%, 221 KB/s], Decompressed: 2514 Downloaded: 2558 file(s) [attempted 2558/8459 = 30%, 209 KB/s], Decompressed: 2555 Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 37 KB/s], Decompressed: 2589 Downloaded: 2638 file(s) [attempted 2638/8459 = 31%, 91 KB/s], Decompressed: 2630 Downloaded: 2678 file(s) [attempted 2678/8459 = 31%, 399 KB/s], Decompressed: 2671 Downloaded: 2719 file(s) [attempted 2719/8459 = 32%, 237 KB/s], Decompressed: 2705 Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 200 KB/s], Decompressed: 2750 Downloaded: 2794 file(s) [attempted 2794/8459 = 33%, 1786 KB/s], Decompressed: 2787 Downloaded: 2835 file(s) [attempted 2835/8459 = 33%, 2145 KB/s], Decompressed: 2833 Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 22 KB/s], Decompressed: 2869 Downloaded: 2914 file(s) [attempted 2914/8459 = 34%, 662 KB/s], Decompressed: 2907 Downloaded: 2950 file(s) [attempted 2950/8459 = 34%, 223 KB/s], Decompressed: 2941 Downloaded: 2989 file(s) [attempted 2989/8459 = 35%, 307 KB/s], Decompressed: 2986 Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 426 KB/s], Decompressed: 3027 Downloaded: 3071 file(s) [attempted 3071/8459 = 36%, 361 KB/s], Decompressed: 3068 Downloaded: 3112 file(s) [attempted 3112/8459 = 36%, 670 KB/s], Decompressed: 3106 Downloaded: 3147 file(s) [attempted 3147/8459 = 37%, 51 KB/s], Decompressed: 3143 Downloaded: 3191 file(s) [attempted 3191/8459 = 37%, 229 KB/s], Decompressed: 3188 Downloaded: 3230 file(s) [attempted 3230/8459 = 38%, 404 KB/s], Decompressed: 3225 Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 252 KB/s], Decompressed: 3266 Downloaded: 3304 file(s) [attempted 3304/8459 = 39%, 640 KB/s], Decompressed: 3297 Downloaded: 3345 file(s) [attempted 3345/8459 = 39%, 1365 KB/s], Decompressed: 3342 Downloaded: 3390 file(s) [attempted 3390/8459 = 40%, 611 KB/s], Decompressed: 3380 Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 226 KB/s], Decompressed: 3424 Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 290 KB/s], Decompressed: 3465 Downloaded: 3503 file(s) [attempted 3503/8459 = 41%, 221 KB/s], Decompressed: 3468 Downloaded: 3530 file(s) [attempted 3530/8459 = 41%, 326 KB/s], Decompressed: 3468 Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 189 KB/s], Decompressed: 3468 Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 201 KB/s], Decompressed: 3468 Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 378 KB/s], Decompressed: 3468 Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 1396 KB/s], Decompressed: 3468 Downloaded: 3681 file(s) [attempted 3681/8459 = 43%, 29 KB/s], Decompressed: 3475 Downloaded: 3718 file(s) [attempted 3718/8459 = 43%, 135 KB/s], Decompressed: 3715 Downloaded: 3752 file(s) [attempted 3752/8459 = 44%, 869 KB/s], Decompressed: 3746 Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 54 KB/s], Decompressed: 3787 Downloaded: 3831 file(s) [attempted 3831/8459 = 45%, 100 KB/s], Decompressed: 3824 Downloaded: 3866 file(s) [attempted 3866/8459 = 45%, 343 KB/s], Decompressed: 3862 Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 51 KB/s], Decompressed: 3903 Downloaded: 3942 file(s) [attempted 3942/8459 = 46%, 224 KB/s], Decompressed: 3937 Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 322 KB/s], Decompressed: 3982 Downloaded: 4024 file(s) [attempted 4024/8459 = 47%, 487 KB/s], Decompressed: 4016 Downloaded: 4058 file(s) [attempted 4058/8459 = 47%, 1874 KB/s], Decompressed: 4050 Downloaded: 4096 file(s) [attempted 4096/8459 = 48%, 788 KB/s], Decompressed: 4091 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 55 KB/s], Decompressed: 4132 Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 452 KB/s], Decompressed: 4180 Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 151 KB/s], Decompressed: 4225 Downloaded: 4266 file(s) [attempted 4266/8459 = 50%, 70 KB/s], Decompressed: 4262 Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 660 KB/s], Decompressed: 4297 Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 62 KB/s], Decompressed: 4334 Downloaded: 4382 file(s) [attempted 4382/8459 = 51%, 836 KB/s], Decompressed: 4379 Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 112 KB/s], Decompressed: 4427 Downloaded: 4465 file(s) [attempted 4465/8459 = 52%, 134 KB/s], Decompressed: 4457 Downloaded: 4500 file(s) [attempted 4500/8459 = 53%, 175 KB/s], Decompressed: 4495 Downloaded: 4540 file(s) [attempted 4540/8459 = 53%, 22 KB/s], Decompressed: 4533 Downloaded: 4579 file(s) [attempted 4579/8459 = 54%, 494 KB/s], Decompressed: 4574 Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 205 KB/s], Decompressed: 4611 Downloaded: 4654 file(s) [attempted 4654/8459 = 55%, 35 KB/s], Decompressed: 4649 Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 336 KB/s], Decompressed: 4687 Downloaded: 4735 file(s) [attempted 4735/8459 = 55%, 539 KB/s], Decompressed: 4728 Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 468 KB/s], Decompressed: 4769 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 233 KB/s], Decompressed: 4807 Downloaded: 4854 file(s) [attempted 4854/8459 = 57%, 61 KB/s], Decompressed: 4851 Downloaded: 4889 file(s) [attempted 4889/8459 = 57%, 124 KB/s], Decompressed: 4885 Downloaded: 4930 file(s) [attempted 4930/8459 = 58%, 507 KB/s], Decompressed: 4926 Downloaded: 4971 file(s) [attempted 4971/8459 = 58%, 161 KB/s], Decompressed: 4964 Downloaded: 5013 file(s) [attempted 5013/8459 = 59%, 86 KB/s], Decompressed: 5008 Downloaded: 5047 file(s) [attempted 5047/8459 = 59%, 491 KB/s], Decompressed: 5039 Downloaded: 5084 file(s) [attempted 5084/8459 = 60%, 227 KB/s], Decompressed: 5080 Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 300 KB/s], Decompressed: 5121 Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 394 KB/s], Decompressed: 5159 Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 93 KB/s], Decompressed: 5193 Downloaded: 5240 file(s) [attempted 5240/8459 = 61%, 1585 KB/s], Decompressed: 5231 Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 256 KB/s], Decompressed: 5269 Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 451 KB/s], Decompressed: 5313 Downloaded: 5354 file(s) [attempted 5354/8459 = 63%, 169 KB/s], Decompressed: 5351 Downloaded: 5392 file(s) [attempted 5392/8459 = 63%, 68 KB/s], Decompressed: 5388 Downloaded: 5430 file(s) [attempted 5430/8459 = 64%, 187 KB/s], Decompressed: 5426 Downloaded: 5470 file(s) [attempted 5470/8459 = 64%, 23 KB/s], Decompressed: 5467 Downloaded: 5511 file(s) [attempted 5511/8459 = 65%, 342 KB/s], Decompressed: 5501 Downloaded: 5550 file(s) [attempted 5550/8459 = 65%, 215 KB/s], Decompressed: 5542 Downloaded: 5587 file(s) [attempted 5587/8459 = 66%, 149 KB/s], Decompressed: 5573 Downloaded: 5628 file(s) [attempted 5628/8459 = 66%, 1097 KB/s], Decompressed: 5624 Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 2235 KB/s], Decompressed: 5666 Downloaded: 5707 file(s) [attempted 5707/8459 = 67%, 575 KB/s], Decompressed: 5703 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 246 KB/s], Decompressed: 5737 Downloaded: 5782 file(s) [attempted 5782/8459 = 68%, 294 KB/s], Decompressed: 5778 Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 364 KB/s], Decompressed: 5823 Downloaded: 5867 file(s) [attempted 5867/8459 = 69%, 166 KB/s], Decompressed: 5864 Downloaded: 5908 file(s) [attempted 5908/8459 = 69%, 448 KB/s], Decompressed: 5898 Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 102 KB/s], Decompressed: 5943 Downloaded: 5986 file(s) [attempted 5986/8459 = 70%, 1518 KB/s], Decompressed: 5981 Downloaded: 6021 file(s) [attempted 6021/8459 = 71%, 279 KB/s], Decompressed: 6018 Downloaded: 6064 file(s) [attempted 6064/8459 = 71%, 982 KB/s], Decompressed: 6060 Downloaded: 6098 file(s) [attempted 6098/8459 = 72%, 1773 KB/s], Decompressed: 6093 Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 223 KB/s], Decompressed: 6134 Downloaded: 6179 file(s) [attempted 6179/8459 = 73%, 465 KB/s], Decompressed: 6176 Downloaded: 6220 file(s) [attempted 6220/8459 = 73%, 460 KB/s], Decompressed: 6217 Downloaded: 6263 file(s) [attempted 6263/8459 = 74%, 325 KB/s], Decompressed: 6254 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 787 KB/s], Decompressed: 6292 Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 798 KB/s], Decompressed: 6329 Downloaded: 6374 file(s) [attempted 6374/8459 = 75%, 499 KB/s], Decompressed: 6364 Downloaded: 6415 file(s) [attempted 6415/8459 = 75%, 47 KB/s], Decompressed: 6412 Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 262 KB/s], Decompressed: 6453 Downloaded: 6495 file(s) [attempted 6495/8459 = 76%, 693 KB/s], Decompressed: 6487 Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 85 KB/s], Decompressed: 6531 Downloaded: 6577 file(s) [attempted 6577/8459 = 77%, 391 KB/s], Decompressed: 6572 Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 849 KB/s], Decompressed: 6610 Downloaded: 6656 file(s) [attempted 6656/8459 = 78%, 133 KB/s], Decompressed: 6651 Downloaded: 6692 file(s) [attempted 6692/8459 = 79%, 263 KB/s], Decompressed: 6682 Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 1000 KB/s], Decompressed: 6723 Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 66 KB/s], Decompressed: 6768 Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 230 KB/s], Decompressed: 6812 Downloaded: 6864 file(s) [attempted 6864/8459 = 81%, 197 KB/s], Decompressed: 6860 Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 433 KB/s], Decompressed: 6898 Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 441 KB/s], Decompressed: 6935 Downloaded: 6976 file(s) [attempted 6976/8459 = 82%, 534 KB/s], Decompressed: 6973 Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 246 KB/s], Decompressed: 7021 Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 144 KB/s], Decompressed: 7065 Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 576 KB/s], Decompressed: 7103 Downloaded: 7141 file(s) [attempted 7141/8459 = 84%, 1600 KB/s], Decompressed: 7137 Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 102 KB/s], Decompressed: 7175 Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 277 KB/s], Decompressed: 7219 Downloaded: 7267 file(s) [attempted 7267/8459 = 85%, 595 KB/s], Decompressed: 7257 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 83 KB/s], Decompressed: 7298 Downloaded: 7341 file(s) [attempted 7341/8459 = 86%, 973 KB/s], Decompressed: 7332 Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 189 KB/s], Decompressed: 7377 Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 23 KB/s], Decompressed: 7418 Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 70 KB/s], Decompressed: 7455 Downloaded: 7503 file(s) [attempted 7503/8459 = 88%, 446 KB/s], Decompressed: 7500 Downloaded: 7541 file(s) [attempted 7541/8459 = 89%, 2075 KB/s], Decompressed: 7538 Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 150 KB/s], Decompressed: 7575 Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 469 KB/s], Decompressed: 7616 Downloaded: 7665 file(s) [attempted 7665/8459 = 90%, 95 KB/s], Decompressed: 7661 Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 89 KB/s], Decompressed: 7702 Downloaded: 7740 file(s) [attempted 7740/8459 = 91%, 757 KB/s], Decompressed: 7736 Downloaded: 7784 file(s) [attempted 7784/8459 = 92%, 144 KB/s], Decompressed: 7781 Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 758 KB/s], Decompressed: 7815 Downloaded: 7863 file(s) [attempted 7863/8459 = 92%, 432 KB/s], Decompressed: 7852 Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 234 KB/s], Decompressed: 7897 Downloaded: 7941 file(s) [attempted 7941/8459 = 93%, 86 KB/s], Decompressed: 7938 Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 661 KB/s], Decompressed: 7969 Downloaded: 8017 file(s) [attempted 8017/8459 = 94%, 186 KB/s], Decompressed: 8013 Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 477 KB/s], Decompressed: 8056 Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 101 KB/s], Decompressed: 8089 Downloaded: 8129 file(s) [attempted 8129/8459 = 96%, 153 KB/s], Decompressed: 8123 Downloaded: 8171 file(s) [attempted 8171/8459 = 96%, 756 KB/s], Decompressed: 8167 Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 426 KB/s], Decompressed: 8205 Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 310 KB/s], Decompressed: 8246 Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 462 KB/s], Decompressed: 8284 Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 309 KB/s], Decompressed: 8325 Downloaded: 8370 file(s) [attempted 8370/8459 = 98%, 292 KB/s], Decompressed: 8362 Downloaded: 8407 file(s) [attempted 8407/8459 = 99%, 137 KB/s], Decompressed: 8403 Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 178 KB/s], Decompressed: 8441 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 178 KB/s], Decompressed: 8455
lean_checker exit 0
lake build
ℹ [3472/3493] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3488/3507] 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`
⚠ [3635/3661] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3640/3661] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3702/3721] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3703/3721] 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`
⚠ [3810/3837] 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`
⚠ [3812/3837] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3944/3952] 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`
⚠ [3947/3984] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3949/3984] 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:786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:839:8: declaration uses `sorry`
⚠ [3951/3984] 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`
⚠ [3954/3984] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3955/3984] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [3956/3984] Built LeanCert.Engine.FinSumDyadic (67s)
✔ [3958/3986] Built LeanCert.Engine.WitnessSum (2.7s)
✔ [3959/3987] Built LeanCert.Engine.ReflectiveSum (4.4s)
✔ [3961/3990] Built LeanCert.Examples.BKLNW_a2_reflective (23s)
⚠ [3977/3990] 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`
⚠ [3996/4017] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
⚠ [3999/4017] 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`
⚠ [4000/4017] 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`
⚠ [4005/4017] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4022/4037] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (22s)
⚠ [4028/4048] 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`
⚠ [4030/4048] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4033/4048] 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`
⚠ [4040/4057] 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`
⚠ [4041/4057] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4042/4057] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (9.5s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:90:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:109:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1143:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1272:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1505:8: declaration uses `sorry`
ℹ [4049/4085] 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.
✔ [4139/4140] Built PrimeNumberTheoremAnd (14s)
Build completed successfully (4140 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
lake build :blueprint
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (532ms)
✔ [33/57] Built Cli:c.o (65ms)
ℹ [3505/3531] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3522/3547] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3669/3694] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3692/3707] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3754/3774] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3756/3774] 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`
⚠ [3867/3889] 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`
⚠ [3870/3889] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [4011/4084] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4015/4084] 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`
⚠ [4017/4084] 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:786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:839:8: declaration uses `sorry`
⚠ [4021/4084] 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`
⚠ [4025/4084] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [4026/4084] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
⚠ [4057/4090] 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`
⚠ [4087/4114] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
⚠ [4095/4114] 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`
⚠ [4097/4114] 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`
⚠ [4101/4114] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4126/4154] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (4.0s)
⚠ [4133/4174] 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`
⚠ [4137/4174] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4141/4174] 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`
⚠ [4147/4185] 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`
⚠ [4149/4185] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:90:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:109:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1143:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1272:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1505:8: declaration uses `sorry`
✔ [4153/4188] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (21s)
⚠ [4165/4240] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4170/4240] 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.
✔ [4324/4326] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.0s)
ℹ [4325/4327] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (57ms)
info: Blueprint indexing
Build completed successfully (4327 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
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
apx-semantic-phase {"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":14,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":423602,"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":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":123,"diagnostic_count":45,"duration_ms":10526,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":367085,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":123,"diagnostic_count":45,"duration_ms":21,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.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":1326648,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1326648,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":158,"diagnostic_count":44,"duration_ms":13565,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":378576,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":158,"diagnostic_count":44,"duration_ms":5,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.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":827226,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":827226,"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":5807}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":8438,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":15,"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":6350,"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 4549027b77760e1404ed67d6aaed72896eb4a3738c27b5ed555044a59351fcf5
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":1198426,"ok":true}