Run 116

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

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

git checkout b325f1e76153489dfa7a16f6f59e76fcac48130d

fatal: reference is not a tree: b325f1e76153489dfa7a16f6f59e76fcac48130d

git fetch --depth 1 origin b325f1e76153489dfa7a16f6f59e76fcac48130d

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

git checkout b325f1e76153489dfa7a16f6f59e76fcac48130d (after fetch)

Note: switching to 'b325f1e76153489dfa7a16f6f59e76fcac48130d'.

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 b325f1e BKLNW: align thm_14 and thm_16 statements and definitions with the papers (#1523)

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%, 4 KB/s], Decompressed: 15
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 13 KB/s], Decompressed: 34
Downloaded: 64 file(s) [attempted 64/8459 = 0%, 331 KB/s], Decompressed: 63
Downloaded: 89 file(s) [attempted 89/8459 = 1%, 278 KB/s], Decompressed: 86
Downloaded: 121 file(s) [attempted 121/8459 = 1%, 162 KB/s], Decompressed: 114
Downloaded: 148 file(s) [attempted 148/8459 = 1%, 209 KB/s], Decompressed: 145
Downloaded: 186 file(s) [attempted 186/8459 = 2%, 241 KB/s], Decompressed: 175
Downloaded: 223 file(s) [attempted 223/8459 = 2%, 265 KB/s], Decompressed: 210
Downloaded: 261 file(s) [attempted 261/8459 = 3%, 37 KB/s], Decompressed: 210
Downloaded: 302 file(s) [attempted 302/8459 = 3%, 90 KB/s], Decompressed: 288
Downloaded: 336 file(s) [attempted 336/8459 = 3%, 181 KB/s], Decompressed: 333
Downloaded: 375 file(s) [attempted 375/8459 = 4%, 108 KB/s], Decompressed: 371
Downloaded: 412 file(s) [attempted 412/8459 = 4%, 302 KB/s], Decompressed: 408
Downloaded: 456 file(s) [attempted 456/8459 = 5%, 169 KB/s], Decompressed: 439
Downloaded: 497 file(s) [attempted 497/8459 = 5%, 57 KB/s], Decompressed: 490
Downloaded: 532 file(s) [attempted 532/8459 = 6%, 323 KB/s], Decompressed: 514
Downloaded: 569 file(s) [attempted 569/8459 = 6%, 226 KB/s], Decompressed: 566
Downloaded: 610 file(s) [attempted 610/8459 = 7%, 150 KB/s], Decompressed: 593
Downloaded: 655 file(s) [attempted 655/8459 = 7%, 377 KB/s], Decompressed: 651
Downloaded: 696 file(s) [attempted 696/8459 = 8%, 101 KB/s], Decompressed: 693
Downloaded: 732 file(s) [attempted 732/8459 = 8%, 532 KB/s], Decompressed: 723
Downloaded: 771 file(s) [attempted 771/8459 = 9%, 1120 KB/s], Decompressed: 765
Downloaded: 812 file(s) [attempted 812/8459 = 9%, 222 KB/s], Decompressed: 809
Downloaded: 857 file(s) [attempted 857/8459 = 10%, 196 KB/s], Decompressed: 850
Downloaded: 898 file(s) [attempted 898/8459 = 10%, 149 KB/s], Decompressed: 895
Downloaded: 932 file(s) [attempted 932/8459 = 11%, 444 KB/s], Decompressed: 915
Downloaded: 970 file(s) [attempted 970/8459 = 11%, 102 KB/s], Decompressed: 967
Downloaded: 1011 file(s) [attempted 1011/8459 = 11%, 172 KB/s], Decompressed: 1008
Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 1891 KB/s], Decompressed: 1038
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 629 KB/s], Decompressed: 1090
Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 476 KB/s], Decompressed: 1124
Downloaded: 1169 file(s) [attempted 1169/8459 = 13%, 89 KB/s], Decompressed: 1162
Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 100 KB/s], Decompressed: 1192
Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 193 KB/s], Decompressed: 1244
Downloaded: 1281 file(s) [attempted 1281/8459 = 15%, 198 KB/s], Decompressed: 1275
Downloaded: 1319 file(s) [attempted 1319/8459 = 15%, 396 KB/s], Decompressed: 1312
Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 65 KB/s], Decompressed: 1353
Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 40 KB/s], Decompressed: 1394
Downloaded: 1439 file(s) [attempted 1439/8459 = 17%, 61 KB/s], Decompressed: 1429
Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 243 KB/s], Decompressed: 1470
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 984 KB/s], Decompressed: 1507
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 246 KB/s], Decompressed: 1545
Downloaded: 1589 file(s) [attempted 1589/8459 = 18%, 169 KB/s], Decompressed: 1586
Downloaded: 1627 file(s) [attempted 1627/8459 = 19%, 77 KB/s], Decompressed: 1620
Downloaded: 1665 file(s) [attempted 1665/8459 = 19%, 437 KB/s], Decompressed: 1661
Downloaded: 1703 file(s) [attempted 1703/8459 = 20%, 116 KB/s], Decompressed: 1699
Downloaded: 1741 file(s) [attempted 1741/8459 = 20%, 302 KB/s], Decompressed: 1733
Downloaded: 1780 file(s) [attempted 1780/8459 = 21%, 550 KB/s], Decompressed: 1774
Downloaded: 1819 file(s) [attempted 1819/8459 = 21%, 626 KB/s], Decompressed: 1812
Downloaded: 1856 file(s) [attempted 1856/8459 = 21%, 386 KB/s], Decompressed: 1853
Downloaded: 1894 file(s) [attempted 1894/8459 = 22%, 43 KB/s], Decompressed: 1887
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 72 KB/s], Decompressed: 1918
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 169 KB/s], Decompressed: 1959
Downloaded: 2010 file(s) [attempted 2010/8459 = 23%, 377 KB/s], Decompressed: 2007
Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 91 KB/s], Decompressed: 2048
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 284 KB/s], Decompressed: 2082
Downloaded: 2128 file(s) [attempted 2128/8459 = 25%, 931 KB/s], Decompressed: 2123
Downloaded: 2169 file(s) [attempted 2169/8459 = 25%, 262 KB/s], Decompressed: 2164
Downloaded: 2206 file(s) [attempted 2206/8459 = 26%, 410 KB/s], Decompressed: 2195
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 198 KB/s], Decompressed: 2236
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 131 KB/s], Decompressed: 2277
Downloaded: 2318 file(s) [attempted 2318/8459 = 27%, 36 KB/s], Decompressed: 2305
Downloaded: 2356 file(s) [attempted 2356/8459 = 27%, 1767 KB/s], Decompressed: 2353
Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 85 KB/s], Decompressed: 2390
Downloaded: 2439 file(s) [attempted 2439/8459 = 28%, 190 KB/s], Decompressed: 2431
Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 446 KB/s], Decompressed: 2462
Downloaded: 2510 file(s) [attempted 2510/8459 = 29%, 47 KB/s], Decompressed: 2507
Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 66 KB/s], Decompressed: 2544
Downloaded: 2596 file(s) [attempted 2596/8459 = 30%, 37 KB/s], Decompressed: 2592
Downloaded: 2644 file(s) [attempted 2644/8459 = 31%, 393 KB/s], Decompressed: 2637
Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 333 KB/s], Decompressed: 2674
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 1173 KB/s], Decompressed: 2705
Downloaded: 2756 file(s) [attempted 2756/8459 = 32%, 97 KB/s], Decompressed: 2750
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 79 KB/s], Decompressed: 2794
Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 75 KB/s], Decompressed: 2839
Downloaded: 2880 file(s) [attempted 2880/8459 = 34%, 36 KB/s], Decompressed: 2863
Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 126 KB/s], Decompressed: 2869
Downloaded: 2958 file(s) [attempted 2958/8459 = 34%, 1224 KB/s], Decompressed: 2869
Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 97 KB/s], Decompressed: 2979
Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 118 KB/s], Decompressed: 3034
Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 764 KB/s], Decompressed: 3071
Downloaded: 3119 file(s) [attempted 3119/8459 = 36%, 36 KB/s], Decompressed: 3112
Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 518 KB/s], Decompressed: 3153
Downloaded: 3196 file(s) [attempted 3196/8459 = 37%, 187 KB/s], Decompressed: 3191
Downloaded: 3236 file(s) [attempted 3236/8459 = 38%, 377 KB/s], Decompressed: 3229
Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 558 KB/s], Decompressed: 3266
Downloaded: 3314 file(s) [attempted 3314/8459 = 39%, 277 KB/s], Decompressed: 3311
Downloaded: 3359 file(s) [attempted 3359/8459 = 39%, 351 KB/s], Decompressed: 3352
Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 50 KB/s], Decompressed: 3393
Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 108 KB/s], Decompressed: 3427
Downloaded: 3472 file(s) [attempted 3472/8459 = 41%, 47 KB/s], Decompressed: 3468
Downloaded: 3516 file(s) [attempted 3516/8459 = 41%, 272 KB/s], Decompressed: 3513
Downloaded: 3561 file(s) [attempted 3561/8459 = 42%, 226 KB/s], Decompressed: 3557
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 374 KB/s], Decompressed: 3592
Downloaded: 3633 file(s) [attempted 3633/8459 = 42%, 332 KB/s], Decompressed: 3629
Downloaded: 3668 file(s) [attempted 3668/8459 = 43%, 99 KB/s], Decompressed: 3663
Downloaded: 3715 file(s) [attempted 3715/8459 = 43%, 239 KB/s], Decompressed: 3711
Downloaded: 3763 file(s) [attempted 3763/8459 = 44%, 58 KB/s], Decompressed: 3759
Downloaded: 3804 file(s) [attempted 3804/8459 = 44%, 48 KB/s], Decompressed: 3783
Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 558 KB/s], Decompressed: 3838
Downloaded: 3878 file(s) [attempted 3878/8459 = 45%, 113 KB/s], Decompressed: 3865
Downloaded: 3913 file(s) [attempted 3913/8459 = 46%, 131 KB/s], Decompressed: 3906
Downloaded: 3960 file(s) [attempted 3960/8459 = 46%, 277 KB/s], Decompressed: 3951
Downloaded: 3995 file(s) [attempted 3995/8459 = 47%, 122 KB/s], Decompressed: 3992
Downloaded: 4033 file(s) [attempted 4033/8459 = 47%, 940 KB/s], Decompressed: 4019
Downloaded: 4064 file(s) [attempted 4064/8459 = 48%, 612 KB/s], Decompressed: 4060
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 431 KB/s], Decompressed: 4102
Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 35 KB/s], Decompressed: 4143
Downloaded: 4187 file(s) [attempted 4187/8459 = 49%, 319 KB/s], Decompressed: 4180
Downloaded: 4218 file(s) [attempted 4218/8459 = 49%, 292 KB/s], Decompressed: 4214
Downloaded: 4256 file(s) [attempted 4256/8459 = 50%, 310 KB/s], Decompressed: 4252
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 656 KB/s], Decompressed: 4293
Downloaded: 4339 file(s) [attempted 4339/8459 = 51%, 67 KB/s], Decompressed: 4334
Downloaded: 4375 file(s) [attempted 4375/8459 = 51%, 657 KB/s], Decompressed: 4368
Downloaded: 4410 file(s) [attempted 4410/8459 = 52%, 394 KB/s], Decompressed: 4406
Downloaded: 4451 file(s) [attempted 4451/8459 = 52%, 25 KB/s], Decompressed: 4447
Downloaded: 4488 file(s) [attempted 4488/8459 = 53%, 212 KB/s], Decompressed: 4485
Downloaded: 4533 file(s) [attempted 4533/8459 = 53%, 940 KB/s], Decompressed: 4529
Downloaded: 4570 file(s) [attempted 4570/8459 = 54%, 240 KB/s], Decompressed: 4567
Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 341 KB/s], Decompressed: 4605
Downloaded: 4653 file(s) [attempted 4653/8459 = 55%, 269 KB/s], Decompressed: 4646
Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 56 KB/s], Decompressed: 4680
Downloaded: 4728 file(s) [attempted 4728/8459 = 55%, 36 KB/s], Decompressed: 4724
Downloaded: 4769 file(s) [attempted 4769/8459 = 56%, 358 KB/s], Decompressed: 4765
Downloaded: 4811 file(s) [attempted 4811/8459 = 56%, 191 KB/s], Decompressed: 4807
Downloaded: 4844 file(s) [attempted 4844/8459 = 57%, 308 KB/s], Decompressed: 4837
Downloaded: 4885 file(s) [attempted 4885/8459 = 57%, 1058 KB/s], Decompressed: 4878
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 147 KB/s], Decompressed: 4919
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 127 KB/s], Decompressed: 4964
Downloaded: 5012 file(s) [attempted 5012/8459 = 59%, 230 KB/s], Decompressed: 5011
Downloaded: 5045 file(s) [attempted 5045/8459 = 59%, 160 KB/s], Decompressed: 5039
Downloaded: 5082 file(s) [attempted 5082/8459 = 60%, 107 KB/s], Decompressed: 5073
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 47 KB/s], Decompressed: 5118
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 872 KB/s], Decompressed: 5162
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 437 KB/s], Decompressed: 5190
Downloaded: 5242 file(s) [attempted 5242/8459 = 61%, 73 KB/s], Decompressed: 5238
Downloaded: 5272 file(s) [attempted 5272/8459 = 62%, 430 KB/s], Decompressed: 5269
Downloaded: 5316 file(s) [attempted 5316/8459 = 62%, 1217 KB/s], Decompressed: 5313
Downloaded: 5359 file(s) [attempted 5359/8459 = 63%, 161 KB/s], Decompressed: 5351
Downloaded: 5395 file(s) [attempted 5395/8459 = 63%, 536 KB/s], Decompressed: 5392
Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 481 KB/s], Decompressed: 5419
Downloaded: 5484 file(s) [attempted 5484/8459 = 64%, 149 KB/s], Decompressed: 5470
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 170 KB/s], Decompressed: 5515
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 302 KB/s], Decompressed: 5553
Downloaded: 5597 file(s) [attempted 5597/8459 = 66%, 165 KB/s], Decompressed: 5594
Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 220 KB/s], Decompressed: 5638
Downloaded: 5679 file(s) [attempted 5679/8459 = 67%, 54 KB/s], Decompressed: 5672
Downloaded: 5718 file(s) [attempted 5718/8459 = 67%, 168 KB/s], Decompressed: 5713
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 812 KB/s], Decompressed: 5748
Downloaded: 5796 file(s) [attempted 5796/8459 = 68%, 88 KB/s], Decompressed: 5792
Downloaded: 5842 file(s) [attempted 5842/8459 = 69%, 141 KB/s], Decompressed: 5837
Downloaded: 5881 file(s) [attempted 5881/8459 = 69%, 208 KB/s], Decompressed: 5878
Downloaded: 5922 file(s) [attempted 5922/8459 = 70%, 28 KB/s], Decompressed: 5919
Downloaded: 5956 file(s) [attempted 5956/8459 = 70%, 550 KB/s], Decompressed: 5946
Downloaded: 5998 file(s) [attempted 5998/8459 = 70%, 54 KB/s], Decompressed: 5994
Downloaded: 6042 file(s) [attempted 6042/8459 = 71%, 612 KB/s], Decompressed: 6028
Downloaded: 6083 file(s) [attempted 6083/8459 = 71%, 236 KB/s], Decompressed: 6028
Downloaded: 6117 file(s) [attempted 6117/8459 = 72%, 131 KB/s], Decompressed: 6032
Downloaded: 6155 file(s) [attempted 6155/8459 = 72%, 46 KB/s], Decompressed: 6148
Downloaded: 6193 file(s) [attempted 6193/8459 = 73%, 911 KB/s], Decompressed: 6189
Downloaded: 6234 file(s) [attempted 6234/8459 = 73%, 943 KB/s], Decompressed: 6231
Downloaded: 6271 file(s) [attempted 6271/8459 = 74%, 233 KB/s], Decompressed: 6264
Downloaded: 6309 file(s) [attempted 6309/8459 = 74%, 140 KB/s], Decompressed: 6299
Downloaded: 6342 file(s) [attempted 6342/8459 = 74%, 206 KB/s], Decompressed: 6336
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 120 KB/s], Decompressed: 6374
Downloaded: 6425 file(s) [attempted 6425/8459 = 75%, 142 KB/s], Decompressed: 6422
Downloaded: 6463 file(s) [attempted 6463/8459 = 76%, 131 KB/s], Decompressed: 6432
Downloaded: 6504 file(s) [attempted 6504/8459 = 76%, 54 KB/s], Decompressed: 6432
Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 509 KB/s], Decompressed: 6456
Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 430 KB/s], Decompressed: 6579
Downloaded: 6624 file(s) [attempted 6624/8459 = 78%, 527 KB/s], Decompressed: 6620
Downloaded: 6663 file(s) [attempted 6663/8459 = 78%, 80 KB/s], Decompressed: 6651
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 1354 KB/s], Decompressed: 6692
Downloaded: 6737 file(s) [attempted 6737/8459 = 79%, 750 KB/s], Decompressed: 6730
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 140 KB/s], Decompressed: 6771
Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 982 KB/s], Decompressed: 6812
Downloaded: 6853 file(s) [attempted 6853/8459 = 81%, 104 KB/s], Decompressed: 6850
Downloaded: 6890 file(s) [attempted 6890/8459 = 81%, 223 KB/s], Decompressed: 6881
Downloaded: 6928 file(s) [attempted 6928/8459 = 81%, 242 KB/s], Decompressed: 6925
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 138 KB/s], Decompressed: 6966
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 136 KB/s], Decompressed: 7007
Downloaded: 7058 file(s) [attempted 7058/8459 = 83%, 292 KB/s], Decompressed: 7055
Downloaded: 7093 file(s) [attempted 7093/8459 = 83%, 94 KB/s], Decompressed: 7086
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 83 KB/s], Decompressed: 7123
Downloaded: 7168 file(s) [attempted 7168/8459 = 84%, 685 KB/s], Decompressed: 7161
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 826 KB/s], Decompressed: 7202
Downloaded: 7247 file(s) [attempted 7247/8459 = 85%, 19 KB/s], Decompressed: 7236
Downloaded: 7283 file(s) [attempted 7283/8459 = 86%, 184 KB/s], Decompressed: 7277
Downloaded: 7322 file(s) [attempted 7322/8459 = 86%, 132 KB/s], Decompressed: 7319
Downloaded: 7357 file(s) [attempted 7357/8459 = 86%, 140 KB/s], Decompressed: 7350
Downloaded: 7397 file(s) [attempted 7397/8459 = 87%, 154 KB/s], Decompressed: 7394
Downloaded: 7439 file(s) [attempted 7439/8459 = 87%, 66 KB/s], Decompressed: 7432
Downloaded: 7476 file(s) [attempted 7476/8459 = 88%, 284 KB/s], Decompressed: 7466
Downloaded: 7517 file(s) [attempted 7517/8459 = 88%, 877 KB/s], Decompressed: 7510
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 50 KB/s], Decompressed: 7541
Downloaded: 7589 file(s) [attempted 7589/8459 = 89%, 148 KB/s], Decompressed: 7582
Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 199 KB/s], Decompressed: 7623
Downloaded: 7668 file(s) [attempted 7668/8459 = 90%, 1223 KB/s], Decompressed: 7657
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 86 KB/s], Decompressed: 7703
Downloaded: 7740 file(s) [attempted 7740/8459 = 91%, 733 KB/s], Decompressed: 7729
Downloaded: 7781 file(s) [attempted 7781/8459 = 91%, 139 KB/s], Decompressed: 7774
Downloaded: 7818 file(s) [attempted 7818/8459 = 92%, 137 KB/s], Decompressed: 7811
Downloaded: 7856 file(s) [attempted 7856/8459 = 92%, 89 KB/s], Decompressed: 7835
Downloaded: 7890 file(s) [attempted 7890/8459 = 93%, 57 KB/s], Decompressed: 7883
Downloaded: 7935 file(s) [attempted 7935/8459 = 93%, 316 KB/s], Decompressed: 7931
Downloaded: 7976 file(s) [attempted 7976/8459 = 94%, 92 KB/s], Decompressed: 7972
Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 240 KB/s], Decompressed: 8013
Downloaded: 8060 file(s) [attempted 8060/8459 = 95%, 182 KB/s], Decompressed: 8048
Downloaded: 8092 file(s) [attempted 8092/8459 = 95%, 351 KB/s], Decompressed: 8078
Downloaded: 8136 file(s) [attempted 8136/8459 = 96%, 298 KB/s], Decompressed: 8109
Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 433 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8459 = 97%, 101 KB/s], Decompressed: 8205
Downloaded: 8249 file(s) [attempted 8249/8459 = 97%, 179 KB/s], Decompressed: 8246
Downloaded: 8290 file(s) [attempted 8290/8459 = 98%, 443 KB/s], Decompressed: 8284
Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 318 KB/s], Decompressed: 8325
Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 273 KB/s], Decompressed: 8366
Downloaded: 8409 file(s) [attempted 8409/8459 = 99%, 432 KB/s], Decompressed: 8400
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 107 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 107 KB/s], Decompressed: 8448

