Run 110

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

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

git checkout 8a3a3905ac385bcd0d0e6daed5b739e12d1e0b6f

fatal: reference is not a tree: 8a3a3905ac385bcd0d0e6daed5b739e12d1e0b6f

git fetch --depth 1 origin 8a3a3905ac385bcd0d0e6daed5b739e12d1e0b6f

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

git checkout 8a3a3905ac385bcd0d0e6daed5b739e12d1e0b6f (after fetch)

Note: switching to '8a3a3905ac385bcd0d0e6daed5b739e12d1e0b6f'.

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 8a3a390 BKLNW: prove bklnw_table_10_verification over the unabridged Table 10 (#1517)

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%, 12 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8459 = 0%, 3 KB/s], Decompressed: 14
Downloaded: 42 file(s) [attempted 42/8459 = 0%, 24 KB/s], Decompressed: 39
Downloaded: 71 file(s) [attempted 71/8459 = 0%, 54 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 63 KB/s], Decompressed: 96
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 39 KB/s], Decompressed: 131
Downloaded: 170 file(s) [attempted 170/8459 = 2%, 353 KB/s], Decompressed: 165
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 392 KB/s], Decompressed: 192
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 82 KB/s], Decompressed: 230
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 296 KB/s], Decompressed: 271
Downloaded: 312 file(s) [attempted 312/8459 = 3%, 504 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 50 KB/s], Decompressed: 347
Downloaded: 388 file(s) [attempted 388/8459 = 4%, 132 KB/s], Decompressed: 384
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 320 KB/s], Decompressed: 422
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 427 KB/s], Decompressed: 466
Downloaded: 514 file(s) [attempted 514/8459 = 6%, 66 KB/s], Decompressed: 511
Downloaded: 554 file(s) [attempted 554/8459 = 6%, 984 KB/s], Decompressed: 545
Downloaded: 586 file(s) [attempted 586/8459 = 6%, 369 KB/s], Decompressed: 580
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 42 KB/s], Decompressed: 624
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 63 KB/s], Decompressed: 665
Downloaded: 711 file(s) [attempted 711/8459 = 8%, 288 KB/s], Decompressed: 706
Downloaded: 747 file(s) [attempted 747/8459 = 8%, 238 KB/s], Decompressed: 744
Downloaded: 782 file(s) [attempted 782/8459 = 9%, 120 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 188 KB/s], Decompressed: 819
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 385 KB/s], Decompressed: 864
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 365 KB/s], Decompressed: 908
Downloaded: 953 file(s) [attempted 953/8459 = 11%, 407 KB/s], Decompressed: 946
Downloaded: 984 file(s) [attempted 984/8459 = 11%, 288 KB/s], Decompressed: 980
Downloaded: 1021 file(s) [attempted 1021/8459 = 12%, 172 KB/s], Decompressed: 1018
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 710 KB/s], Decompressed: 1059
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 427 KB/s], Decompressed: 1100
Downloaded: 1141 file(s) [attempted 1141/8459 = 13%, 1933 KB/s], Decompressed: 1134
Downloaded: 1179 file(s) [attempted 1179/8459 = 13%, 89 KB/s], Decompressed: 1169
Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 222 KB/s], Decompressed: 1210
Downloaded: 1261 file(s) [attempted 1261/8459 = 14%, 190 KB/s], Decompressed: 1258
Downloaded: 1299 file(s) [attempted 1299/8459 = 15%, 213 KB/s], Decompressed: 1292
Downloaded: 1334 file(s) [attempted 1334/8459 = 15%, 51 KB/s], Decompressed: 1329
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 35 KB/s], Decompressed: 1370
Downloaded: 1412 file(s) [attempted 1412/8459 = 16%, 93 KB/s], Decompressed: 1408
Downloaded: 1459 file(s) [attempted 1459/8459 = 17%, 520 KB/s], Decompressed: 1449
Downloaded: 1497 file(s) [attempted 1497/8459 = 17%, 1476 KB/s], Decompressed: 1494
Downloaded: 1535 file(s) [attempted 1535/8459 = 18%, 314 KB/s], Decompressed: 1531
Downloaded: 1579 file(s) [attempted 1579/8459 = 18%, 327 KB/s], Decompressed: 1576
Downloaded: 1622 file(s) [attempted 1622/8459 = 19%, 204 KB/s], Decompressed: 1613
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 58 KB/s], Decompressed: 1655
Downloaded: 1696 file(s) [attempted 1696/8459 = 20%, 295 KB/s], Decompressed: 1689
Downloaded: 1737 file(s) [attempted 1737/8459 = 20%, 347 KB/s], Decompressed: 1733
Downloaded: 1774 file(s) [attempted 1774/8459 = 20%, 145 KB/s], Decompressed: 1771
Downloaded: 1813 file(s) [attempted 1813/8459 = 21%, 88 KB/s], Decompressed: 1809
Downloaded: 1854 file(s) [attempted 1854/8459 = 21%, 297 KB/s], Decompressed: 1852
Downloaded: 1887 file(s) [attempted 1887/8459 = 22%, 1363 KB/s], Decompressed: 1884
Downloaded: 1931 file(s) [attempted 1931/8459 = 22%, 559 KB/s], Decompressed: 1921
Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 314 KB/s], Decompressed: 1959
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 358 KB/s], Decompressed: 2000
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 185 KB/s], Decompressed: 2041
Downloaded: 2081 file(s) [attempted 2081/8459 = 24%, 1102 KB/s], Decompressed: 2075
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 188 KB/s], Decompressed: 2120
Downloaded: 2161 file(s) [attempted 2161/8459 = 25%, 201 KB/s], Decompressed: 2158
Downloaded: 2203 file(s) [attempted 2203/8459 = 26%, 517 KB/s], Decompressed: 2199
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 186 KB/s], Decompressed: 2236
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 379 KB/s], Decompressed: 2277
Downloaded: 2322 file(s) [attempted 2322/8459 = 27%, 81 KB/s], Decompressed: 2318
Downloaded: 2363 file(s) [attempted 2363/8459 = 27%, 1280 KB/s], Decompressed: 2360
Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 45 KB/s], Decompressed: 2397
Downloaded: 2442 file(s) [attempted 2442/8459 = 28%, 25 KB/s], Decompressed: 2438
Downloaded: 2480 file(s) [attempted 2480/8459 = 29%, 43 KB/s], Decompressed: 2476
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 81 KB/s], Decompressed: 2503
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 202 KB/s], Decompressed: 2558
Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 119 KB/s], Decompressed: 2596
Downloaded: 2644 file(s) [attempted 2644/8459 = 31%, 220 KB/s], Decompressed: 2637
Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 134 KB/s], Decompressed: 2681
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 190 KB/s], Decompressed: 2719
Downloaded: 2764 file(s) [attempted 2764/8459 = 32%, 57 KB/s], Decompressed: 2757
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 490 KB/s], Decompressed: 2798
Downloaded: 2846 file(s) [attempted 2846/8459 = 33%, 73 KB/s], Decompressed: 2839
Downloaded: 2887 file(s) [attempted 2887/8459 = 34%, 145 KB/s], Decompressed: 2883
Downloaded: 2927 file(s) [attempted 2927/8459 = 34%, 79 KB/s], Decompressed: 2921
Downloaded: 2965 file(s) [attempted 2965/8459 = 35%, 155 KB/s], Decompressed: 2955
Downloaded: 3003 file(s) [attempted 3003/8459 = 35%, 300 KB/s], Decompressed: 3000
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 162 KB/s], Decompressed: 3037
Downloaded: 3087 file(s) [attempted 3087/8459 = 36%, 240 KB/s], Decompressed: 3082
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 150 KB/s], Decompressed: 3123
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 65 KB/s], Decompressed: 3160
Downloaded: 3201 file(s) [attempted 3201/8459 = 37%, 513 KB/s], Decompressed: 3198
Downloaded: 3246 file(s) [attempted 3246/8459 = 38%, 44 KB/s], Decompressed: 3239
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 99 KB/s], Decompressed: 3284
Downloaded: 3332 file(s) [attempted 3332/8459 = 39%, 394 KB/s], Decompressed: 3325
Downloaded: 3368 file(s) [attempted 3368/8459 = 39%, 1876 KB/s], Decompressed: 3355
Downloaded: 3401 file(s) [attempted 3401/8459 = 40%, 70 KB/s], Decompressed: 3396
Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 67 KB/s], Decompressed: 3438
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 195 KB/s], Decompressed: 3479
Downloaded: 3527 file(s) [attempted 3527/8459 = 41%, 81 KB/s], Decompressed: 3523
Downloaded: 3564 file(s) [attempted 3564/8459 = 42%, 409 KB/s], Decompressed: 3557
Downloaded: 3602 file(s) [attempted 3602/8459 = 42%, 382 KB/s], Decompressed: 3592
Downloaded: 3639 file(s) [attempted 3639/8459 = 43%, 133 KB/s], Decompressed: 3636
Downloaded: 3684 file(s) [attempted 3684/8459 = 43%, 706 KB/s], Decompressed: 3681
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 157 KB/s], Decompressed: 3722
Downloaded: 3762 file(s) [attempted 3762/8459 = 44%, 59 KB/s], Decompressed: 3756
Downloaded: 3800 file(s) [attempted 3800/8459 = 44%, 86 KB/s], Decompressed: 3793
Downloaded: 3838 file(s) [attempted 3838/8459 = 45%, 132 KB/s], Decompressed: 3835
Downloaded: 3882 file(s) [attempted 3882/8459 = 45%, 585 KB/s], Decompressed: 3879
Downloaded: 3924 file(s) [attempted 3924/8459 = 46%, 79 KB/s], Decompressed: 3920
Downloaded: 3961 file(s) [attempted 3961/8459 = 46%, 81 KB/s], Decompressed: 3958
Downloaded: 3999 file(s) [attempted 3999/8459 = 47%, 561 KB/s], Decompressed: 3992
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 117 KB/s], Decompressed: 4033
Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 168 KB/s], Decompressed: 4074
Downloaded: 4122 file(s) [attempted 4122/8459 = 48%, 152 KB/s], Decompressed: 4115
Downloaded: 4156 file(s) [attempted 4156/8459 = 49%, 44 KB/s], Decompressed: 4149
Downloaded: 4197 file(s) [attempted 4197/8459 = 49%, 414 KB/s], Decompressed: 4190
Downloaded: 4238 file(s) [attempted 4238/8459 = 50%, 246 KB/s], Decompressed: 4232
Downloaded: 4283 file(s) [attempted 4283/8459 = 50%, 220 KB/s], Decompressed: 4279
Downloaded: 4327 file(s) [attempted 4327/8459 = 51%, 1924 KB/s], Decompressed: 4321
Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 1901 KB/s], Decompressed: 4356
Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 1000 KB/s], Decompressed: 4396
Downloaded: 4444 file(s) [attempted 4444/8459 = 52%, 777 KB/s], Decompressed: 4433
Downloaded: 4481 file(s) [attempted 4481/8459 = 52%, 389 KB/s], Decompressed: 4478
Downloaded: 4522 file(s) [attempted 4522/8459 = 53%, 522 KB/s], Decompressed: 4519
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 1476 KB/s], Decompressed: 4553
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 719 KB/s], Decompressed: 4598
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 360 KB/s], Decompressed: 4646
Downloaded: 4697 file(s) [attempted 4697/8459 = 55%, 1052 KB/s], Decompressed: 4694
Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 94 KB/s], Decompressed: 4731
Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 122 KB/s], Decompressed: 4765
Downloaded: 4811 file(s) [attempted 4811/8459 = 56%, 425 KB/s], Decompressed: 4807
Downloaded: 4852 file(s) [attempted 4852/8459 = 57%, 441 KB/s], Decompressed: 4844
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 44 KB/s], Decompressed: 4889
Downloaded: 4931 file(s) [attempted 4931/8459 = 58%, 560 KB/s], Decompressed: 4923
Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 242 KB/s], Decompressed: 4957
Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 82 KB/s], Decompressed: 5002
Downloaded: 5046 file(s) [attempted 5046/8459 = 59%, 159 KB/s], Decompressed: 5039
Downloaded: 5091 file(s) [attempted 5091/8459 = 60%, 871 KB/s], Decompressed: 5084
Downloaded: 5128 file(s) [attempted 5128/8459 = 60%, 272 KB/s], Decompressed: 5121
Downloaded: 5166 file(s) [attempted 5166/8459 = 61%, 424 KB/s], Decompressed: 5149
Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 109 KB/s], Decompressed: 5197
Downloaded: 5248 file(s) [attempted 5248/8459 = 62%, 425 KB/s], Decompressed: 5245
Downloaded: 5294 file(s) [attempted 5294/8459 = 62%, 59 KB/s], Decompressed: 5289
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 1069 KB/s], Decompressed: 5323
Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 728 KB/s], Decompressed: 5354
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 59 KB/s], Decompressed: 5402
Downloaded: 5450 file(s) [attempted 5450/8459 = 64%, 281 KB/s], Decompressed: 5447
Downloaded: 5494 file(s) [attempted 5494/8459 = 64%, 217 KB/s], Decompressed: 5491
Downloaded: 5536 file(s) [attempted 5536/8459 = 65%, 230 KB/s], Decompressed: 5529
Downloaded: 5563 file(s) [attempted 5563/8459 = 65%, 120 KB/s], Decompressed: 5559
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 475 KB/s], Decompressed: 5604
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 182 KB/s], Decompressed: 5645
Downloaded: 5696 file(s) [attempted 5696/8459 = 67%, 110 KB/s], Decompressed: 5693
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 38 KB/s], Decompressed: 5741
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 41 KB/s], Decompressed: 5789
Downloaded: 5824 file(s) [attempted 5824/8459 = 68%, 365 KB/s], Decompressed: 5816
Downloaded: 5861 file(s) [attempted 5861/8459 = 69%, 115 KB/s], Decompressed: 5854
Downloaded: 5902 file(s) [attempted 5902/8459 = 69%, 142 KB/s], Decompressed: 5898
Downloaded: 5943 file(s) [attempted 5943/8459 = 70%, 627 KB/s], Decompressed: 5939
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 252 KB/s], Decompressed: 5984
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 1058 KB/s], Decompressed: 6025
Downloaded: 6063 file(s) [attempted 6063/8459 = 71%, 1791 KB/s], Decompressed: 6059
Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 583 KB/s], Decompressed: 6097
Downloaded: 6142 file(s) [attempted 6142/8459 = 72%, 221 KB/s], Decompressed: 6138
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 205 KB/s], Decompressed: 6186
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 365 KB/s], Decompressed: 6230
Downloaded: 6276 file(s) [attempted 6276/8459 = 74%, 167 KB/s], Decompressed: 6271
Downloaded: 6311 file(s) [attempted 6311/8459 = 74%, 506 KB/s], Decompressed: 6302
Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 814 KB/s], Decompressed: 6343
Downloaded: 6396 file(s) [attempted 6396/8459 = 75%, 458 KB/s], Decompressed: 6391
Downloaded: 6433 file(s) [attempted 6433/8459 = 76%, 154 KB/s], Decompressed: 6425
Downloaded: 6473 file(s) [attempted 6473/8459 = 76%, 271 KB/s], Decompressed: 6466
Downloaded: 6509 file(s) [attempted 6509/8459 = 76%, 110 KB/s], Decompressed: 6497
Downloaded: 6548 file(s) [attempted 6548/8459 = 77%, 1357 KB/s], Decompressed: 6545
Downloaded: 6596 file(s) [attempted 6596/8459 = 77%, 127 KB/s], Decompressed: 6593
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 129 KB/s], Decompressed: 6637
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 242 KB/s], Decompressed: 6682
Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 264 KB/s], Decompressed: 6723
Downloaded: 6764 file(s) [attempted 6764/8459 = 79%, 444 KB/s], Decompressed: 6757
Downloaded: 6805 file(s) [attempted 6805/8459 = 80%, 552 KB/s], Decompressed: 6802
Downloaded: 6846 file(s) [attempted 6846/8459 = 80%, 391 KB/s], Decompressed: 6843
Downloaded: 6891 file(s) [attempted 6891/8459 = 81%, 52 KB/s], Decompressed: 6880
Downloaded: 6926 file(s) [attempted 6926/8459 = 81%, 92 KB/s], Decompressed: 6922
Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 170 KB/s], Decompressed: 6959
Downloaded: 7000 file(s) [attempted 7000/8459 = 82%, 175 KB/s], Decompressed: 6997
Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 146 KB/s], Decompressed: 7038
Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 43 KB/s], Decompressed: 7072
Downloaded: 7123 file(s) [attempted 7123/8459 = 84%, 492 KB/s], Decompressed: 7119
Downloaded: 7161 file(s) [attempted 7161/8459 = 84%, 76 KB/s], Decompressed: 7154
Downloaded: 7202 file(s) [attempted 7202/8459 = 85%, 201 KB/s], Decompressed: 7199
Downloaded: 7240 file(s) [attempted 7240/8459 = 85%, 90 KB/s], Decompressed: 7236
Downloaded: 7284 file(s) [attempted 7284/8459 = 86%, 178 KB/s], Decompressed: 7277
Downloaded: 7329 file(s) [attempted 7329/8459 = 86%, 462 KB/s], Decompressed: 7316
Downloaded: 7360 file(s) [attempted 7360/8459 = 87%, 312 KB/s], Decompressed: 7356
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 1326 KB/s], Decompressed: 7397
Downloaded: 7435 file(s) [attempted 7435/8459 = 87%, 113 KB/s], Decompressed: 7428
Downloaded: 7483 file(s) [attempted 7483/8459 = 88%, 608 KB/s], Decompressed: 7479
Downloaded: 7524 file(s) [attempted 7524/8459 = 88%, 326 KB/s], Decompressed: 7514
Downloaded: 7551 file(s) [attempted 7551/8459 = 89%, 627 KB/s], Decompressed: 7544
Downloaded: 7594 file(s) [attempted 7594/8459 = 89%, 223 KB/s], Decompressed: 7589
Downloaded: 7634 file(s) [attempted 7634/8459 = 90%, 1217 KB/s], Decompressed: 7630
Downloaded: 7681 file(s) [attempted 7681/8459 = 90%, 616 KB/s], Decompressed: 7678
Downloaded: 7719 file(s) [attempted 7719/8459 = 91%, 855 KB/s], Decompressed: 7712
Downloaded: 7753 file(s) [attempted 7753/8459 = 91%, 140 KB/s], Decompressed: 7750
Downloaded: 7792 file(s) [attempted 7792/8459 = 92%, 477 KB/s], Decompressed: 7784
Downloaded: 7832 file(s) [attempted 7832/8459 = 92%, 689 KB/s], Decompressed: 7828
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 544 KB/s], Decompressed: 7873
Downloaded: 7918 file(s) [attempted 7918/8459 = 93%, 33 KB/s], Decompressed: 7911
Downloaded: 7952 file(s) [attempted 7952/8459 = 94%, 225 KB/s], Decompressed: 7948
Downloaded: 7993 file(s) [attempted 7993/8459 = 94%, 292 KB/s], Decompressed: 7989
Downloaded: 8030 file(s) [attempted 8030/8459 = 94%, 895 KB/s], Decompressed: 8027
Downloaded: 8071 file(s) [attempted 8071/8459 = 95%, 301 KB/s], Decompressed: 8068
Downloaded: 8114 file(s) [attempted 8114/8459 = 95%, 368 KB/s], Decompressed: 8102
Downloaded: 8150 file(s) [attempted 8150/8459 = 96%, 779 KB/s], Decompressed: 8147
Downloaded: 8195 file(s) [attempted 8195/8459 = 96%, 91 KB/s], Decompressed: 8191
Downloaded: 8233 file(s) [attempted 8233/8459 = 97%, 355 KB/s], Decompressed: 8229
Downloaded: 8273 file(s) [attempted 8273/8459 = 97%, 283 KB/s], Decompressed: 8256
Downloaded: 8314 file(s) [attempted 8314/8459 = 98%, 481 KB/s], Decompressed: 8308
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 310 KB/s], Decompressed: 8349
Downloaded: 8393 file(s) [attempted 8393/8459 = 99%, 321 KB/s], Decompressed: 8390
Downloaded: 8434 file(s) [attempted 8434/8459 = 99%, 154 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 473 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 473 KB/s], Decompressed: 8455

