Verification run

Run 43

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

succeeded commit 47d19b91ae7e toolchain lean-v4-30-0 prover lean took 5h 54m · finished 5w ago

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 942 ms · created 6/13/2026, 3:03:11 PM

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

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

git_checkout exit 0 duration 28 ms · created 6/13/2026, 3:03:11 PM

git checkout 47d19b91ae7ed3e5bb49762473a04ed3394e2ee9

Note: switching to '47d19b91ae7ed3e5bb49762473a04ed3394e2ee9'.

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 47d19b9 feat(FKS2): sharp Dawson bound, μ_asymp evaluation, and admissible-curve antitonicity (towards #721) (#1548)

lake_cache exit 0 duration 43s · created 6/13/2026, 3:03:11 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)

info: leancert: cloning https://github.com/alerad/leancert
info: leancert: checking out revision 'fa684975c884d1b699977b1117bbeec9cb999d27'
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%, 14 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8459 = 0%, 8 KB/s], Decompressed: 12
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 11 KB/s], Decompressed: 35
Downloaded: 60 file(s) [attempted 60/8459 = 0%, 55 KB/s], Decompressed: 57
Downloaded: 90 file(s) [attempted 90/8459 = 1%, 185 KB/s], Decompressed: 86
Downloaded: 126 file(s) [attempted 126/8459 = 1%, 387 KB/s], Decompressed: 121
Downloaded: 155 file(s) [attempted 155/8459 = 1%, 98 KB/s], Decompressed: 151
Downloaded: 192 file(s) [attempted 192/8459 = 2%, 227 KB/s], Decompressed: 189
Downloaded: 230 file(s) [attempted 230/8459 = 2%, 286 KB/s], Decompressed: 223
Downloaded: 268 file(s) [attempted 268/8459 = 3%, 280 KB/s], Decompressed: 261
Downloaded: 308 file(s) [attempted 308/8459 = 3%, 342 KB/s], Decompressed: 302
Downloaded: 347 file(s) [attempted 347/8459 = 4%, 24 KB/s], Decompressed: 343
Downloaded: 384 file(s) [attempted 384/8459 = 4%, 43 KB/s], Decompressed: 383
Downloaded: 425 file(s) [attempted 425/8459 = 5%, 304 KB/s], Decompressed: 419
Downloaded: 465 file(s) [attempted 465/8459 = 5%, 852 KB/s], Decompressed: 460
Downloaded: 504 file(s) [attempted 504/8459 = 5%, 247 KB/s], Decompressed: 497
Downloaded: 542 file(s) [attempted 542/8459 = 6%, 72 KB/s], Decompressed: 538
Downloaded: 583 file(s) [attempted 583/8459 = 6%, 34 KB/s], Decompressed: 580
Downloaded: 627 file(s) [attempted 627/8459 = 7%, 157 KB/s], Decompressed: 624
Downloaded: 669 file(s) [attempted 669/8459 = 7%, 340 KB/s], Decompressed: 662
Downloaded: 707 file(s) [attempted 707/8459 = 8%, 29 KB/s], Decompressed: 703
Downloaded: 749 file(s) [attempted 749/8459 = 8%, 241 KB/s], Decompressed: 741
Downloaded: 783 file(s) [attempted 783/8459 = 9%, 148 KB/s], Decompressed: 778
Downloaded: 826 file(s) [attempted 826/8459 = 9%, 1828 KB/s], Decompressed: 823
Downloaded: 867 file(s) [attempted 867/8459 = 10%, 163 KB/s], Decompressed: 866
Downloaded: 907 file(s) [attempted 907/8459 = 10%, 609 KB/s], Decompressed: 902
Downloaded: 949 file(s) [attempted 949/8459 = 11%, 181 KB/s], Decompressed: 946
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 204 KB/s], Decompressed: 984
Downloaded: 1029 file(s) [attempted 1029/8459 = 12%, 312 KB/s], Decompressed: 1025
Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 255 KB/s], Decompressed: 1062
Downloaded: 1110 file(s) [attempted 1110/8459 = 13%, 423 KB/s], Decompressed: 1107
Downloaded: 1151 file(s) [attempted 1151/8459 = 13%, 2098 KB/s], Decompressed: 1148
Downloaded: 1186 file(s) [attempted 1186/8459 = 14%, 995 KB/s], Decompressed: 1182
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 414 KB/s], Decompressed: 1227
Downloaded: 1272 file(s) [attempted 1272/8459 = 15%, 271 KB/s], Decompressed: 1264
Downloaded: 1314 file(s) [attempted 1314/8459 = 15%, 46 KB/s], Decompressed: 1305
Downloaded: 1353 file(s) [attempted 1353/8459 = 15%, 208 KB/s], Decompressed: 1346
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 109 KB/s], Decompressed: 1384
Downloaded: 1432 file(s) [attempted 1432/8459 = 16%, 1365 KB/s], Decompressed: 1429
Downloaded: 1474 file(s) [attempted 1474/8459 = 17%, 341 KB/s], Decompressed: 1470
Downloaded: 1516 file(s) [attempted 1516/8459 = 17%, 1011 KB/s], Decompressed: 1507
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 363 KB/s], Decompressed: 1547
Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 140 KB/s], Decompressed: 1589
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 637 KB/s], Decompressed: 1634
Downloaded: 1682 file(s) [attempted 1682/8459 = 19%, 372 KB/s], Decompressed: 1675
Downloaded: 1723 file(s) [attempted 1723/8459 = 20%, 171 KB/s], Decompressed: 1720
Downloaded: 1764 file(s) [attempted 1764/8459 = 20%, 150 KB/s], Decompressed: 1757
Downloaded: 1798 file(s) [attempted 1798/8459 = 21%, 24 KB/s], Decompressed: 1795
Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 217 KB/s], Decompressed: 1836
Downloaded: 1877 file(s) [attempted 1877/8459 = 22%, 129 KB/s], Decompressed: 1874
Downloaded: 1918 file(s) [attempted 1918/8459 = 22%, 66 KB/s], Decompressed: 1915
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 167 KB/s], Decompressed: 1956
Downloaded: 2000 file(s) [attempted 2000/8459 = 23%, 80 KB/s], Decompressed: 1997
Downloaded: 2041 file(s) [attempted 2041/8459 = 24%, 35 KB/s], Decompressed: 2034
Downloaded: 2077 file(s) [attempted 2077/8459 = 24%, 250 KB/s], Decompressed: 2072
Downloaded: 2117 file(s) [attempted 2117/8459 = 25%, 77 KB/s], Decompressed: 2113
Downloaded: 2158 file(s) [attempted 2158/8459 = 25%, 165 KB/s], Decompressed: 2154
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 515 KB/s], Decompressed: 2195
Downloaded: 2243 file(s) [attempted 2243/8459 = 26%, 111 KB/s], Decompressed: 2236
Downloaded: 2284 file(s) [attempted 2284/8459 = 27%, 808 KB/s], Decompressed: 2281
Downloaded: 2325 file(s) [attempted 2325/8459 = 27%, 321 KB/s], Decompressed: 2322
Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 106 KB/s], Decompressed: 2364
Downloaded: 2403 file(s) [attempted 2403/8459 = 28%, 326 KB/s], Decompressed: 2397
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 1335 KB/s], Decompressed: 2431
Downloaded: 2479 file(s) [attempted 2479/8459 = 29%, 44 KB/s], Decompressed: 2476
Downloaded: 2520 file(s) [attempted 2520/8459 = 29%, 79 KB/s], Decompressed: 2514
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 145 KB/s], Decompressed: 2561
Downloaded: 2613 file(s) [attempted 2613/8459 = 30%, 335 KB/s], Decompressed: 2609
Downloaded: 2649 file(s) [attempted 2649/8459 = 31%, 263 KB/s], Decompressed: 2640
Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 26 KB/s], Decompressed: 2678
Downloaded: 2726 file(s) [attempted 2726/8459 = 32%, 306 KB/s], Decompressed: 2722
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 325 KB/s], Decompressed: 2767
Downloaded: 2817 file(s) [attempted 2817/8459 = 33%, 568 KB/s], Decompressed: 2811
Downloaded: 2856 file(s) [attempted 2856/8459 = 33%, 331 KB/s], Decompressed: 2849
Downloaded: 2892 file(s) [attempted 2892/8459 = 34%, 29 KB/s], Decompressed: 2887
Downloaded: 2931 file(s) [attempted 2931/8459 = 34%, 116 KB/s], Decompressed: 2924
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 39 KB/s], Decompressed: 2965
Downloaded: 3017 file(s) [attempted 3017/8459 = 35%, 617 KB/s], Decompressed: 3013
Downloaded: 3061 file(s) [attempted 3061/8459 = 36%, 2056 KB/s], Decompressed: 3058
Downloaded: 3099 file(s) [attempted 3099/8459 = 36%, 100 KB/s], Decompressed: 3095
Downloaded: 3136 file(s) [attempted 3136/8459 = 37%, 334 KB/s], Decompressed: 3133
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 26 KB/s], Decompressed: 3171
Downloaded: 3218 file(s) [attempted 3218/8459 = 38%, 232 KB/s], Decompressed: 3215
Downloaded: 3256 file(s) [attempted 3256/8459 = 38%, 109 KB/s], Decompressed: 3253
Downloaded: 3297 file(s) [attempted 3297/8459 = 38%, 227 KB/s], Decompressed: 3294
Downloaded: 3338 file(s) [attempted 3338/8459 = 39%, 147 KB/s], Decompressed: 3331
Downloaded: 3383 file(s) [attempted 3383/8459 = 39%, 453 KB/s], Decompressed: 3376
Downloaded: 3417 file(s) [attempted 3417/8459 = 40%, 223 KB/s], Decompressed: 3414
Downloaded: 3460 file(s) [attempted 3460/8459 = 40%, 82 KB/s], Decompressed: 3451
Downloaded: 3499 file(s) [attempted 3499/8459 = 41%, 521 KB/s], Decompressed: 3496
Downloaded: 3544 file(s) [attempted 3544/8459 = 41%, 1140 KB/s], Decompressed: 3540
Downloaded: 3587 file(s) [attempted 3587/8459 = 42%, 569 KB/s], Decompressed: 3574
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 234 KB/s], Decompressed: 3615
Downloaded: 3663 file(s) [attempted 3663/8459 = 43%, 261 KB/s], Decompressed: 3657
Downloaded: 3704 file(s) [attempted 3704/8459 = 43%, 196 KB/s], Decompressed: 3701
Downloaded: 3749 file(s) [attempted 3749/8459 = 44%, 234 KB/s], Decompressed: 3742
Downloaded: 3790 file(s) [attempted 3790/8459 = 44%, 133 KB/s], Decompressed: 3783
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 409 KB/s], Decompressed: 3817
Downloaded: 3862 file(s) [attempted 3862/8459 = 45%, 815 KB/s], Decompressed: 3855
Downloaded: 3903 file(s) [attempted 3903/8459 = 46%, 398 KB/s], Decompressed: 3900
Downloaded: 3947 file(s) [attempted 3947/8459 = 46%, 365 KB/s], Decompressed: 3944
Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 676 KB/s], Decompressed: 3978
Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 111 KB/s], Decompressed: 4023
Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 269 KB/s], Decompressed: 4054
Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 355 KB/s], Decompressed: 4095
Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 37 KB/s], Decompressed: 4143
Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 313 KB/s], Decompressed: 4190
Downloaded: 4235 file(s) [attempted 4235/8459 = 50%, 83 KB/s], Decompressed: 4228
Downloaded: 4279 file(s) [attempted 4279/8459 = 50%, 71 KB/s], Decompressed: 4276
Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 361 KB/s], Decompressed: 4314
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 83 KB/s], Decompressed: 4348
Downloaded: 4393 file(s) [attempted 4393/8459 = 51%, 217 KB/s], Decompressed: 4389
Downloaded: 4431 file(s) [attempted 4431/8459 = 52%, 96 KB/s], Decompressed: 4427
Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 368 KB/s], Decompressed: 4468
Downloaded: 4509 file(s) [attempted 4509/8459 = 53%, 249 KB/s], Decompressed: 4505
Downloaded: 4550 file(s) [attempted 4550/8459 = 53%, 1200 KB/s], Decompressed: 4546
Downloaded: 4588 file(s) [attempted 4588/8459 = 54%, 276 KB/s], Decompressed: 4581
Downloaded: 4625 file(s) [attempted 4625/8459 = 54%, 272 KB/s], Decompressed: 4622
Downloaded: 4670 file(s) [attempted 4670/8459 = 55%, 104 KB/s], Decompressed: 4666
Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 334 KB/s], Decompressed: 4707
Downloaded: 4752 file(s) [attempted 4752/8459 = 56%, 110 KB/s], Decompressed: 4748
Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 58 KB/s], Decompressed: 4786
Downloaded: 4830 file(s) [attempted 4830/8459 = 57%, 75 KB/s], Decompressed: 4824
Downloaded: 4872 file(s) [attempted 4872/8459 = 57%, 118 KB/s], Decompressed: 4868
Downloaded: 4913 file(s) [attempted 4913/8459 = 58%, 227 KB/s], Decompressed: 4909
Downloaded: 4950 file(s) [attempted 4950/8459 = 58%, 449 KB/s], Decompressed: 4947
Downloaded: 4991 file(s) [attempted 4991/8459 = 59%, 1101 KB/s], Decompressed: 4988
Downloaded: 5039 file(s) [attempted 5039/8459 = 59%, 230 KB/s], Decompressed: 5036
Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 115 KB/s], Decompressed: 5077
Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 48 KB/s], Decompressed: 5118
Downloaded: 5162 file(s) [attempted 5162/8459 = 61%, 1281 KB/s], Decompressed: 5156
Downloaded: 5203 file(s) [attempted 5203/8459 = 61%, 26 KB/s], Decompressed: 5197
Downloaded: 5242 file(s) [attempted 5242/8459 = 61%, 83 KB/s], Decompressed: 5238
Downloaded: 5286 file(s) [attempted 5286/8459 = 62%, 356 KB/s], Decompressed: 5282
Downloaded: 5327 file(s) [attempted 5327/8459 = 62%, 1053 KB/s], Decompressed: 5323
Downloaded: 5364 file(s) [attempted 5364/8459 = 63%, 890 KB/s], Decompressed: 5361
Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 375 KB/s], Decompressed: 5402
Downloaded: 5446 file(s) [attempted 5446/8459 = 64%, 726 KB/s], Decompressed: 5443
Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 105 KB/s], Decompressed: 5481
Downloaded: 5525 file(s) [attempted 5525/8459 = 65%, 292 KB/s], Decompressed: 5522
Downloaded: 5566 file(s) [attempted 5566/8459 = 65%, 82 KB/s], Decompressed: 5559
Downloaded: 5607 file(s) [attempted 5607/8459 = 66%, 269 KB/s], Decompressed: 5604
Downloaded: 5648 file(s) [attempted 5648/8459 = 66%, 186 KB/s], Decompressed: 5642
Downloaded: 5689 file(s) [attempted 5689/8459 = 67%, 147 KB/s], Decompressed: 5686
Downloaded: 5727 file(s) [attempted 5727/8459 = 67%, 713 KB/s], Decompressed: 5724
Downloaded: 5772 file(s) [attempted 5772/8459 = 68%, 473 KB/s], Decompressed: 5768
Downloaded: 5813 file(s) [attempted 5813/8459 = 68%, 125 KB/s], Decompressed: 5806
Downloaded: 5850 file(s) [attempted 5850/8459 = 69%, 648 KB/s], Decompressed: 5843
Downloaded: 5891 file(s) [attempted 5891/8459 = 69%, 303 KB/s], Decompressed: 5888
Downloaded: 5932 file(s) [attempted 5932/8459 = 70%, 36 KB/s], Decompressed: 5929
Downloaded: 5977 file(s) [attempted 5977/8459 = 70%, 524 KB/s], Decompressed: 5974
Downloaded: 6018 file(s) [attempted 6018/8459 = 71%, 233 KB/s], Decompressed: 6015
Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 103 KB/s], Decompressed: 6052
Downloaded: 6097 file(s) [attempted 6097/8459 = 72%, 735 KB/s], Decompressed: 6093
Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 231 KB/s], Decompressed: 6134
Downloaded: 6182 file(s) [attempted 6182/8459 = 73%, 132 KB/s], Decompressed: 6179
Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 529 KB/s], Decompressed: 6220
Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 36 KB/s], Decompressed: 6251
Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 2516 KB/s], Decompressed: 6295
Downloaded: 6343 file(s) [attempted 6343/8459 = 74%, 1065 KB/s], Decompressed: 6340
Downloaded: 6384 file(s) [attempted 6384/8459 = 75%, 125 KB/s], Decompressed: 6377
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 168 KB/s], Decompressed: 6425
Downloaded: 6466 file(s) [attempted 6466/8459 = 76%, 131 KB/s], Decompressed: 6459
Downloaded: 6507 file(s) [attempted 6507/8459 = 76%, 79 KB/s], Decompressed: 6504
Downloaded: 6550 file(s) [attempted 6550/8459 = 77%, 552 KB/s], Decompressed: 6545
Downloaded: 6590 file(s) [attempted 6590/8459 = 77%, 132 KB/s], Decompressed: 6586
Downloaded: 6628 file(s) [attempted 6628/8459 = 78%, 63 KB/s], Decompressed: 6624
Downloaded: 6668 file(s) [attempted 6668/8459 = 78%, 681 KB/s], Decompressed: 6661
Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 63 KB/s], Decompressed: 6702
Downloaded: 6745 file(s) [attempted 6745/8459 = 79%, 244 KB/s], Decompressed: 6740
Downloaded: 6787 file(s) [attempted 6787/8459 = 80%, 243 KB/s], Decompressed: 6778
Downloaded: 6823 file(s) [attempted 6823/8459 = 80%, 1477 KB/s], Decompressed: 6819
Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 116 KB/s], Decompressed: 6860
Downloaded: 6908 file(s) [attempted 6908/8459 = 81%, 778 KB/s], Decompressed: 6901
Downloaded: 6944 file(s) [attempted 6944/8459 = 82%, 72 KB/s], Decompressed: 6940
Downloaded: 6987 file(s) [attempted 6987/8459 = 82%, 110 KB/s], Decompressed: 6983
Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 353 KB/s], Decompressed: 7029
Downloaded: 7072 file(s) [attempted 7072/8459 = 83%, 253 KB/s], Decompressed: 7062
Downloaded: 7107 file(s) [attempted 7107/8459 = 84%, 593 KB/s], Decompressed: 7103
Downloaded: 7147 file(s) [attempted 7147/8459 = 84%, 432 KB/s], Decompressed: 7141
Downloaded: 7188 file(s) [attempted 7188/8459 = 84%, 66 KB/s], Decompressed: 7185
Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 558 KB/s], Decompressed: 7229
Downloaded: 7277 file(s) [attempted 7277/8459 = 86%, 297 KB/s], Decompressed: 7274
Downloaded: 7309 file(s) [attempted 7309/8459 = 86%, 36 KB/s], Decompressed: 7305
Downloaded: 7350 file(s) [attempted 7350/8459 = 86%, 888 KB/s], Decompressed: 7346
Downloaded: 7390 file(s) [attempted 7390/8459 = 87%, 182 KB/s], Decompressed: 7387
Downloaded: 7431 file(s) [attempted 7431/8459 = 87%, 162 KB/s], Decompressed: 7425
Downloaded: 7472 file(s) [attempted 7472/8459 = 88%, 94 KB/s], Decompressed: 7466
Downloaded: 7518 file(s) [attempted 7518/8459 = 88%, 67 KB/s], Decompressed: 7514
Downloaded: 7560 file(s) [attempted 7560/8459 = 89%, 232 KB/s], Decompressed: 7551
Downloaded: 7593 file(s) [attempted 7593/8459 = 89%, 115 KB/s], Decompressed: 7589
Downloaded: 7633 file(s) [attempted 7633/8459 = 90%, 207 KB/s], Decompressed: 7630
Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 375 KB/s], Decompressed: 7671
Downloaded: 7715 file(s) [attempted 7715/8459 = 91%, 433 KB/s], Decompressed: 7712
Downloaded: 7757 file(s) [attempted 7757/8459 = 91%, 2001 KB/s], Decompressed: 7753
Downloaded: 7798 file(s) [attempted 7798/8459 = 92%, 163 KB/s], Decompressed: 7794
Downloaded: 7842 file(s) [attempted 7842/8459 = 92%, 460 KB/s], Decompressed: 7835
Downloaded: 7876 file(s) [attempted 7876/8459 = 93%, 669 KB/s], Decompressed: 7873
Downloaded: 7917 file(s) [attempted 7917/8459 = 93%, 801 KB/s], Decompressed: 7914
Downloaded: 7958 file(s) [attempted 7958/8459 = 94%, 56 KB/s], Decompressed: 7955
Downloaded: 7996 file(s) [attempted 7996/8459 = 94%, 386 KB/s], Decompressed: 7993
Downloaded: 8041 file(s) [attempted 8041/8459 = 95%, 804 KB/s], Decompressed: 8037
Downloaded: 8082 file(s) [attempted 8082/8459 = 95%, 119 KB/s], Decompressed: 8078
Downloaded: 8116 file(s) [attempted 8116/8459 = 95%, 367 KB/s], Decompressed: 8112
Downloaded: 8157 file(s) [attempted 8157/8459 = 96%, 188 KB/s], Decompressed: 8153
Downloaded: 8198 file(s) [attempted 8198/8459 = 96%, 355 KB/s], Decompressed: 8195
Downloaded: 8240 file(s) [attempted 8240/8459 = 97%, 111 KB/s], Decompressed: 8232
Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 1081 KB/s], Decompressed: 8273
Downloaded: 8319 file(s) [attempted 8319/8459 = 98%, 303 KB/s], Decompressed: 8311
Downloaded: 8352 file(s) [attempted 8352/8459 = 98%, 316 KB/s], Decompressed: 8349
Downloaded: 8396 file(s) [attempted 8396/8459 = 99%, 99 KB/s], Decompressed: 8393
Downloaded: 8441 file(s) [attempted 8441/8459 = 99%, 108 KB/s], Decompressed: 8438
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 108 KB/s], Decompressed: 8455