lake build

ℹ [3472/3483] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3494/3512] 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`
⚠ [3628/3645] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3639/3645] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3703/3723] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3704/3723] 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/3824] 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/3824] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3946/3955] 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`
⚠ [3949/3956] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3950/3956] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (86s)
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:803:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:856:8: declaration uses `sorry`
⚠ [3953/3984] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (28s)
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 (3.1s)
✔ [3958/3986] Built LeanCert.Engine.WitnessSum (2.7s)
✔ [3959/3987] Built LeanCert.Engine.ReflectiveSum (4.1s)
✔ [3961/3987] Built LeanCert.Examples.BKLNW_a2_reflective (20s)
✔ [3964/3989] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.4s)
✔ [3966/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.9s)
⚠ [3967/3994] 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`
✔ [3968/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [3969/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [3970/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (98s)
✔ [3971/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (94s)
✔ [3972/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (80s)
✔ [3973/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (84s)
✔ [3974/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (63s)
✔ [3975/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (60s)
✔ [3976/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (58s)
✔ [3977/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (58s)
✔ [3978/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (57s)
✔ [3979/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (55s)
✔ [3980/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (52s)
✔ [3981/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (51s)
✔ [3982/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (8.3s)
✔ [3983/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (36s)
✔ [3984/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
✔ [3987/3999] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (117s)
✔ [3989/4003] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (74s)
✔ [3994/4008] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.2s)
⚠ [3995/4008] 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`
⚠ [3997/4008] 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`
✔ [3999/4008] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
⚠ [4002/4008] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (36s)
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`
⚠ [4005/4009] Built PrimeNumberTheoremAnd.IEANTN.Dusart (18s)
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`
✔ [4026/4037] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.6s)
⚠ [4028/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`
⚠ [4030/4048] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
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`
⚠ [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`
⚠ [4034/4048] 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`
⚠ [4041/4055] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.5s)
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`
✔ [4044/4055] Built PrimeNumberTheoremAnd.IEANTN.Lcm (27s)
⚠ [4045/4059] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.4s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4046/4059] 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.
✔ [4053/4059] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
✔ [4139/4140] Built PrimeNumberTheoremAnd (5.1s)
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

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (510ms)
✔ [33/40] Built Cli:c.o (71ms)
ℹ [3505/3513] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3523/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`
⚠ [3674/3697] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3686/3697] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3754/3772] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3756/3772] 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`
⚠ [3868/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/4027] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4014/4027] 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`
⚠ [4016/4027] 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:803:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:856:8: declaration uses `sorry`
✔ [4021/4078] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (33s)
⚠ [4023/4078] 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`
⚠ [4024/4078] 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/4085] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
⚠ [4027/4085] 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`
⚠ [4037/4085] 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`
✔ [4038/4090] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.9s)
✔ [4042/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.0s)
✔ [4061/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.0s)
✔ [4062/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.1s)
✔ [4064/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.0s)
✔ [4065/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (2.0s)
✔ [4066/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.1s)
✔ [4067/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.0s)
✔ [4068/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (2.0s)
✔ [4069/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.0s)
✔ [4070/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.0s)
✔ [4071/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.0s)
✔ [4072/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.0s)
✔ [4073/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (2.0s)
✔ [4074/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.0s)
✔ [4075/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (2.0s)
✔ [4076/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.0s)
✔ [4077/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.0s)
✔ [4078/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.0s)
✔ [4083/4113] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.0s)
⚠ [4089/4113] 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`
⚠ [4092/4113] 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`
⚠ [4095/4113] 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`
⚠ [4098/4113] 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`
✔ [4100/4114] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.0s)
✔ [4102/4115] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4105/4115] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.1s)
✔ [4109/4115] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4112/4147] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (13s)
✔ [4135/4174] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.0s)
⚠ [4136/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`
⚠ [4138/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`
✔ [4148/4185] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (44s)
⚠ [4149/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`
⚠ [4151/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`
✔ [4163/4191] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.5s)
⚠ [4164/4191] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4168/4191] 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.
✔ [4172/4191] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.0s)
✔ [4173/4191] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4182/4240] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4324/4327] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.1s)
ℹ [4325/4327] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
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

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

apx-semantic-phase	{"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":4990,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":435303,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":6,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.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":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":4,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":20}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":8501,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 7469f2193d342472bdf6aaf14bb56ed1af99a360468a777986f0b9df1f170b27
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":47,"runner_cache_hit":true}
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":500885,"ok":true}

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

apx-semantic-phase	{"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":265,"diagnostic_count":144,"duration_ms":21831,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":429587,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":265,"diagnostic_count":144,"duration_ms":9,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.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":1291893,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1291893,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":23}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":9924,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 7469f2193d342472bdf6aaf14bb56ed1af99a360468a777986f0b9df1f170b27
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":52,"runner_cache_hit":true}
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":462113,"ok":true}