Verification run

Run 10

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit 58ad140e0f83 toolchain lean-v4-30-0 prover lean took 4h 18m · finished 6w ago

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

Open project

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 707 ms · created 6/6/2026, 3:22:32 AM

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

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

git_checkout exit 0 duration 34 ms · created 6/6/2026, 3:22:32 AM

git checkout 58ad140e0f835b1f8e152cef25bcb1880a460420

Note: switching to '58ad140e0f835b1f8e152cef25bcb1880a460420'.

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 58ad140 chore(deps): bump actions/checkout from 6.0.2 to 6.0.3 (#1481)

lake_cache exit 0 duration 43s · created 6/6/2026, 3:22:32 AM

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: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision 'beeecef76cb3c72e8710df6dcf693d59e69472af'
info: leancert: cloning https://github.com/alerad/leancert
info: leancert: checking out revision '77fd0c1e9e215f7abd5dc50b67b02faffcc8cca6'
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
info: LeanArchitect: cloning https://github.com/hanwenzhu/LeanArchitect.git
info: LeanArchitect: checking out revision 'b72ae37b08d264cf371f164f4ba60c5257c17727'
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8459 = 0%, 4 KB/s], Decompressed: 14
Downloaded: 44 file(s) [attempted 44/8459 = 0%, 28 KB/s], Decompressed: 42
Downloaded: 70 file(s) [attempted 70/8459 = 0%, 42 KB/s], Decompressed: 65
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 240 KB/s], Decompressed: 97
Downloaded: 134 file(s) [attempted 134/8459 = 1%, 343 KB/s], Decompressed: 131
Downloaded: 169 file(s) [attempted 169/8459 = 1%, 275 KB/s], Decompressed: 162
Downloaded: 200 file(s) [attempted 200/8459 = 2%, 83 KB/s], Decompressed: 196
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 956 KB/s], Decompressed: 237
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 1014 KB/s], Decompressed: 278
Downloaded: 326 file(s) [attempted 326/8459 = 3%, 102 KB/s], Decompressed: 323
Downloaded: 371 file(s) [attempted 371/8459 = 4%, 288 KB/s], Decompressed: 367
Downloaded: 408 file(s) [attempted 408/8459 = 4%, 76 KB/s], Decompressed: 405
Downloaded: 441 file(s) [attempted 441/8459 = 5%, 757 KB/s], Decompressed: 432
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 576 KB/s], Decompressed: 480
Downloaded: 521 file(s) [attempted 521/8459 = 6%, 795 KB/s], Decompressed: 514
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 28 KB/s], Decompressed: 559
Downloaded: 607 file(s) [attempted 607/8459 = 7%, 157 KB/s], Decompressed: 603
Downloaded: 651 file(s) [attempted 651/8459 = 7%, 128 KB/s], Decompressed: 641
Downloaded: 683 file(s) [attempted 683/8459 = 8%, 352 KB/s], Decompressed: 679
Downloaded: 723 file(s) [attempted 723/8459 = 8%, 461 KB/s], Decompressed: 720
Downloaded: 768 file(s) [attempted 768/8459 = 9%, 143 KB/s], Decompressed: 765
Downloaded: 809 file(s) [attempted 809/8459 = 9%, 102 KB/s], Decompressed: 802
Downloaded: 843 file(s) [attempted 843/8459 = 9%, 96 KB/s], Decompressed: 840
Downloaded: 884 file(s) [attempted 884/8459 = 10%, 946 KB/s], Decompressed: 881
Downloaded: 925 file(s) [attempted 925/8459 = 10%, 348 KB/s], Decompressed: 922
Downloaded: 967 file(s) [attempted 967/8459 = 11%, 298 KB/s], Decompressed: 963
Downloaded: 1008 file(s) [attempted 1008/8459 = 11%, 368 KB/s], Decompressed: 1004
Downloaded: 1052 file(s) [attempted 1052/8459 = 12%, 115 KB/s], Decompressed: 1047
Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 597 KB/s], Decompressed: 1086
Downloaded: 1128 file(s) [attempted 1128/8459 = 13%, 711 KB/s], Decompressed: 1124
Downloaded: 1165 file(s) [attempted 1165/8459 = 13%, 310 KB/s], Decompressed: 1158
Downloaded: 1210 file(s) [attempted 1210/8459 = 14%, 332 KB/s], Decompressed: 1206
Downloaded: 1258 file(s) [attempted 1258/8459 = 14%, 211 KB/s], Decompressed: 1256
Downloaded: 1303 file(s) [attempted 1303/8459 = 15%, 122 KB/s], Decompressed: 1295
Downloaded: 1340 file(s) [attempted 1340/8459 = 15%, 875 KB/s], Decompressed: 1336
Downloaded: 1377 file(s) [attempted 1377/8459 = 16%, 202 KB/s], Decompressed: 1370
Downloaded: 1418 file(s) [attempted 1418/8459 = 16%, 601 KB/s], Decompressed: 1415
Downloaded: 1463 file(s) [attempted 1463/8459 = 17%, 517 KB/s], Decompressed: 1459
Downloaded: 1504 file(s) [attempted 1504/8459 = 17%, 1392 KB/s], Decompressed: 1500
Downloaded: 1542 file(s) [attempted 1542/8459 = 18%, 1073 KB/s], Decompressed: 1535
Downloaded: 1583 file(s) [attempted 1583/8459 = 18%, 148 KB/s], Decompressed: 1572
Downloaded: 1620 file(s) [attempted 1620/8459 = 19%, 50 KB/s], Decompressed: 1617
Downloaded: 1661 file(s) [attempted 1661/8459 = 19%, 236 KB/s], Decompressed: 1658
Downloaded: 1706 file(s) [attempted 1706/8459 = 20%, 959 KB/s], Decompressed: 1702
Downloaded: 1747 file(s) [attempted 1747/8459 = 20%, 103 KB/s], Decompressed: 1740
Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 72 KB/s], Decompressed: 1781
Downloaded: 1829 file(s) [attempted 1829/8459 = 21%, 559 KB/s], Decompressed: 1822
Downloaded: 1867 file(s) [attempted 1867/8459 = 22%, 292 KB/s], Decompressed: 1860
Downloaded: 1905 file(s) [attempted 1905/8459 = 22%, 265 KB/s], Decompressed: 1901
Downloaded: 1947 file(s) [attempted 1947/8459 = 23%, 24 KB/s], Decompressed: 1942
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 79 KB/s], Decompressed: 1976
Downloaded: 2024 file(s) [attempted 2024/8459 = 23%, 409 KB/s], Decompressed: 2017
Downloaded: 2065 file(s) [attempted 2065/8459 = 24%, 129 KB/s], Decompressed: 2062
Downloaded: 2110 file(s) [attempted 2110/8459 = 24%, 771 KB/s], Decompressed: 2106
Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 521 KB/s], Decompressed: 2151
Downloaded: 2195 file(s) [attempted 2195/8459 = 25%, 29 KB/s], Decompressed: 2188
Downloaded: 2233 file(s) [attempted 2233/8459 = 26%, 527 KB/s], Decompressed: 2229
Downloaded: 2277 file(s) [attempted 2277/8459 = 26%, 228 KB/s], Decompressed: 2274
Downloaded: 2319 file(s) [attempted 2319/8459 = 27%, 39 KB/s], Decompressed: 2315
Downloaded: 2360 file(s) [attempted 2360/8459 = 27%, 72 KB/s], Decompressed: 2356
Downloaded: 2395 file(s) [attempted 2395/8459 = 28%, 37 KB/s], Decompressed: 2390
Downloaded: 2435 file(s) [attempted 2435/8459 = 28%, 1442 KB/s], Decompressed: 2431
Downloaded: 2478 file(s) [attempted 2478/8459 = 29%, 46 KB/s], Decompressed: 2472
Downloaded: 2519 file(s) [attempted 2519/8459 = 29%, 53 KB/s], Decompressed: 2513
Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 398 KB/s], Decompressed: 2555
Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 112 KB/s], Decompressed: 2596
Downloaded: 2639 file(s) [attempted 2639/8459 = 31%, 96 KB/s], Decompressed: 2633
Downloaded: 2674 file(s) [attempted 2674/8459 = 31%, 67 KB/s], Decompressed: 2673
Downloaded: 2715 file(s) [attempted 2715/8459 = 32%, 72 KB/s], Decompressed: 2712
Downloaded: 2758 file(s) [attempted 2758/8459 = 32%, 176 KB/s], Decompressed: 2753
Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 158 KB/s], Decompressed: 2794
Downloaded: 2841 file(s) [attempted 2841/8459 = 33%, 78 KB/s], Decompressed: 2837
Downloaded: 2880 file(s) [attempted 2880/8459 = 34%, 725 KB/s], Decompressed: 2876
Downloaded: 2924 file(s) [attempted 2924/8459 = 34%, 226 KB/s], Decompressed: 2917
Downloaded: 2962 file(s) [attempted 2962/8459 = 35%, 146 KB/s], Decompressed: 2955
Downloaded: 2999 file(s) [attempted 2999/8459 = 35%, 325 KB/s], Decompressed: 2996
Downloaded: 3044 file(s) [attempted 3044/8459 = 35%, 167 KB/s], Decompressed: 3041
Downloaded: 3085 file(s) [attempted 3085/8459 = 36%, 525 KB/s], Decompressed: 3084
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 281 KB/s], Decompressed: 3123
Downloaded: 3167 file(s) [attempted 3167/8459 = 37%, 155 KB/s], Decompressed: 3164
Downloaded: 3208 file(s) [attempted 3208/8459 = 37%, 85 KB/s], Decompressed: 3198
Downloaded: 3247 file(s) [attempted 3247/8459 = 38%, 44 KB/s], Decompressed: 3239
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 318 KB/s], Decompressed: 3284
Downloaded: 3330 file(s) [attempted 3330/8459 = 39%, 780 KB/s], Decompressed: 3325
Downloaded: 3372 file(s) [attempted 3372/8459 = 39%, 275 KB/s], Decompressed: 3369
Downloaded: 3414 file(s) [attempted 3414/8459 = 40%, 244 KB/s], Decompressed: 3412
Downloaded: 3455 file(s) [attempted 3455/8459 = 40%, 237 KB/s], Decompressed: 3454
Downloaded: 3490 file(s) [attempted 3490/8459 = 41%, 497 KB/s], Decompressed: 3485
Downloaded: 3537 file(s) [attempted 3537/8459 = 41%, 171 KB/s], Decompressed: 3530
Downloaded: 3575 file(s) [attempted 3575/8459 = 42%, 289 KB/s], Decompressed: 3571
Downloaded: 3615 file(s) [attempted 3615/8459 = 42%, 786 KB/s], Decompressed: 3609
Downloaded: 3653 file(s) [attempted 3653/8459 = 43%, 290 KB/s], Decompressed: 3650
Downloaded: 3698 file(s) [attempted 3698/8459 = 43%, 42 KB/s], Decompressed: 3694
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 392 KB/s], Decompressed: 3739
Downloaded: 3781 file(s) [attempted 3781/8459 = 44%, 201 KB/s], Decompressed: 3776
Downloaded: 3822 file(s) [attempted 3822/8459 = 45%, 126 KB/s], Decompressed: 3817
Downloaded: 3856 file(s) [attempted 3856/8459 = 45%, 443 KB/s], Decompressed: 3852
Downloaded: 3900 file(s) [attempted 3900/8459 = 46%, 364 KB/s], Decompressed: 3896
Downloaded: 3937 file(s) [attempted 3937/8459 = 46%, 68 KB/s], Decompressed: 3934
Downloaded: 3978 file(s) [attempted 3978/8459 = 47%, 865 KB/s], Decompressed: 3975
Downloaded: 4019 file(s) [attempted 4019/8459 = 47%, 42 KB/s], Decompressed: 4012
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 103 KB/s], Decompressed: 4054
Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 715 KB/s], Decompressed: 4095
Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 1026 KB/s], Decompressed: 4136
Downloaded: 4180 file(s) [attempted 4180/8459 = 49%, 318 KB/s], Decompressed: 4177
Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 422 KB/s], Decompressed: 4214
Downloaded: 4260 file(s) [attempted 4260/8459 = 50%, 456 KB/s], Decompressed: 4255
Downloaded: 4301 file(s) [attempted 4301/8459 = 50%, 211 KB/s], Decompressed: 4297
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 67 KB/s], Decompressed: 4327
Downloaded: 4374 file(s) [attempted 4374/8459 = 51%, 180 KB/s], Decompressed: 4369
Downloaded: 4420 file(s) [attempted 4420/8459 = 52%, 301 KB/s], Decompressed: 4413
Downloaded: 4464 file(s) [attempted 4464/8459 = 52%, 573 KB/s], Decompressed: 4461
Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 420 KB/s], Decompressed: 4498
Downloaded: 4540 file(s) [attempted 4540/8459 = 53%, 113 KB/s], Decompressed: 4536
Downloaded: 4581 file(s) [attempted 4581/8459 = 54%, 652 KB/s], Decompressed: 4577
Downloaded: 4622 file(s) [attempted 4622/8459 = 54%, 256 KB/s], Decompressed: 4618
Downloaded: 4663 file(s) [attempted 4663/8459 = 55%, 121 KB/s], Decompressed: 4659
Downloaded: 4704 file(s) [attempted 4704/8459 = 55%, 208 KB/s], Decompressed: 4702
Downloaded: 4736 file(s) [attempted 4736/8459 = 55%, 1282 KB/s], Decompressed: 4731
Downloaded: 4779 file(s) [attempted 4779/8459 = 56%, 154 KB/s], Decompressed: 4776
Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 415 KB/s], Decompressed: 4824
Downloaded: 4875 file(s) [attempted 4875/8459 = 57%, 599 KB/s], Decompressed: 4868
Downloaded: 4917 file(s) [attempted 4917/8459 = 58%, 216 KB/s], Decompressed: 4909
Downloaded: 4949 file(s) [attempted 4949/8459 = 58%, 201 KB/s], Decompressed: 4943
Downloaded: 4984 file(s) [attempted 4984/8459 = 58%, 296 KB/s], Decompressed: 4981
Downloaded: 5029 file(s) [attempted 5029/8459 = 59%, 376 KB/s], Decompressed: 5026
Downloaded: 5070 file(s) [attempted 5070/8459 = 59%, 98 KB/s], Decompressed: 5067
Downloaded: 5111 file(s) [attempted 5111/8459 = 60%, 432 KB/s], Decompressed: 5108
Downloaded: 5150 file(s) [attempted 5150/8459 = 60%, 132 KB/s], Decompressed: 5138
Downloaded: 5186 file(s) [attempted 5186/8459 = 61%, 571 KB/s], Decompressed: 5183
Downloaded: 5227 file(s) [attempted 5227/8459 = 61%, 154 KB/s], Decompressed: 5221
Downloaded: 5265 file(s) [attempted 5265/8459 = 62%, 71 KB/s], Decompressed: 5262
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 155 KB/s], Decompressed: 5296
Downloaded: 5335 file(s) [attempted 5335/8459 = 63%, 287 KB/s], Decompressed: 5330
Downloaded: 5368 file(s) [attempted 5368/8459 = 63%, 383 KB/s], Decompressed: 5364
Downloaded: 5411 file(s) [attempted 5411/8459 = 63%, 328 KB/s], Decompressed: 5402
Downloaded: 5446 file(s) [attempted 5446/8459 = 64%, 153 KB/s], Decompressed: 5443
Downloaded: 5491 file(s) [attempted 5491/8459 = 64%, 256 KB/s], Decompressed: 5484
Downloaded: 5535 file(s) [attempted 5535/8459 = 65%, 231 KB/s], Decompressed: 5532
Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 835 KB/s], Decompressed: 5577
Downloaded: 5621 file(s) [attempted 5621/8459 = 66%, 203 KB/s], Decompressed: 5614
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 1352 KB/s], Decompressed: 5655
Downloaded: 5700 file(s) [attempted 5700/8459 = 67%, 512 KB/s], Decompressed: 5693
Downloaded: 5741 file(s) [attempted 5741/8459 = 67%, 206 KB/s], Decompressed: 5737
Downloaded: 5785 file(s) [attempted 5785/8459 = 68%, 217 KB/s], Decompressed: 5782
Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 379 KB/s], Decompressed: 5820
Downloaded: 5866 file(s) [attempted 5866/8459 = 69%, 167 KB/s], Decompressed: 5861
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 1980 KB/s], Decompressed: 5898
Downloaded: 5945 file(s) [attempted 5945/8459 = 70%, 101 KB/s], Decompressed: 5939
Downloaded: 5987 file(s) [attempted 5987/8459 = 70%, 1612 KB/s], Decompressed: 5980
Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 143 KB/s], Decompressed: 6021
Downloaded: 6070 file(s) [attempted 6070/8459 = 71%, 361 KB/s], Decompressed: 6066
Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 562 KB/s], Decompressed: 6107
Downloaded: 6149 file(s) [attempted 6149/8459 = 72%, 221 KB/s], Decompressed: 6145
Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 74 KB/s], Decompressed: 6182
Downloaded: 6230 file(s) [attempted 6230/8459 = 73%, 149 KB/s], Decompressed: 6227
Downloaded: 6270 file(s) [attempted 6270/8459 = 74%, 238 KB/s], Decompressed: 6264
Downloaded: 6305 file(s) [attempted 6305/8459 = 74%, 36 KB/s], Decompressed: 6302
Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 116 KB/s], Decompressed: 6343
Downloaded: 6390 file(s) [attempted 6390/8459 = 75%, 873 KB/s], Decompressed: 6381
Downloaded: 6429 file(s) [attempted 6429/8459 = 76%, 279 KB/s], Decompressed: 6425
Downloaded: 6473 file(s) [attempted 6473/8459 = 76%, 268 KB/s], Decompressed: 6466
Downloaded: 6512 file(s) [attempted 6512/8459 = 76%, 108 KB/s], Decompressed: 6507
Downloaded: 6550 file(s) [attempted 6550/8459 = 77%, 116 KB/s], Decompressed: 6538
Downloaded: 6593 file(s) [attempted 6593/8459 = 77%, 166 KB/s], Decompressed: 6586
Downloaded: 6631 file(s) [attempted 6631/8459 = 78%, 427 KB/s], Decompressed: 6627
Downloaded: 6675 file(s) [attempted 6675/8459 = 78%, 1236 KB/s], Decompressed: 6672
Downloaded: 6710 file(s) [attempted 6710/8459 = 79%, 141 KB/s], Decompressed: 6706
Downloaded: 6750 file(s) [attempted 6750/8459 = 79%, 111 KB/s], Decompressed: 6744
Downloaded: 6791 file(s) [attempted 6791/8459 = 80%, 617 KB/s], Decompressed: 6788
Downloaded: 6832 file(s) [attempted 6832/8459 = 80%, 97 KB/s], Decompressed: 6829
Downloaded: 6880 file(s) [attempted 6880/8459 = 81%, 367 KB/s], Decompressed: 6874
Downloaded: 6925 file(s) [attempted 6925/8459 = 81%, 270 KB/s], Decompressed: 6921
Downloaded: 6963 file(s) [attempted 6963/8459 = 82%, 179 KB/s], Decompressed: 6952
Downloaded: 7004 file(s) [attempted 7004/8459 = 82%, 145 KB/s], Decompressed: 6997
Downloaded: 7045 file(s) [attempted 7045/8459 = 83%, 636 KB/s], Decompressed: 7038
Downloaded: 7086 file(s) [attempted 7086/8459 = 83%, 323 KB/s], Decompressed: 7082
Downloaded: 7129 file(s) [attempted 7129/8459 = 84%, 30 KB/s], Decompressed: 7123
Downloaded: 7168 file(s) [attempted 7168/8459 = 84%, 43 KB/s], Decompressed: 7164
Downloaded: 7206 file(s) [attempted 7206/8459 = 85%, 139 KB/s], Decompressed: 7202
Downloaded: 7250 file(s) [attempted 7250/8459 = 85%, 858 KB/s], Decompressed: 7247
Downloaded: 7288 file(s) [attempted 7288/8459 = 86%, 152 KB/s], Decompressed: 7284
Downloaded: 7332 file(s) [attempted 7332/8459 = 86%, 286 KB/s], Decompressed: 7329
Downloaded: 7373 file(s) [attempted 7373/8459 = 87%, 73 KB/s], Decompressed: 7370
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 414 KB/s], Decompressed: 7411
Downloaded: 7455 file(s) [attempted 7455/8459 = 88%, 223 KB/s], Decompressed: 7452
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 21 KB/s], Decompressed: 7496
Downloaded: 7544 file(s) [attempted 7544/8459 = 89%, 525 KB/s], Decompressed: 7541
Downloaded: 7585 file(s) [attempted 7585/8459 = 89%, 209 KB/s], Decompressed: 7581
Downloaded: 7623 file(s) [attempted 7623/8459 = 90%, 1108 KB/s], Decompressed: 7620
Downloaded: 7661 file(s) [attempted 7661/8459 = 90%, 133 KB/s], Decompressed: 7657
Downloaded: 7705 file(s) [attempted 7705/8459 = 91%, 285 KB/s], Decompressed: 7702
Downloaded: 7746 file(s) [attempted 7746/8459 = 91%, 313 KB/s], Decompressed: 7743
Downloaded: 7791 file(s) [attempted 7791/8459 = 92%, 522 KB/s], Decompressed: 7787
Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 384 KB/s], Decompressed: 7822
Downloaded: 7868 file(s) [attempted 7868/8459 = 93%, 256 KB/s], Decompressed: 7863
Downloaded: 7908 file(s) [attempted 7908/8459 = 93%, 608 KB/s], Decompressed: 7904
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 1832 KB/s], Decompressed: 7941
Downloaded: 7989 file(s) [attempted 7989/8459 = 94%, 198 KB/s], Decompressed: 7986
Downloaded: 8027 file(s) [attempted 8027/8459 = 94%, 458 KB/s], Decompressed: 8023
Downloaded: 8068 file(s) [attempted 8068/8459 = 95%, 135 KB/s], Decompressed: 8064
Downloaded: 8107 file(s) [attempted 8107/8459 = 95%, 94 KB/s], Decompressed: 8102
Downloaded: 8152 file(s) [attempted 8152/8459 = 96%, 198 KB/s], Decompressed: 8147
Downloaded: 8189 file(s) [attempted 8189/8459 = 96%, 499 KB/s], Decompressed: 8184
Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 320 KB/s], Decompressed: 8219
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 219 KB/s], Decompressed: 8263
Downloaded: 8307 file(s) [attempted 8307/8459 = 98%, 23 KB/s], Decompressed: 8304
Downloaded: 8350 file(s) [attempted 8350/8459 = 98%, 569 KB/s], Decompressed: 8342
Downloaded: 8390 file(s) [attempted 8390/8459 = 99%, 86 KB/s], Decompressed: 8383
Downloaded: 8427 file(s) [attempted 8427/8459 = 99%, 663 KB/s], Decompressed: 8426
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 357 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 357 KB/s], Decompressed: 8455

