Verification run

Run 24

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit a249829a5503 toolchain lean-v4-30-0 prover lean took 8h 5m · finished 5w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase ./.apodeixis/tools/lean-semantic-extract.sh)

Open project

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 867 ms · created 6/9/2026, 6:01:39 PM

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

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

git_checkout exit 0 duration 38 ms · created 6/9/2026, 6:01:39 PM

git checkout a249829a55039f4122d87650ef5c1109d18c1a6a

Note: switching to 'a249829a55039f4122d87650ef5c1109d18c1a6a'.

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 a249829 feat(HadamardZeta): specialize Hadamard factorization to Riemann zeta & xi (#1504)

lake_cache exit 0 duration 40s · created 6/9/2026, 6:01:39 PM

lake exe cache get

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

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 11 KB/s], Decompressed: 11
Downloaded: 36 file(s) [attempted 36/8459 = 0%, 14 KB/s], Decompressed: 33
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 57 KB/s], Decompressed: 61
Downloaded: 88 file(s) [attempted 88/8459 = 1%, 584 KB/s], Decompressed: 83
Downloaded: 124 file(s) [attempted 124/8459 = 1%, 330 KB/s], Decompressed: 117
Downloaded: 158 file(s) [attempted 158/8459 = 1%, 95 KB/s], Decompressed: 151
Downloaded: 196 file(s) [attempted 196/8459 = 2%, 276 KB/s], Decompressed: 192
Downloaded: 237 file(s) [attempted 237/8459 = 2%, 452 KB/s], Decompressed: 234
Downloaded: 275 file(s) [attempted 275/8459 = 3%, 297 KB/s], Decompressed: 271
Downloaded: 316 file(s) [attempted 316/8459 = 3%, 346 KB/s], Decompressed: 309
Downloaded: 353 file(s) [attempted 353/8459 = 4%, 23 KB/s], Decompressed: 347
Downloaded: 391 file(s) [attempted 391/8459 = 4%, 54 KB/s], Decompressed: 388
Downloaded: 432 file(s) [attempted 432/8459 = 5%, 113 KB/s], Decompressed: 429
Downloaded: 470 file(s) [attempted 470/8459 = 5%, 877 KB/s], Decompressed: 466
Downloaded: 511 file(s) [attempted 511/8459 = 6%, 600 KB/s], Decompressed: 508
Downloaded: 552 file(s) [attempted 552/8459 = 6%, 516 KB/s], Decompressed: 545
Downloaded: 587 file(s) [attempted 587/8459 = 6%, 45 KB/s], Decompressed: 583
Downloaded: 626 file(s) [attempted 626/8459 = 7%, 156 KB/s], Decompressed: 621
Downloaded: 665 file(s) [attempted 665/8459 = 7%, 47 KB/s], Decompressed: 662
Downloaded: 708 file(s) [attempted 708/8459 = 8%, 426 KB/s], Decompressed: 699
Downloaded: 748 file(s) [attempted 748/8459 = 8%, 62 KB/s], Decompressed: 744
Downloaded: 783 file(s) [attempted 783/8459 = 9%, 113 KB/s], Decompressed: 778
Downloaded: 822 file(s) [attempted 822/8459 = 9%, 200 KB/s], Decompressed: 812
Downloaded: 860 file(s) [attempted 860/8459 = 10%, 215 KB/s], Decompressed: 857
Downloaded: 902 file(s) [attempted 902/8459 = 10%, 131 KB/s], Decompressed: 898
Downloaded: 939 file(s) [attempted 939/8459 = 11%, 339 KB/s], Decompressed: 936
Downloaded: 977 file(s) [attempted 977/8459 = 11%, 74 KB/s], Decompressed: 970
Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 902 KB/s], Decompressed: 1011
Downloaded: 1057 file(s) [attempted 1057/8459 = 12%, 528 KB/s], Decompressed: 1052
Downloaded: 1097 file(s) [attempted 1097/8459 = 12%, 1593 KB/s], Decompressed: 1090
Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 100 KB/s], Decompressed: 1127
Downloaded: 1172 file(s) [attempted 1172/8459 = 13%, 834 KB/s], Decompressed: 1169
Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 154 KB/s], Decompressed: 1210
Downloaded: 1254 file(s) [attempted 1254/8459 = 14%, 538 KB/s], Decompressed: 1247
Downloaded: 1288 file(s) [attempted 1288/8459 = 15%, 224 KB/s], Decompressed: 1281
Downloaded: 1329 file(s) [attempted 1329/8459 = 15%, 89 KB/s], Decompressed: 1327
Downloaded: 1370 file(s) [attempted 1370/8459 = 16%, 747 KB/s], Decompressed: 1367
Downloaded: 1408 file(s) [attempted 1408/8459 = 16%, 1059 KB/s], Decompressed: 1405
Downloaded: 1448 file(s) [attempted 1448/8459 = 17%, 276 KB/s], Decompressed: 1442
Downloaded: 1487 file(s) [attempted 1487/8459 = 17%, 63 KB/s], Decompressed: 1483
Downloaded: 1528 file(s) [attempted 1528/8459 = 18%, 126 KB/s], Decompressed: 1521
Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 210 KB/s], Decompressed: 1562
Downloaded: 1605 file(s) [attempted 1605/8459 = 18%, 104 KB/s], Decompressed: 1600
Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 269 KB/s], Decompressed: 1641
Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 325 KB/s], Decompressed: 1682
Downloaded: 1726 file(s) [attempted 1726/8459 = 20%, 129 KB/s], Decompressed: 1723
Downloaded: 1764 file(s) [attempted 1764/8459 = 20%, 148 KB/s], Decompressed: 1761
Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 291 KB/s], Decompressed: 1802
Downloaded: 1853 file(s) [attempted 1853/8459 = 21%, 150 KB/s], Decompressed: 1846
Downloaded: 1897 file(s) [attempted 1897/8459 = 22%, 129 KB/s], Decompressed: 1891
Downloaded: 1932 file(s) [attempted 1932/8459 = 22%, 46 KB/s], Decompressed: 1928
Downloaded: 1969 file(s) [attempted 1969/8459 = 23%, 180 KB/s], Decompressed: 1966
Downloaded: 2006 file(s) [attempted 2006/8459 = 23%, 734 KB/s], Decompressed: 2000
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 189 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8459 = 24%, 696 KB/s], Decompressed: 2082
Downloaded: 2127 file(s) [attempted 2127/8459 = 25%, 34 KB/s], Decompressed: 2120
Downloaded: 2164 file(s) [attempted 2164/8459 = 25%, 280 KB/s], Decompressed: 2161
Downloaded: 2206 file(s) [attempted 2206/8459 = 26%, 741 KB/s], Decompressed: 2202
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 176 KB/s], Decompressed: 2236
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 801 KB/s], Decompressed: 2277
Downloaded: 2325 file(s) [attempted 2325/8459 = 27%, 294 KB/s], Decompressed: 2322
Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 278 KB/s], Decompressed: 2360
Downloaded: 2404 file(s) [attempted 2404/8459 = 28%, 266 KB/s], Decompressed: 2397
Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 67 KB/s], Decompressed: 2442
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 29 KB/s], Decompressed: 2479
Downloaded: 2524 file(s) [attempted 2524/8459 = 29%, 247 KB/s], Decompressed: 2520
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 700 KB/s], Decompressed: 2561
Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 116 KB/s], Decompressed: 2603
Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 586 KB/s], Decompressed: 2644
Downloaded: 2688 file(s) [attempted 2688/8459 = 31%, 402 KB/s], Decompressed: 2681
Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 190 KB/s], Decompressed: 2715
Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 1137 KB/s], Decompressed: 2757
Downloaded: 2804 file(s) [attempted 2804/8459 = 33%, 484 KB/s], Decompressed: 2801
Downloaded: 2846 file(s) [attempted 2846/8459 = 33%, 1441 KB/s], Decompressed: 2842
Downloaded: 2890 file(s) [attempted 2890/8459 = 34%, 292 KB/s], Decompressed: 2887
Downloaded: 2926 file(s) [attempted 2926/8459 = 34%, 111 KB/s], Decompressed: 2917
Downloaded: 2963 file(s) [attempted 2963/8459 = 35%, 141 KB/s], Decompressed: 2958
Downloaded: 3000 file(s) [attempted 3000/8459 = 35%, 619 KB/s], Decompressed: 2996
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 1316 KB/s], Decompressed: 3041
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 517 KB/s], Decompressed: 3082
Downloaded: 3133 file(s) [attempted 3133/8459 = 37%, 100 KB/s], Decompressed: 3126
Downloaded: 3171 file(s) [attempted 3171/8459 = 37%, 62 KB/s], Decompressed: 3164
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 221 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 94 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 278 KB/s], Decompressed: 3284
Downloaded: 3330 file(s) [attempted 3330/8459 = 39%, 173 KB/s], Decompressed: 3325
Downloaded: 3369 file(s) [attempted 3369/8459 = 39%, 175 KB/s], Decompressed: 3366
Downloaded: 3408 file(s) [attempted 3408/8459 = 40%, 629 KB/s], Decompressed: 3403
Downloaded: 3444 file(s) [attempted 3444/8459 = 40%, 68 KB/s], Decompressed: 3438
Downloaded: 3485 file(s) [attempted 3485/8459 = 41%, 194 KB/s], Decompressed: 3482
Downloaded: 3528 file(s) [attempted 3528/8459 = 41%, 602 KB/s], Decompressed: 3520
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 24 KB/s], Decompressed: 3564
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 1361 KB/s], Decompressed: 3605
Downloaded: 3650 file(s) [attempted 3650/8459 = 43%, 686 KB/s], Decompressed: 3643
Downloaded: 3685 file(s) [attempted 3685/8459 = 43%, 30 KB/s], Decompressed: 3681
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 153 KB/s], Decompressed: 3718
Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 632 KB/s], Decompressed: 3764
Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 420 KB/s], Decompressed: 3800
Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 424 KB/s], Decompressed: 3841
Downloaded: 3886 file(s) [attempted 3886/8459 = 45%, 142 KB/s], Decompressed: 3879
Downloaded: 3920 file(s) [attempted 3920/8459 = 46%, 330 KB/s], Decompressed: 3917
Downloaded: 3958 file(s) [attempted 3958/8459 = 46%, 90 KB/s], Decompressed: 3954
Downloaded: 4000 file(s) [attempted 4000/8459 = 47%, 81 KB/s], Decompressed: 3995
Downloaded: 4040 file(s) [attempted 4040/8459 = 47%, 94 KB/s], Decompressed: 4036
Downloaded: 4078 file(s) [attempted 4078/8459 = 48%, 255 KB/s], Decompressed: 4071
Downloaded: 4112 file(s) [attempted 4112/8459 = 48%, 217 KB/s], Decompressed: 4108
Downloaded: 4150 file(s) [attempted 4150/8459 = 49%, 35 KB/s], Decompressed: 4146
Downloaded: 4190 file(s) [attempted 4190/8459 = 49%, 252 KB/s], Decompressed: 4188
Downloaded: 4228 file(s) [attempted 4228/8459 = 49%, 468 KB/s], Decompressed: 4221
Downloaded: 4267 file(s) [attempted 4267/8459 = 50%, 70 KB/s], Decompressed: 4262
Downloaded: 4302 file(s) [attempted 4302/8459 = 50%, 47 KB/s], Decompressed: 4293
Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 211 KB/s], Decompressed: 4338
Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 466 KB/s], Decompressed: 4382
Downloaded: 4421 file(s) [attempted 4421/8459 = 52%, 284 KB/s], Decompressed: 4416
Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 217 KB/s], Decompressed: 4454
Downloaded: 4495 file(s) [attempted 4495/8459 = 53%, 203 KB/s], Decompressed: 4492
Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 92 KB/s], Decompressed: 4535
Downloaded: 4576 file(s) [attempted 4576/8459 = 54%, 216 KB/s], Decompressed: 4570
Downloaded: 4615 file(s) [attempted 4615/8459 = 54%, 215 KB/s], Decompressed: 4611
Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 359 KB/s], Decompressed: 4642
Downloaded: 4690 file(s) [attempted 4690/8459 = 55%, 216 KB/s], Decompressed: 4687
Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 91 KB/s], Decompressed: 4728
Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 23 KB/s], Decompressed: 4769
Downloaded: 4807 file(s) [attempted 4807/8459 = 56%, 381 KB/s], Decompressed: 4803
Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 114 KB/s], Decompressed: 4837
Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 136 KB/s], Decompressed: 4878
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 152 KB/s], Decompressed: 4923
Downloaded: 4969 file(s) [attempted 4969/8459 = 58%, 168 KB/s], Decompressed: 4957
Downloaded: 5006 file(s) [attempted 5006/8459 = 59%, 283 KB/s], Decompressed: 4998
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 229 KB/s], Decompressed: 5036
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 146 KB/s], Decompressed: 5077
Downloaded: 5125 file(s) [attempted 5125/8459 = 60%, 1005 KB/s], Decompressed: 5121
Downloaded: 5168 file(s) [attempted 5168/8459 = 61%, 406 KB/s], Decompressed: 5159
Downloaded: 5204 file(s) [attempted 5204/8459 = 61%, 187 KB/s], Decompressed: 5200
Downloaded: 5243 file(s) [attempted 5243/8459 = 61%, 96 KB/s], Decompressed: 5234
Downloaded: 5275 file(s) [attempted 5275/8459 = 62%, 255 KB/s], Decompressed: 5272
Downloaded: 5317 file(s) [attempted 5317/8459 = 62%, 232 KB/s], Decompressed: 5313
Downloaded: 5358 file(s) [attempted 5358/8459 = 63%, 232 KB/s], Decompressed: 5354
Downloaded: 5401 file(s) [attempted 5401/8459 = 63%, 664 KB/s], Decompressed: 5395
Downloaded: 5434 file(s) [attempted 5434/8459 = 64%, 152 KB/s], Decompressed: 5429
Downloaded: 5474 file(s) [attempted 5474/8459 = 64%, 267 KB/s], Decompressed: 5470
Downloaded: 5518 file(s) [attempted 5518/8459 = 65%, 170 KB/s], Decompressed: 5512
Downloaded: 5559 file(s) [attempted 5559/8459 = 65%, 323 KB/s], Decompressed: 5549
Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 21 KB/s], Decompressed: 5594
Downloaded: 5640 file(s) [attempted 5640/8459 = 66%, 48 KB/s], Decompressed: 5636
Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 50 KB/s], Decompressed: 5672
Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 392 KB/s], Decompressed: 5710
Downloaded: 5751 file(s) [attempted 5751/8459 = 67%, 31 KB/s], Decompressed: 5744
Downloaded: 5792 file(s) [attempted 5792/8459 = 68%, 40 KB/s], Decompressed: 5789
Downloaded: 5833 file(s) [attempted 5833/8459 = 68%, 132 KB/s], Decompressed: 5830
Downloaded: 5874 file(s) [attempted 5874/8459 = 69%, 356 KB/s], Decompressed: 5871
Downloaded: 5915 file(s) [attempted 5915/8459 = 69%, 266 KB/s], Decompressed: 5909
Downloaded: 5953 file(s) [attempted 5953/8459 = 70%, 270 KB/s], Decompressed: 5950
Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 534 KB/s], Decompressed: 5987
Downloaded: 6033 file(s) [attempted 6033/8459 = 71%, 127 KB/s], Decompressed: 6028
Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 456 KB/s], Decompressed: 6066
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 542 KB/s], Decompressed: 6104
Downloaded: 6145 file(s) [attempted 6145/8459 = 72%, 43 KB/s], Decompressed: 6141
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 486 KB/s], Decompressed: 6186
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 969 KB/s], Decompressed: 6227
Downloaded: 6268 file(s) [attempted 6268/8459 = 74%, 842 KB/s], Decompressed: 6264
Downloaded: 6306 file(s) [attempted 6306/8459 = 74%, 484 KB/s], Decompressed: 6295
Downloaded: 6336 file(s) [attempted 6336/8459 = 74%, 699 KB/s], Decompressed: 6333
Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 281 KB/s], Decompressed: 6377
Downloaded: 6423 file(s) [attempted 6423/8459 = 75%, 224 KB/s], Decompressed: 6418
Downloaded: 6457 file(s) [attempted 6457/8459 = 76%, 920 KB/s], Decompressed: 6453
Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 1277 KB/s], Decompressed: 6490
Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 87 KB/s], Decompressed: 6531
Downloaded: 6579 file(s) [attempted 6579/8459 = 77%, 395 KB/s], Decompressed: 6576
Downloaded: 6617 file(s) [attempted 6617/8459 = 78%, 337 KB/s], Decompressed: 6610
Downloaded: 6657 file(s) [attempted 6657/8459 = 78%, 132 KB/s], Decompressed: 6651
Downloaded: 6699 file(s) [attempted 6699/8459 = 79%, 118 KB/s], Decompressed: 6692
Downloaded: 6733 file(s) [attempted 6733/8459 = 79%, 435 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 41 KB/s], Decompressed: 6771
Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 1011 KB/s], Decompressed: 6809
Downloaded: 6855 file(s) [attempted 6855/8459 = 81%, 417 KB/s], Decompressed: 6850
Downloaded: 6898 file(s) [attempted 6898/8459 = 81%, 110 KB/s], Decompressed: 6887
Downloaded: 6929 file(s) [attempted 6929/8459 = 81%, 198 KB/s], Decompressed: 6925
Downloaded: 6969 file(s) [attempted 6969/8459 = 82%, 143 KB/s], Decompressed: 6966
Downloaded: 7011 file(s) [attempted 7011/8459 = 82%, 492 KB/s], Decompressed: 7007
Downloaded: 7052 file(s) [attempted 7052/8459 = 83%, 177 KB/s], Decompressed: 7048
Downloaded: 7093 file(s) [attempted 7093/8459 = 83%, 97 KB/s], Decompressed: 7089
Downloaded: 7130 file(s) [attempted 7130/8459 = 84%, 295 KB/s], Decompressed: 7127
Downloaded: 7169 file(s) [attempted 7169/8459 = 84%, 218 KB/s], Decompressed: 7165
Downloaded: 7209 file(s) [attempted 7209/8459 = 85%, 167 KB/s], Decompressed: 7206
Downloaded: 7247 file(s) [attempted 7247/8459 = 85%, 120 KB/s], Decompressed: 7243
Downloaded: 7290 file(s) [attempted 7290/8459 = 86%, 596 KB/s], Decompressed: 7284
Downloaded: 7325 file(s) [attempted 7325/8459 = 86%, 91 KB/s], Decompressed: 7315
Downloaded: 7362 file(s) [attempted 7362/8459 = 87%, 134 KB/s], Decompressed: 7356
Downloaded: 7401 file(s) [attempted 7401/8459 = 87%, 961 KB/s], Decompressed: 7397
Downloaded: 7446 file(s) [attempted 7446/8459 = 88%, 63 KB/s], Decompressed: 7438
Downloaded: 7480 file(s) [attempted 7480/8459 = 88%, 1414 KB/s], Decompressed: 7476
Downloaded: 7520 file(s) [attempted 7520/8459 = 88%, 24 KB/s], Decompressed: 7517
Downloaded: 7560 file(s) [attempted 7560/8459 = 89%, 165 KB/s], Decompressed: 7555
Downloaded: 7604 file(s) [attempted 7604/8459 = 89%, 422 KB/s], Decompressed: 7599
Downloaded: 7640 file(s) [attempted 7640/8459 = 90%, 1439 KB/s], Decompressed: 7637
Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 63 KB/s], Decompressed: 7671
Downloaded: 7716 file(s) [attempted 7716/8459 = 91%, 81 KB/s], Decompressed: 7712
Downloaded: 7757 file(s) [attempted 7757/8459 = 91%, 672 KB/s], Decompressed: 7753
Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 615 KB/s], Decompressed: 7798
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 1071 KB/s], Decompressed: 7832
Downloaded: 7872 file(s) [attempted 7872/8459 = 93%, 211 KB/s], Decompressed: 7866
Downloaded: 7914 file(s) [attempted 7914/8459 = 93%, 405 KB/s], Decompressed: 7911
Downloaded: 7958 file(s) [attempted 7958/8459 = 94%, 74 KB/s], Decompressed: 7955
Downloaded: 8001 file(s) [attempted 8001/8459 = 94%, 161 KB/s], Decompressed: 7996
Downloaded: 8037 file(s) [attempted 8037/8459 = 95%, 493 KB/s], Decompressed: 8030
Downloaded: 8075 file(s) [attempted 8075/8459 = 95%, 470 KB/s], Decompressed: 8068
Downloaded: 8112 file(s) [attempted 8112/8459 = 95%, 89 KB/s], Decompressed: 8109
Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 98 KB/s], Decompressed: 8154
Downloaded: 8200 file(s) [attempted 8200/8459 = 96%, 121 KB/s], Decompressed: 8191
Downloaded: 8236 file(s) [attempted 8236/8459 = 97%, 279 KB/s], Decompressed: 8232
Downloaded: 8270 file(s) [attempted 8270/8459 = 97%, 42 KB/s], Decompressed: 8266
Downloaded: 8311 file(s) [attempted 8311/8459 = 98%, 52 KB/s], Decompressed: 8308
Downloaded: 8353 file(s) [attempted 8353/8459 = 98%, 518 KB/s], Decompressed: 8349
Downloaded: 8390 file(s) [attempted 8390/8459 = 99%, 282 KB/s], Decompressed: 8386
Downloaded: 8432 file(s) [attempted 8432/8459 = 99%, 386 KB/s], Decompressed: 8427
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 405 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 405 KB/s], Decompressed: 8455