lake build

ℹ [3472/3480] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3488/3504] 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`
⚠ [3627/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`
⚠ [3702/3720] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3703/3720] 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`
⚠ [3811/3843] 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/3843] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3945/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`
✔ [3947/3956] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (92s)
⚠ [3949/3956] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (18s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
⚠ [3950/3956] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [3951/3956] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (88s)
⚠ [3953/3956] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (29s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
⚠ [3954/3956] 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.0s)
✔ [3958/3986] Built LeanCert.Engine.WitnessSum (2.7s)
✔ [3959/3987] Built LeanCert.Engine.ReflectiveSum (4.0s)
✔ [3961/3989] Built LeanCert.Examples.BKLNW_a2_reflective (20s)
✔ [3964/3989] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.5s)
✔ [3966/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.0s)
⚠ [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 (102s)
✔ [3971/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (98s)
✔ [3972/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (78s)
✔ [3973/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (77s)
✔ [3974/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (64s)
✔ [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 (59s)
✔ [3978/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (55s)
✔ [3979/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (52s)
✔ [3980/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (53s)
✔ [3981/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (49s)
✔ [3982/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.7s)
✔ [3983/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (36s)
✔ [3984/3994] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
✔ [3987/4001] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (116s)
✔ [3989/4003] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (74s)
✔ [3994/4008] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.1s)
⚠ [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/4016] 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`
✔ [4025/4047] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.3s)
⚠ [4027/4047] 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`
⚠ [4029/4047] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (13s)
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`
⚠ [4032/4047] 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`
⚠ [4035/4047] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (9.3s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1142:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1196:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1271:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1297:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1381:8: declaration uses `sorry`
⚠ [4040/4054] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.3s)
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`
✔ [4043/4054] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
⚠ [4044/4058] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.2s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4045/4058] 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.
✔ [4052/4058] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
✔ [4138/4139] Built PrimeNumberTheoremAnd (4.4s)
Build completed successfully (4139 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.7s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (517ms)
✔ [33/39] Built Cli:c.o (62ms)
ℹ [3505/3515] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3529/3549] 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`
⚠ [3681/3700] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3691/3700] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3754/3765] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3756/3765] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
⚠ [3867/3887] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean: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`
⚠ [3869/3887] 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.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4015/4027] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4016/4027] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (4.7s)
⚠ [4017/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:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [4021/4078] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (21s)
✔ [4022/4078] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.7s)
⚠ [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/4081] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
⚠ [4027/4081] 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/4090] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.9s)
⚠ [4039/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`
✔ [4040/4090] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.0s)
✔ [4061/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.0s)
✔ [4062/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (2.0s)
✔ [4063/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.0s)
✔ [4064/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.0s)
✔ [4065/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (2.9s)
✔ [4066/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (2.0s)
✔ [4067/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.0s)
✔ [4068/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.0s)
✔ [4069/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.0s)
✔ [4070/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.0s)
✔ [4071/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.0s)
✔ [4072/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (2.0s)
✔ [4073/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (2.0s)
✔ [4074/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (2.0s)
✔ [4075/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.1s)
✔ [4076/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.0s)
✔ [4077/4102] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.0s)
✔ [4083/4112] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (2.0s)
⚠ [4089/4112] 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`
✔ [4091/4113] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.0s)
⚠ [4093/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`
⚠ [4096/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`
⚠ [4099/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`
✔ [4102/4115] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.0s)
✔ [4106/4115] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4108/4115] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4112/4121] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (14s)
✔ [4133/4172] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.8s)
⚠ [4134/4172] 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`
⚠ [4136/4172] 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`
⚠ [4139/4172] 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/4172] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1142:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1196:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1271:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1297:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1381:8: declaration uses `sorry`
✔ [4149/4183] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (47s)
⚠ [4150/4183] 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`
✔ [4161/4186] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.9s)
✔ [4162/4186] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (15s)
⚠ [4166/4189] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4169/4189] 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.
✔ [4170/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.0s)
✔ [4171/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4180/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
✔ [4322/4324] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (5.7s)
ℹ [4324/4325] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (64ms)
info: Blueprint indexing
Build completed successfully (4325 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":21,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":20059,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":447653,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":235,"diagnostic_count":164,"duration_ms":24,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.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":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":269,"diagnostic_count":182,"duration_ms":23513,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":443574,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":269,"diagnostic_count":182,"duration_ms":21,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.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":1825220,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1825220,"phase":"lean_module_json_write"}

apx-semantic-phase	{"phase":"core_compile","duration_ms":22}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":6969,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache f7532979943cf33a280af87b3b56d9f73d2a2caf1be530104ca3086a03229abb
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":48,"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":977881,"ok":true}

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

apx-semantic-phase	{"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":3325,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":442188,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":41,"diagnostic_count":6,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.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":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":67,"diagnostic_count":53,"duration_ms":5366,"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":450078,"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":5,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":265,"diagnostic_count":144,"duration_ms":22926,"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":455568,"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":10,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":1291893,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"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":8855,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache f7532979943cf33a280af87b3b56d9f73d2a2caf1be530104ca3086a03229abb
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":44,"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":1390743,"ok":true}