lean_checker exit 0 duration 12m 0s · created 6/6/2026, 3:22:32 AM

lake build

✔ [2787/2815] Built Architect.Command (1.7s)
✔ [2833/2856] Built Architect.Basic (2.1s)
✔ [2835/2856] Built Architect.Tactic (1.3s)
✔ [2836/2856] Built Architect.CollectUsed (900ms)
✔ [2837/2858] Built Architect.Content (882ms)
✔ [2840/2858] Built Architect.Output (1.7s)
✔ [2842/2859] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (5.9s)
✔ [2845/2859] Built PrimeNumberTheoremAnd.Auxiliary (8.2s)
✔ [2847/2886] Built Architect.Attribute (1.9s)
✔ [2848/2886] Built Architect.Load (1.1s)
✔ [3085/3099] Built Architect (881ms)
✔ [3089/3130] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (2.7s)
✔ [3449/3463] Built PrimeNumberTheoremAnd.Sobolev (12s)
✔ [3454/3464] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (2.2s)
✔ [3456/3464] Built PrimeNumberTheoremAnd.Rectangle (4.0s)
✔ [3457/3464] Built PrimeNumberTheoremAnd.Fourier (5.2s)
✔ [3459/3479] Built PrimeNumberTheoremAnd.ZetaConj (4.9s)
✔ [3480/3499] Built PrimeNumberTheoremAnd.SmoothExistence (5.3s)
✔ [3484/3499] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (2.8s)
✔ [3485/3504] Built PrimeNumberTheoremAnd.MellinCalculus (13s)
✔ [3609/3635] Built PrimeNumberTheoremAnd.HadamardFactorization (1.3s)
✔ [3610/3641] Built PrimeNumberTheoremAnd.Defs (5.4s)
✔ [3616/3642] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (5.5s)
✔ [3620/3642] Built PrimeNumberTheoremAnd.HoffsteinLockhart (3.4s)
✔ [3621/3643] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (10s)
✔ [3624/3646] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (5.4s)
✔ [3626/3646] Built PrimeNumberTheoremAnd.GeneralMeromorphic (3.1s)
✔ [3628/3646] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (7.6s)
⚠ [3631/3646] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (5.1s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3632/3648] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (8.3s)
✔ [3636/3650] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (15s)
✔ [3638/3650] Built PrimeNumberTheoremAnd.IEANTN.KLN (6.1s)
✔ [3695/3710] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (7.9s)
✔ [3696/3710] Built LeanCert.Core.Interval (5.3s)
✔ [3697/3720] Built PrimeNumberTheoremAnd.BrunTitchmarsh (10s)
✔ [3702/3720] Built LeanCert.Core.IntervalRat.Basic (14s)
✔ [3703/3721] Built LeanCert.Core.Expr (11s)
✔ [3704/3721] Built LeanCert.Tactic.IntervalAuto.Types (7.4s)
✔ [3705/3721] Built LeanCert.Meta.Numeral (4.3s)
✔ [3706/3722] Built LeanCert.Core.Support (3.8s)
✔ [3707/3722] Built LeanCert.Tactic.IntervalAuto.Norm (4.8s)
✔ [3708/3722] Built PrimeNumberTheoremAnd.ZetaBounds (48s)
✔ [3709/3723] Built LeanCert.Tactic.IntervalAuto.Extract (4.3s)
✔ [3710/3723] Built LeanCert.Meta.ToExpr (5.9s)
✔ [3711/3723] Built LeanCert.Core.IntervalRat.Transcendental (5.6s)
✔ [3712/3723] Built LeanCert.Core.IntervalRat.LogReduction (6.5s)
✔ [3713/3723] Built LeanCert.Tactic.IntervalAuto.Parse (12s)
⚠ [3714/3723] Built PrimeNumberTheoremAnd.Wiener (64s)
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3715/3731] Built LeanCert.Tactic.IntervalAuto.Diagnostic (6.7s)
✔ [3729/3746] Built LeanCert.Core.DerivativeIntervals (9.3s)
✔ [3732/3750] Built LeanCert.Core.Taylor (15s)
✔ [3733/3752] Built LeanCert.Core.IntervalRat.Taylor (27s)
✔ [3734/3752] Built LeanCert.Core.IntervalRat.TrigReduced (7.9s)
ℹ [3735/3754] Built PrimeNumberTheoremAnd.MediumPNT (90s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3736/3759] Built LeanCert.Core.IntervalReal (5.9s)
✔ [3737/3759] Built LeanCert.Contrib.Sinc (6.8s)
✔ [3738/3763] Built PrimeNumberTheoremAnd.Consequences (82s)
✔ [3749/3781] Built LeanCert.Core.IntervalRealEndpoints (7.6s)
✔ [3750/3785] Built LeanCert.Core.Dyadic (4.9s)
⚠ [3751/3786] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (112s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3752/3786] Built LeanCert.Engine.Eval.Core (10s)
✔ [3753/3789] Built LeanCert.Core.IntervalDyadic (10s)
✔ [3754/3790] Built LeanCert.Engine.Affine.Basic (8.8s)
⚠ [3755/3792] Built PrimeNumberTheoremAnd.StrongPNT (30s)
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`
⚠ [3756/3793] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (4.2s)
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`
✔ [3757/3796] Built LeanCert.Engine.Eval.Extended (4.1s)
✔ [3758/3820] Built LeanCert.Engine.Affine.Nonlinear (4.7s)
✔ [3760/3820] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (3.6s)
✔ [3761/3822] Built LeanCert.Tactic.Bound.Lemmas (3.1s)
✔ [3762/3829] Built PrimeNumberTheoremAnd.BorelCaratheodory (5.6s)
✔ [3888/3958] Built LeanCert.Engine.IntervalEval (3.3s)
✔ [3889/3958] Built LeanCert.Tactic.VecUtil (4.2s)
✔ [3890/3958] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (8.9s)
✔ [3891/3958] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (2.8s)
✔ [3892/3958] Built LeanCert.Engine.Affine.Transcendental (5.0s)
✔ [3893/3958] Built LeanCert.Engine.Integrate (8.1s)
✔ [3894/3958] Built LeanCert.Engine.RootFinding.Basic (5.5s)
✔ [3895/3958] Built LeanCert.Engine.IntervalEvalDyadic (3.9s)
✔ [3896/3960] Built LeanCert.Engine.Optimization.Box (2.8s)
✔ [3897/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (17s)
✔ [3899/3961] Built LeanCert.Tactic.FinSumExpand (2.1s)
✔ [3900/3961] Built LeanCert.Engine.AD.Basic (3.5s)
✔ [3901/3961] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (26s)
✔ [3902/3964] Built LeanCert.Engine.IntervalEvalAffine (4.2s)
✔ [3905/3964] Built LeanCert.Engine.TaylorModel.Core (8.2s)
✔ [3906/3971] Built LeanCert.Engine.RootFinding.Bisection (4.7s)
✔ [3909/3971] Built LeanCert.Validity.DyadicBounds (3.4s)
✔ [3910/3971] Built LeanCert.Engine.AD.Transcendental (4.3s)
✔ [3911/3971] Built LeanCert.Engine.TaylorModel.Special (3.5s)
✔ [3912/3971] Built LeanCert.Engine.TaylorModel.Log1p (7.0s)
✔ [3913/3971] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (12s)
✔ [3914/3971] Built LeanCert.Engine.TaylorModel.ExpLog (9.3s)
✔ [3915/3971] Built LeanCert.Engine.TaylorModel.Hyperbolic (12s)
✔ [3916/3971] Built LeanCert.Engine.TaylorModel.Trig (9.0s)
✔ [3917/3973] Built LeanCert.Engine.Chebyshev.Psi (4.3s)
✔ [3918/3978] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (3.6s)
✔ [3919/3978] Built LeanCert.Engine.AD.Eval (3.7s)
✔ [3920/3978] Built LeanCert.Engine.TaylorModel.Functions (4.2s)
⚠ [3922/3978] Built LeanCert.Examples.Li2Bounds (5.4s)
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3924/3979] Built LeanCert.Engine.ChebyshevPsi (3.8s)
✔ [3926/3979] Built PrimeNumberTheoremAnd.Tactic.Simprocs (2.7s)
✔ [3927/3979] Built LeanCert.Engine.AD.Correctness (5.9s)
✔ [3929/3980] Built LeanCert.Engine.TaylorModel.Expr (8.8s)
✔ [3930/3981] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (6.5s)
✔ [3931/3981] Built PrimeCert.Interval (3.7s)
✔ [3932/3981] Built LeanCert.Engine.AD.Computable (6.3s)
✔ [3933/3981] Built LeanCert.Engine.AD.PartialCorrectness (8.2s)
✔ [3934/3982] Built LeanCert.Engine.TaylorModel (4.9s)
✔ [3935/3983] Built PrimeCert.Meta.PrimeCert (2.7s)
✔ [3936/3984] Built PrimeCert.PredMod (668ms)
✔ [3937/3984] Built PrimeCert.Meta.SmallPrime (2.2s)
✔ [3938/3986] Built LeanCert.Engine.AD (3.8s)
✔ [3940/3987] Built PrimeCert.PowMod (3.3s)
✔ [3941/3987] Built LeanCert.Engine.IntervalEvalRefined (5.0s)
✔ [3942/3988] Built LeanCert.Meta.ProveSupported (4.7s)
⚠ [3944/3995] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (39s)
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`
✔ [3945/3995] Built LeanCert.Meta.ProveContinuous (4.9s)
✔ [3946/3995] Built LeanCert.Engine.Optimize (8.3s)
✔ [3947/3995] Built LeanCert.Tactic.IntervalAuto.ProveCommon (7.5s)
✔ [3948/3995] Built PrimeCert.Pocklington (5.8s)
✔ [3949/3995] Built PrimeCert.Wieferich (4.9s)
✔ [3950/3995] Built LeanCert.Tactic.IntervalAuto.Basic (4.1s)
✔ [3951/3995] Built LeanCert.Engine.Optimization.Gradient (6.6s)
✔ [3952/3995] Built LeanCert.Engine.RootFinding.Newton (6.3s)
✔ [3953/3996] Built PrimeCert.SmallPrimes (4.4s)
✔ [3954/4007] Built PrimeCert.Pocklington3 (11s)
✔ [3956/4007] Built LeanCert.Engine.RootFinding.MVTBounds (11s)
✔ [3958/4010] Built PrimeCert (4.6s)
✔ [3961/4010] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (5.0s)
✔ [3963/4019] Built LeanCert.Engine.RootFinding.Contraction (6.1s)
✔ [3965/4019] Built LeanCert.Engine.Optimization.Global (22s)
✔ [3967/4019] Built LeanCert.Engine.RootFinding.Main (3.2s)
✔ [3968/4019] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (11s)
✔ [3969/4019] Built LeanCert.Engine.Chebyshev.Theta (13s)
⚠ [3970/4019] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (110s)
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`
⚠ [3971/4019] Built PrimeNumberTheoremAnd.IEANTN.Mertens (23s)
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:263:0: ArithmeticFunction.vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, Λ i = log ↑n
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:855:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:859:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1239:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1272:8: declaration uses `sorry`
✔ [3973/4019] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (21s)
✔ [3974/4019] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (3.2s)
✔ [3975/4019] Built LeanCert.Engine.Optimization.BoundVerify (4.3s)
✔ [3976/4019] Built LeanCert.Engine.ChebyshevTheta (3.9s)
⚠ [3978/4019] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (8.5s)
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`
✔ [3979/4019] Built LeanCert.Validity.Bounds (9.1s)
✔ [3980/4019] Built PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative (4.8s)
⚠ [3981/4019] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (8.3s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:513:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:542:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:603:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:834:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:899:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1023:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1037:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1051:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1063:8: declaration uses `sorry`
✔ [3982/4019] Built LeanCert.Tactic.IntervalAuto.OptBound (3.8s)
✔ [3983/4019] Built PrimeNumberTheoremAnd.PerronFormula (10s)
✔ [3984/4019] Built LeanCert.Tactic.IntervalAuto.Multivariate (5.4s)
✔ [3985/4019] Built LeanCert.Tactic.IntervalAuto.RootBound (3.0s)
⚠ [3986/4019] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (6.7s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:235:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:262:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:303:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:386:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
✔ [3987/4019] Built LeanCert.Tactic.IntervalAuto.Bound (23s)
✔ [3988/4019] Built LeanCert.Tactic.IntervalAuto.Adaptive (6.1s)
✔ [3989/4019] Built LeanCert.Tactic.IntervalAuto.Subdiv (6.4s)
✔ [3990/4019] Built LeanCert.Tactic.IntervalAuto.PointIneq (12s)
✔ [3991/4019] Built LeanCert.Tactic.IntervalAuto (2.7s)
✔ [3992/4019] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (9.3s)
✔ [3993/4019] Built PrimeNumberTheoremAnd.IEANTN.LogTables (10s)
✔ [3994/4019] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (5.1s)
ℹ [3995/4019] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (27s)
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.
⚠ [3996/4019] Built PrimeNumberTheoremAnd.IEANTN.Buthe (17s)
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`
⚠ [3997/4019] Built LeanCert.Examples.BKLNW_a2_pow2 (30s)
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3998/4019] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (24s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [3999/4019] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (20s)
✔ [4000/4019] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (3.2s)
⚠ [4001/4019] Built LeanCert.Examples.BKLNW_a2_bounds (6.4s)
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [4002/4019] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (32s)
⚠ [4003/4019] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (9.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [4004/4019] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (4.6s)
⚠ [4005/4019] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (7.6s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [4006/4019] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (73s)
✔ [4007/4019] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (109s)
⚠ [4008/4019] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
✔ [4009/4019] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (9.0s)
⚠ [4010/4019] Built PrimeNumberTheoremAnd.IEANTN.Dusart (23s)
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`
✔ [4011/4019] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (11s)
⚠ [4012/4019] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (50s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [4013/4019] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (17s)
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`
⚠ [4014/4019] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.6s)
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`
⚠ [4015/4019] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (10s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4016/4019] Built PrimeNumberTheoremAnd.IEANTN.Lcm (35s)
✔ [4017/4019] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (62s)
✔ [4018/4019] Built PrimeNumberTheoremAnd (3.1s)
Build completed successfully (4019 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 4m 13s · created 6/6/2026, 3:22:32 AM

lake build :blueprint

✔ [7/35] Built Architect.Command:c.o (570ms)
✔ [11/35] Built Batteries.Lean.NameMapAttribute:c.o (710ms)
✔ [12/35] Built Architect.CollectUsed:c.o (145ms)
✔ [15/35] Built Architect.Content:c.o (185ms)
✔ [19/35] Built Architect.Basic:c.o (1.2s)
✔ [22/35] Built Architect.Load:c.o (161ms)
✔ [24/35] Built Architect.Tactic:c.o (822ms)
✔ [25/35] Built Architect:c.o (79ms)
✔ [27/35] Built Cli.Extensions:c.o (508ms)
✔ [28/56] Built Architect.Attribute:c.o (915ms)
✔ [29/56] Built Cli:c.o (63ms)
✔ [468/518] Built Main (1.1s)
✔ [510/569] Built Architect.Output:c.o (2.2s)
✔ [559/658] Built Main:c.o (231ms)
✔ [2239/2396] Built Cli.Basic:c.o (3.2s)
ℹ [3492/3653] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3508/3653] 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`
⚠ [3646/3797] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3659/3797] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3722/3797] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3723/3797] 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`
⚠ [3830/3961] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
⚠ [3832/3961] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3966/4119] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3968/4119] 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`
⚠ [3969/4119] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
⚠ [3971/4119] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
⚠ [3974/4119] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [3975/4119] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
⚠ [3982/4119] 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`
⚠ [3983/4119] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:513:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:542:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:603:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:834:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:899:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1023:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1037:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1051:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1063:8: declaration uses `sorry`
⚠ [3989/4119] 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`
⚠ [3990/4119] 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`
⚠ [3995/4119] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [4012/4119] 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`
⚠ [4013/4119] 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`
⚠ [4014/4119] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4022/4119] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:89:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:235:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:262:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:303:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:386:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:540:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:567:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:599:8: declaration uses `sorry`
⚠ [4026/4119] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:263:0: ArithmeticFunction.vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, Λ i = log ↑n
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:855:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:859:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1239:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1272:8: declaration uses `sorry`
ℹ [4032/4119] 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.
⚠ [4034/4119] 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`
✔ [4038/4119] Built extract_blueprint:exe (1.9s)
✔ [4039/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (1.0s)
✔ [4040/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (2.3s)
✔ [4041/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (2.3s)
✔ [4042/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (1.0s)
✔ [4043/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (2.1s)
✔ [4044/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.3s)
✔ [4045/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (13s)
✔ [4046/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (11s)
✔ [4047/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (1.3s)
✔ [4048/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (4.2s)
✔ [4049/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (48s)
✔ [4050/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.4s)
✔ [4051/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.8s)
✔ [4052/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (2.4s)
✔ [4053/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.3s)
✔ [4054/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [4055/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (2.3s)
✔ [4056/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (2.3s)
✔ [4057/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (8.2s)
✔ [4058/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (34s)
✔ [4059/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (13s)
✔ [4060/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.1s)
✔ [4061/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (2.8s)
✔ [4062/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.1s)
✔ [4063/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (2.4s)
✔ [4064/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (10s)
✔ [4065/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (2.9s)
✔ [4066/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.1s)
✔ [4067/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (25s)
✔ [4068/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.3s)
✔ [4069/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.8s)
✔ [4070/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.5s)
✔ [4071/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.5s)
✔ [4072/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [4073/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (5.9s)
✔ [4074/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (2.3s)
✔ [4075/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.6s)
✔ [4076/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.3s)
✔ [4077/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.5s)
✔ [4078/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.6s)
✔ [4079/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (2.7s)
✔ [4080/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4081/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (2.9s)
✔ [4082/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.1s)
✔ [4083/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (16s)
✔ [4084/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.6s)
✔ [4085/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4086/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.8s)
✔ [4087/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
✔ [4088/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (16s)
✔ [4089/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4090/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.5s)
✔ [4091/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.5s)
✔ [4092/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.2s)
✔ [4093/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4094/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4095/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4096/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (1.4s)
✔ [4097/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (2.2s)
✔ [4098/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (2.9s)
✔ [4099/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (45s)
✔ [4100/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.4s)
✔ [4101/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.9s)
✔ [4102/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative:blueprint (2.7s)
✔ [4103/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (14s)
✔ [4104/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (2.5s)
✔ [4105/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4106/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (33s)
✔ [4107/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4108/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.0s)
✔ [4109/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.6s)
✔ [4110/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (17s)
✔ [4111/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (48s)
✔ [4112/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (3.9s)
✔ [4113/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (24s)
✔ [4114/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.3s)
✔ [4115/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (58s)
✔ [4116/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (23s)
✔ [4117/4119] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (61s)
ℹ [4118/4120] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (82ms)
info: Blueprint indexing
Build completed successfully (4120 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 - duration 4h 0m · created 6/6/2026, 3:22:32 AM

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

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 98ff86bd5560f0d0812ecbbd2abaf350eb36788d19aa8c86aa7352abba74fe91
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-68-runtime-semantic_extract-2608519-1780701738239054533-7