lean_checker exit 0 duration 1m 55s · created 6/9/2026, 6:01:39 PM

lake build

ℹ [3472/3603] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3488/3603] 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`
⚠ [3626/3843] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3639/3843] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3702/3843] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3703/3843] 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/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:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
⚠ [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`
⚠ [3946/4021] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3948/4021] 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/4021] 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`
⚠ [3951/4021] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [3954/4021] 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/4021] 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`
⚠ [3962/4021] 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`
⚠ [3972/4021] 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`
⚠ [3973/4021] 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`
⚠ [3978/4021] 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`
⚠ [3995/4021] 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`
⚠ [3996/4021] 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`
⚠ [3997/4021] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4001/4021] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4007/4021] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4008/4021] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring (3.2s)
✔ [4010/4021] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial (4.2s)
✔ [4011/4021] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax (2.3s)
✔ [4015/4030] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic (2.1s)
✔ [4017/4030] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory (2.7s)
ℹ [4018/4032] 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.
✔ [4019/4032] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (3.2s)
✔ [4025/4032] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm (1.9s)
✔ [4026/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog (2.5s)
✔ [4027/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition (3.1s)
✔ [4029/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport (4.8s)
✔ [4030/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor (8.4s)
✔ [4031/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit (6.2s)
✔ [4032/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound (4.3s)
✔ [4033/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral (4.4s)
✔ [4034/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex (5.6s)
⚠ [4035/4058] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (32s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2960:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2980:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3036:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3098:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3296:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3322:8: declaration uses `sorry`
✔ [4037/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp (2.3s)
⚠ [4038/4058] Built PrimeNumberTheoremAnd.IEANTN.Mertens (33s)
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`
✔ [4040/4058] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus (3.1s)
✔ [4041/4058] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct (3.5s)
✔ [4042/4075] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth (3.4s)
✔ [4062/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly (9.9s)
✔ [4063/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex (3.0s)
✔ [4064/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic (2.7s)
✔ [4065/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric (2.7s)
✔ [4066/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation (3.6s)
✔ [4067/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic (5.4s)
✔ [4068/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound (9.5s)
✔ [4069/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux (3.6s)
✔ [4070/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds (2.6s)
✔ [4071/4113] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn (2.3s)
✔ [4072/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real (2.5s)
✔ [4073/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv (2.6s)
✔ [4074/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds (4.3s)
✔ [4077/4113] Built PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (1.9s)
✔ [4079/4113] Built PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy (1.5s)
✔ [4080/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation (2.2s)
✔ [4081/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta (3.6s)
✔ [4082/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits (2.6s)
✔ [4083/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi (2.9s)
✔ [4084/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth (5.7s)
✔ [4085/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence (4.8s)
✔ [4086/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound (3.8s)
✔ [4089/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (2.6s)
✔ [4091/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues (4.1s)
✔ [4092/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber (4.5s)
✔ [4093/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (3.1s)
✔ [4094/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel (4.0s)
✔ [4095/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds (8.7s)
✔ [4096/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement (5.1s)
✔ [4097/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum (3.5s)
✔ [4098/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth (4.7s)
✔ [4099/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor (2.5s)
✔ [4100/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation (2.8s)
✔ [4101/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity (2.8s)
✔ [4102/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence (3.8s)
✔ [4103/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound (1.7s)
✔ [4104/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable (2.7s)
✔ [4105/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor (2.5s)
✔ [4106/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization (4.3s)
✔ [4107/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability (6.4s)
✔ [4108/4113] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder (16s)
✔ [4109/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound (13s)
✔ [4110/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth (4.5s)
✔ [4111/4113] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order (2.4s)
✔ [4112/4113] Built PrimeNumberTheoremAnd (13s)
Build completed successfully (4113 jobs).

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

blueprint_build exit 0 duration 1m 24s · created 6/9/2026, 6:01:39 PM

lake build :blueprint

✔ [550/680] Built Batteries.Lean.NameMapAttribute:c.o (705ms)
✔ [1289/1356] Built Cli:c.o (64ms)
✔ [1797/1970] Built Cli.Extensions:c.o (517ms)
ℹ [3491/3706] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3507/3706] 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`
⚠ [3650/3706] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3666/3901] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3721/3901] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3722/3901] 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`
⚠ [3829/3901] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
⚠ [3831/3901] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3965/4156] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3967/4156] 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`
⚠ [3968/4156] 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`
⚠ [3970/4156] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [3973/4156] 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`
⚠ [3974/4156] 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`
⚠ [3981/4156] 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`
⚠ [3986/4156] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2960:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2980:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3036:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3098:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3296:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3322:8: declaration uses `sorry`
⚠ [3992/4156] 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`
⚠ [3993/4156] 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`
⚠ [3998/4156] 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`
⚠ [4015/4156] 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`
⚠ [4016/4156] 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`
⚠ [4017/4156] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4021/4156] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:198:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:265:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:290:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:414:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4025/4156] 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`
ℹ [4031/4156] 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.
⚠ [4033/4156] 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`
✔ [4131/4276] Built Cli.Basic:c.o (3.1s)
✔ [4207/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring:blueprint (1.6s)
✔ [4208/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial:blueprint (2.5s)
✔ [4210/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax:blueprint (2.6s)
✔ [4211/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic:blueprint (2.1s)
✔ [4212/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory:blueprint (2.6s)
✔ [4213/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition:blueprint (2.4s)
✔ [4214/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds:blueprint (2.6s)
✔ [4215/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm:blueprint (2.0s)
✔ [4216/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct:blueprint (2.6s)
✔ [4217/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog:blueprint (2.3s)
✔ [4218/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound:blueprint (2.6s)
✔ [4219/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound:blueprint (2.7s)
✔ [4220/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport:blueprint (2.3s)
✔ [4221/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex:blueprint (2.6s)
✔ [4222/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit:blueprint (2.6s)
✔ [4223/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence:blueprint (2.6s)
✔ [4224/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits:blueprint (2.6s)
✔ [4225/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber:blueprint (2.6s)
✔ [4226/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement:blueprint (2.6s)
✔ [4227/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor:blueprint (2.6s)
✔ [4228/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence:blueprint (2.7s)
✔ [4229/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable:blueprint (2.7s)
✔ [4230/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor:blueprint (2.7s)
✔ [4231/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound:blueprint (2.6s)
✔ [4232/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound:blueprint (2.2s)
✔ [4233/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral:blueprint (2.7s)
✔ [4234/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex:blueprint (2.2s)
✔ [4235/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly:blueprint (2.6s)
✔ [4236/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp:blueprint (2.4s)
✔ [4237/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth:blueprint (2.3s)
✔ [4238/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth:blueprint (2.6s)
✔ [4239/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus:blueprint (1.8s)
✔ [4240/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization:blueprint (2.6s)
✔ [4241/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic:blueprint (2.6s)
✔ [4242/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth:blueprint (2.6s)
✔ [4243/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic:blueprint (2.5s)
✔ [4244/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic:blueprint (2.2s)
✔ [4245/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability:blueprint (2.6s)
✔ [4246/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth:blueprint (2.7s)
✔ [4247/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order:blueprint (2.7s)
✔ [4248/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric:blueprint (1.9s)
✔ [4249/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation:blueprint (2.8s)
✔ [4250/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi:blueprint (2.7s)
✔ [4251/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux:blueprint (2.5s)
✔ [4252/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds:blueprint (2.6s)
✔ [4253/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds:blueprint (2.6s)
✔ [4254/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds:blueprint (2.7s)
✔ [4255/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn:blueprint (2.4s)
✔ [4256/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals:blueprint (2.5s)
✔ [4257/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv:blueprint (2.5s)
✔ [4258/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real:blueprint (2.2s)
✔ [4259/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic:blueprint (2.6s)
✔ [4260/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation:blueprint (2.6s)
✔ [4261/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta:blueprint (2.8s)
✔ [4262/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel:blueprint (3.1s)
✔ [4263/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum:blueprint (3.2s)
✔ [4264/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation:blueprint (3.1s)
✔ [4265/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity:blueprint (3.2s)
✔ [4266/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound:blueprint (4.3s)
✔ [4267/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues:blueprint (4.3s)
✔ [4268/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder:blueprint (4.3s)
✔ [4269/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy:blueprint (1.8s)
✔ [4271/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (4.7s)
✔ [4272/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor:blueprint (2.6s)
✔ [4273/4276] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (18s)
✔ [4274/4277] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (36s)
ℹ [4275/4277] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (85ms)
info: Blueprint indexing
Build completed successfully (4277 jobs).

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

semantic_module_facts exit - duration 4h 0m · created 6/9/2026, 6:01:39 PM

./.apodeixis/tools/lean-semantic-extract.sh --module-facts

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper: restored compiled static runner cache 96c5b285aa919a69e192314b1734aeb61041a50101be9db784d952ef8cb4ea70
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-409-runtime-semantic_module_facts-1166115-1780999274943416642-3

semantic_extract exit - duration 4h 0m · created 6/9/2026, 6:01:39 PM

./.apodeixis/tools/lean-semantic-extract.sh

lean semantic helper: restored compiled static runner cache 96c5b285aa919a69e192314b1734aeb61041a50101be9db784d952ef8cb4ea70
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-409-runtime-semantic_extract-1166115-1781013685337972919-4