lean_checker exit 0 duration 44m 20s · created 6/13/2026, 3:03:11 PM

lake build

ℹ [3540/3572] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3555/3572] 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`
⚠ [3692/3712] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3702/3712] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3760/3768] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3762/3768] 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`
✔ [3763/3768] Built LeanCert.Core.Interval (16s)
✔ [3765/3768] Built LeanCert.Core.IntervalRat.Basic (5.5s)
✔ [3766/3768] Built LeanCert.Tactic.IntervalAuto.Types (2.7s)
✔ [3767/3778] Built LeanCert.Tactic.IntervalAuto.Norm (2.8s)
✔ [3772/3778] Built LeanCert.Core.Expr (4.1s)
✔ [3773/3779] Built LeanCert.Meta.Numeral (2.9s)
✔ [3774/3779] Built LeanCert.Meta.ToExpr (3.6s)
✔ [3775/3779] Built LeanCert.Tactic.IntervalAuto.Extract (2.3s)
✔ [3776/3779] Built LeanCert.Core.Support (2.5s)
✔ [3777/3780] Built LeanCert.Tactic.IntervalAuto.Parse (3.8s)
✔ [3778/3780] Built LeanCert.Tactic.IntervalAuto.Diagnostic (2.4s)
✔ [3779/3781] Built LeanCert.Core.IntervalRat.Transcendental (3.5s)
✔ [3780/3781] Built LeanCert.Core.IntervalRat.LogReduction (3.5s)
✔ [3794/3804] Built LeanCert.Core.DerivativeIntervals (2.5s)
✔ [3796/3806] Built LeanCert.Core.TrigReduction (2.8s)
✔ [3797/3806] Built LeanCert.Core.Taylor (4.6s)
✔ [3798/3807] Built LeanCert.Core.IntervalRat.Taylor (9.6s)
✔ [3799/3808] Built LeanCert.Core.IntervalRat.TrigReduced (2.5s)
✔ [3800/3809] Built LeanCert.Core.IntervalReal (2.3s)
✔ [3801/3810] Built LeanCert.Core.IntervalRealEndpoints (3.1s)
✔ [3802/3810] Built LeanCert.Engine.Eval.Core (4.9s)
✔ [3803/3812] Built LeanCert.Engine.Eval.Extended (3.3s)
✔ [3804/3817] Built LeanCert.Tactic.Bound.Lemmas (2.5s)
✔ [3805/3817] Built LeanCert.Contrib.Sinc (3.2s)
✔ [3806/3817] Built LeanCert.Engine.IntervalEval (2.1s)
✔ [3807/3817] Built LeanCert.Engine.AD.Basic (2.2s)
✔ [3808/3817] Built LeanCert.Engine.AD.Transcendental (3.2s)
✔ [3809/3817] Built LeanCert.Engine.AD.Eval (2.2s)
✔ [3810/3817] Built LeanCert.Engine.AD.Correctness (2.8s)
✔ [3811/3818] Built LeanCert.Engine.AD.Computable (2.7s)
✔ [3812/3818] Built LeanCert.Engine.AD.PartialCorrectness (4.8s)
✔ [3813/3818] Built LeanCert.Engine.TaylorModel.Core (5.2s)
✔ [3814/3818] Built LeanCert.Engine.AD (2.0s)
✔ [3815/3820] Built LeanCert.Meta.ProveSupported (2.7s)
✔ [3816/3821] Built LeanCert.Tactic.IntervalAuto.ProveCommon (3.7s)
✔ [3818/3821] Built LeanCert.Tactic.IntervalAuto.Basic (2.1s)
✔ [3819/3821] Built LeanCert.Engine.TaylorModel.ExpLog (4.0s)
✔ [3820/3822] Built LeanCert.Engine.TaylorModel.Trig (6.1s)
✔ [3829/3837] Built LeanCert.Engine.TaylorModel.Special (2.3s)
✔ [3830/3837] Built LeanCert.Engine.Integrate (4.1s)
✔ [3831/3837] Built LeanCert.Engine.TaylorModel.Hyperbolic (7.1s)
✔ [3832/3840] Built LeanCert.Engine.TaylorModel.Integral (2.7s)
✔ [3833/3840] Built LeanCert.Engine.TaylorModel.Functions (2.1s)
✔ [3834/3840] Built LeanCert.Core.Dyadic (2.2s)
✔ [3835/3840] Built LeanCert.Engine.TaylorModel.Expr (3.4s)
✔ [3836/3840] Built LeanCert.Core.IntervalDyadic (4.0s)
✔ [3837/3844] Built LeanCert.Engine.TaylorModel (2.1s)
✔ [3838/3844] Built LeanCert.Engine.IntervalEvalDyadic (3.2s)
✔ [3839/3845] Built LeanCert.Engine.IntervalEvalRefined (2.9s)
✔ [3840/3845] Built LeanCert.Engine.Affine.Basic (4.0s)
✔ [3841/3845] Built LeanCert.Engine.Optimization.Box (2.4s)
✔ [3842/3848] Built LeanCert.Engine.Affine.Nonlinear (3.4s)
✔ [3843/3848] Built LeanCert.Engine.Affine.Transcendental (2.9s)
✔ [3844/3848] Built LeanCert.Engine.Optimize (4.2s)
✔ [3845/3849] Built LeanCert.Engine.IntervalEvalAffine (2.0s)
✔ [3846/3850] Built LeanCert.Engine.Optimization.Gradient (3.7s)
✔ [3847/3850] Built LeanCert.Engine.RootFinding.Basic (3.5s)
✔ [3848/3851] Built LeanCert.Engine.Optimization.Global (10s)
✔ [3849/3852] Built LeanCert.Engine.RootFinding.Bisection (3.4s)
✔ [3850/3854] Built LeanCert.Engine.RootFinding.Newton (3.2s)
✔ [3851/3855] Built LeanCert.Engine.RootFinding.MVTBounds (3.0s)
✔ [3852/3855] Built LeanCert.Engine.RootFinding.Contraction (3.6s)
✔ [3853/3855] Built LeanCert.Meta.ProveContinuous (2.0s)
✔ [3854/3857] Built LeanCert.Engine.RootFinding.Main (2.1s)
✔ [3855/3858] Built LeanCert.Validity.Bounds.Core (2.4s)
✔ [3856/3860] Built LeanCert.Validity.Bounds.WithInv (2.3s)
✔ [3857/3862] Built LeanCert.Validity.Bounds.Smart (2.4s)
✔ [3858/3863] Built LeanCert.Validity.Bounds.Bridge (2.5s)
✔ [3859/3863] Built LeanCert.Validity.Integration (3.3s)
✔ [3860/3865] Built LeanCert.Validity.Bounds.Basic (2.1s)
✔ [3861/3865] Built LeanCert.Validity.DyadicBounds (2.4s)
✔ [3862/3866] Built LeanCert.Validity.Bounds (4.1s)
✔ [3863/3867] Built LeanCert.Engine.Optimization.BoundVerify (2.5s)
✔ [3864/3867] Built LeanCert.Tactic.IntervalAuto.Multivariate (3.7s)
✔ [3865/3868] Built LeanCert.Tactic.IntervalAuto.Bound (20s)
✔ [3866/3869] Built LeanCert.Tactic.IntervalAuto.OptBound (2.3s)
✔ [3867/3870] Built LeanCert.Tactic.IntervalAuto.RootBound (2.5s)
✔ [3868/3875] Built LeanCert.Tactic.IntervalAuto.PointIneq (11s)
✔ [3869/3875] Built LeanCert.Tactic.IntervalAuto.Subdiv (5.5s)
✔ [3870/3875] Built LeanCert.Tactic.IntervalAuto.Adaptive (5.4s)
✔ [3871/3879] Built LeanCert.Tactic.IntervalAuto (2.4s)
✔ [3872/3885] Built PrimeNumberTheoremAnd.IEANTN.LogTables (7.2s)
✔ [3873/3885] Built LeanCert.Engine.TaylorModel.Log1p (4.2s)
✔ [3874/3885] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.5s)
✔ [3877/3885] Built LeanCert.Examples.Li2Base (2.9s)
⚠ [3878/3887] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (8.4s)
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`
⚠ [3880/3888] Built LeanCert.Examples.Li2Bounds (2.4s)
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3883/3890] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (2.0s)
✔ [3886/3890] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (6.0s)
✔ [3889/3892] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (8.8s)
⚠ [4012/4020] Built PrimeNumberTheoremAnd.IEANTN.Buthe (11s)
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`
⚠ [4013/4020] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (14s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4014/4021] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (90s)
⚠ [4015/4021] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (10s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4016/4021] Built LeanCert.Engine.FinSumDyadic (2.9s)
✔ [4017/4021] Built LeanCert.Examples.BKLNW_a2_base (4.2s)
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4019/4049] Built LeanCert.Engine.WitnessSum (2.5s)
✔ [4020/4049] Built LeanCert.Tactic.VecUtil (2.2s)
✔ [4021/4050] Built LeanCert.Engine.ReflectiveSum (4.2s)
✔ [4022/4050] Built LeanCert.Tactic.FinSumExpand (1.6s)
✔ [4024/4052] Built LeanCert.Examples.BKLNW_a2_reflective (92s)
✔ [4025/4053] Built LeanCert.Examples.BKLNW_a2_bounds (2.8s)
✔ [4026/4056] Built LeanCert.Examples.BKLNW_a2_pow2 (2.4s)
✔ [4029/4063] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.4s)
✔ [4032/4063] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.7s)
⚠ [4033/4063] 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`
✔ [4034/4063] Built LeanCert.Engine.Chebyshev.Psi (2.8s)
✔ [4035/4063] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (3.6s)
✔ [4037/4063] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4038/4063] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4039/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (266s)
✔ [4040/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (187s)
✔ [4041/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (160s)
✔ [4042/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (147s)
✔ [4043/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (110s)
✔ [4044/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (92s)
✔ [4045/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (85s)
✔ [4046/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (86s)
✔ [4047/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (77s)
✔ [4048/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (63s)
✔ [4049/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (65s)
✔ [4050/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (57s)
✔ [4051/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.2s)
✔ [4052/4065] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (35s)
✔ [4053/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (17s)
⚠ [4054/4070] 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`
✔ [4055/4070] Built LeanCert.Engine.ChebyshevPsi (2.1s)
⚠ [4056/4070] 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`
✔ [4058/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (116s)
⚠ [4060/4070] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (52s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
✔ [4063/4071] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (15s)
⚠ [4064/4071] 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`
✔ [4066/4072] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (75s)
✔ [4068/4073] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (44s)
✔ [4069/4073] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (2.8s)
✔ [4071/4092] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
⚠ [4082/4092] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4087/4100] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.2s)
⚠ [4089/4135] 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`
⚠ [4109/4139] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.1s)
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`
⚠ [4117/4139] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.3s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4124/4150] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
⚠ [4125/4150] 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`
✔ [4129/4152] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.4s)
✔ [4130/4152] Built LeanCert.Engine.Chebyshev.Theta (5.1s)
⚠ [4131/4152] 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`
✔ [4141/4152] Built LeanCert.Engine.ChebyshevTheta (2.1s)
ℹ [4146/4152] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (18s)
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.
✔ [4148/4152] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
✔ [4149/4152] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard (3.7s)
⚠ [4150/4152] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (10s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:128:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:165:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:273:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:532:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:575:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1975:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2001:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2607:8: declaration uses `sorry`
✔ [4151/4152] Built PrimeNumberTheoremAnd (2.7s)
Build completed successfully (4152 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 7m 22s · created 6/13/2026, 3:03:11 PM

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (766ms)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (539ms)
✔ [33/45] Built Cli:c.o (63ms)
ℹ [3591/3608] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3617/3642] 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`
⚠ [3762/3787] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3778/3787] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3838/3860] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3840/3860] 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`
✔ [3955/3975] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.7s)
✔ [3959/3978] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.3s)
⚠ [3960/3978] 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`
✔ [3964/3980] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
⚠ [3965/3980] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3972/3980] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (5.7s)
✔ [3977/3982] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.2s)
✔ [3979/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.4s)
⚠ [4099/4114] 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`
✔ [4102/4114] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (5.9s)
⚠ [4105/4118] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4107/4118] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4110/4129] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4111/4129] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (18s)
✔ [4112/4129] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.4s)
⚠ [4113/4129] 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`
✔ [4116/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (23s)
✔ [4129/4192] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.7s)
⚠ [4131/4192] 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`
✔ [4135/4201] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (2.8s)
⚠ [4154/4201] 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`
✔ [4156/4201] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.3s)
⚠ [4158/4201] 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`
⚠ [4161/4201] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3779:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4434:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4456:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4483:8: declaration uses `sorry`
⚠ [4167/4201] 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`
✔ [4169/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (2.7s)
✔ [4170/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (2.7s)
✔ [4172/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (2.8s)
✔ [4173/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (2.8s)
✔ [4174/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (2.8s)
✔ [4175/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (2.7s)
✔ [4176/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (2.8s)
✔ [4177/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.8s)
✔ [4178/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (2.8s)
✔ [4179/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (2.7s)
✔ [4180/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (2.8s)
✔ [4181/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (2.7s)
✔ [4182/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (2.7s)
✔ [4183/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (2.8s)
✔ [4184/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (2.7s)
✔ [4185/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.8s)
✔ [4186/4202] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (2.8s)
✔ [4187/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (30s)
✔ [4190/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (2.8s)
✔ [4192/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (17s)
✔ [4193/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4196/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.8s)
✔ [4198/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4201/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (2.8s)
✔ [4205/4297] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (10s)
⚠ [4215/4297] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4221/4311] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (2.8s)
⚠ [4222/4311] 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`
✔ [4242/4318] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
⚠ [4243/4318] 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`
✔ [4270/4328] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.3s)
⚠ [4271/4328] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4284/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.6s)
✔ [4290/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
⚠ [4291/4340] 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`
⚠ [4295/4340] 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`
✔ [4308/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.7s)
ℹ [4310/4340] 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.
✔ [4325/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (7.3s)
✔ [4333/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4334/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard:blueprint (2.6s)
⚠ [4335/4340] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:128:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:165:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:273:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:532:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:575:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1975:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2001:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2607:8: declaration uses `sorry`
✔ [4336/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (43s)
✔ [4338/4340] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (2.8s)
ℹ [4340/4341] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (60ms)
info: Blueprint indexing
Build completed successfully (4341 jobs).

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

semantic_extract exit 0 duration 4m 26s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
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: stored compiled static runner cache df4f47a1f40057295e5d228a4169acd70354fdf16085fd2aa42843632abcfe54
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 4m 32s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)

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: stored compiled static runner cache 68b45331a76823f967cb09674b9bd2e3fd133548341604c0448748a77aea45a5
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 4m 10s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)

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: stored compiled static runner cache e031231ed26a31b97c4284504ced1519a03fcc3ca1b59d1eef1f1bc83a65527d
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 24s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)

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: stored compiled static runner cache 4ccba06d09a0f97cea95b416b35f23222df57ef5899d080815e7a628e13055f2
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 4m 11s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)

lean semantic helper: restored compiled static runner cache a9be9aa136ac0e1b9ed39ca9fe3c6732a14c79aca987bd52e0d55b84e59ae3cf
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 49s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)

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: stored compiled static runner cache f9f3ecf0c0dd6e37e844f52c41e8d044b1da492592aaee8c3b3344fccd823126
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 4s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)

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: stored compiled static runner cache bcd48acbe831054ca420dc8f177fee58f273f2906e6fffb0d52aff3f2880c44b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 38s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)

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: stored compiled static runner cache e045867cd937d200b3cb849937eacd765989a9fcd93ba8e19d50470255813501
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 38s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)

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: stored compiled static runner cache 5498ebc1dfb9e7f032a51398d0b9992be4c566a93b17869e6d33452522aa36af
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 36s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)

lean semantic helper: restored compiled static runner cache ab48e153fa222e749af2c2ce00b7f3ab058201c977792d7c92b21abf6bb4ef3b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 29s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)

lean semantic helper: restored compiled static runner cache b4760a95cb83f6f313e92d0899f90c0a9d398820352e08241a61c6ea77ad4d37
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 35s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)

lean semantic helper: restored compiled static runner cache 395e475866a73f2ae513581b343de5074d6f70f10184712f6182dd2fdd60b0e3
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 28s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)

lean semantic helper: restored compiled static runner cache 4402c3a67a5478be83cacb232992831b3c8faac62dd3ffe231caba88fe2962c3
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 2s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)

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: stored compiled static runner cache 1c8c6a06d3e19123aff7fe635de03d9b89cf997b328298eef4c0dad484ca98ce
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 39s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)

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: stored compiled static runner cache 0fb0054909c6999a77a451660d80c1e877d1ede4acf80d1a6b9996d2622570fc
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 27s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)

lean semantic helper: restored compiled static runner cache a435981e9150db1553b61dc1c48337081a4863cbc469b5864f2c22b0a45c3466
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 3s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)

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: stored compiled static runner cache 3597c4bca1ad08f341c76835d9a78b271e633e63ec2d40c57863de56a9a9e46d
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 28s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00017)

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: stored compiled static runner cache 19dde6b6d0649b703331843e44fc9025d00e26c1c06f63716d6beb84ff56dc88
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 57s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018)

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: stored compiled static runner cache bf5ae48dd69ecd3f5814f56412a447e5ae1fcb1bdfd6c64538cdc2bfd5c6f958
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 51s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00019)

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: stored compiled static runner cache c920ddefe15ba0d3843b73faed99c0d721921d213481e9b5478584c6c71f8f3e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 57s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00020)

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: stored compiled static runner cache c9954f52cf3fdbafcc651becddd06ea36c51ce1820210efced9800d103786fc8
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 57s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00021)

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: stored compiled static runner cache 7989cba604a929229ba3cb25caff1ab7aea90b56bccdad9a9dfc96a13c3c0b01
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 52s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00022)

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: stored compiled static runner cache f613cfb20c0ac57237f78d51c44746ba9bd538c43ffd4753e0cce9b60550dd6b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 6s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00023)

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: stored compiled static runner cache 9abf44024c74beed4061b5cd0605d96139fa2b4aaec878f1fd754e3185c48413
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 18s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00024)

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: stored compiled static runner cache 6c77834e88b5c33ad4da8fad6e54c12129f47549de3c9abd65f06df32f2eddd7
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 26s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00025)

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: stored compiled static runner cache 1b2ed8cd65aeec3cbf46199acbf485f13ed4736010fa7db31af292aa7e6534c3
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 20s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00026)

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: stored compiled static runner cache 52800dc2daa779c13b2ed99f531fec8831e52756066df5171557c1b74236a5ce
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 17s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00027)

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: stored compiled static runner cache 8d1b9112eaff61ca0deab6226435aca6c513f132acc04e1989c4f85e03ad7492
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 22s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00028)

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: stored compiled static runner cache 6d64bd7e2555fadba109a94f03e03424ee242b8eddd2899539d8e629a975311a
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 34s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00029)

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: stored compiled static runner cache da91e35c55f1c514b3a5b9a1fd9c96c512db9e815532e5214163753342002b86
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 34s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00030)

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: stored compiled static runner cache 1d5c9fdf840ed7fdd9b7ca6a6ea1a2a7e143a244c4920d41eae4b1af4ea5215c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 29s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00031)

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: stored compiled static runner cache 33e74256677bf5ed7806619e3d46f651e2815d6c3ef8547c32f39cfde28b4d05
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 35s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00032)

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: stored compiled static runner cache 14796fbdac5b0d69232dafb70c4a4ad27e875f365d85de2d78c17b291bcdf771
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 29s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00033)

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: stored compiled static runner cache 84722e59ab9e8001b283fece09c5b6fe762a1e4636e4a43faae13b6d1b733f87
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 31s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00034)

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: stored compiled static runner cache 6558ffc83723192252bca414276ed3cb6f49e80c460860443146d70bc73789fc
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 27s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00035)

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: stored compiled static runner cache a58fdf40c19441eec4aaf776c1c7537c6ea562d9ef45388ac8773e65291b336c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 24s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00036)

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: stored compiled static runner cache ae6f4a6d079f026639adec07402129dc70497aeee1b4a12c0270e9a041397afb
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 50s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00037)

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: stored compiled static runner cache 9f74e608d02b28bcbb44a94e740668444b39baca34797007c2a46e7843711093
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 53s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00038)

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: stored compiled static runner cache 9b71e2dc3b5c16d5ff9f4e8c5755aea74240d14c40b8cc48dc055357372577e3
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 2s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00039)

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: stored compiled static runner cache 8490d3ed3808dab8b345ed995a799e2ea51539e689d6892b3e6f39745cfba6a1
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 10s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00040)

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: stored compiled static runner cache b3812fe51de865a3569c7da634aa92f2842f3d464ebad8e51310047eb9a09f98
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 7m 28s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00041)

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: stored compiled static runner cache bbe07079ba8dbb90e38cd884657f474a74bf51c293d9a1bbbe23609027c8fd8d
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 32s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00042)

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: stored compiled static runner cache 9e9633427a0c107c856333fa76cdaf21fbb39bcd219055c91ceb279fba264482
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 55s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00043)

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: stored compiled static runner cache 093f1dd424596f4974ef70020a3ed234b68cfac18e327db605a8442d8ce6d9c5
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 56s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00044)

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: stored compiled static runner cache 65d02e0b45322095024ccee30e0f39a2caf4226f61fb72d40d12181c0886960a
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 2s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00045)

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: stored compiled static runner cache 33787c75d11c15367f5d49c2265a1d034dc457c97cb8b3959964a39cfb1f21b4
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 16s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00046)

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: stored compiled static runner cache 2e3431b9565c0e0c9d1a3d1d9e0016a53323d5d3cfcfc273028183496df1d01d
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 5m 50s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00047)

lean semantic helper: restored compiled static runner cache 90f3fc0f5c7381426e827cb32c9c2b80a878b4d83d4cf63860fc79351d390e0f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 3s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00048)

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: stored compiled static runner cache 0f97991b85bef3524033ba6e1735da09ba007ceef52df5cf440c2d39593ba580
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

semantic_extract exit 0 duration 6m 12s · created 6/13/2026, 3:03:11 PM

./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00049)

lean semantic helper: restored compiled static runner cache 11c9da964b9868851a044d0f6c6083776b2612db4ab6e78036a85cdda3549898
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes