Verification run

Run 114

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit 6f8a0637eeaf toolchain lean-v4-31-0 prover lean took 2h 17m · finished 2w ago

lake build failed with exit code none (process did not exit cleanly) (toolchain lean-v4-31-0, command: elan run leanprover/lean4:v4.31.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

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

$ git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-741-source
exit_code=Some(0) duration_ms=947
stderr:
Cloning into '/var/lib/apodeixis/repos/job-741-source'...


$ git checkout 6f8a0637eeaf00e35b6c4715decc8da160b18cc2
exit_code=Some(0) duration_ms=53
stderr:
Note: switching to '6f8a0637eeaf00e35b6c4715decc8da160b18cc2'.

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 6f8a063 fix: use nth_prime' k in Dusart lemma_5_10a (#1627)

Resolved source revision: 6f8a0637eeaf00e35b6c4715decc8da160b18cc2

Detected prover: lean
Detected requested toolchain: lean-v4-31-0
Materialized Lean semantic helper assets
Prepared source: revision=6f8a0637eeaf00e35b6c4715decc8da160b18cc2 provenance={"branch":"main","checked_out_revision":"6f8a0637eeaf00e35b6c4715decc8da160b18cc2","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"6f8a0637eeaf00e35b6c4715decc8da160b18cc2","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-31-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 13 Lean dependency package snapshot(s)
Prepared 13 shared Lean git mirror alias(es)
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction

$ lake exe cache get
exit_code=Some(0) duration_ms=63749
stdout:
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8546 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Decompressed 8546 file(s)
Already decompressed 8546 file(s)

stderr:
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/8546 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8546 = 0%, 12 KB/s], Decompressed: 15
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 119 KB/s], Decompressed: 40
Downloaded: 67 file(s) [attempted 67/8546 = 0%, 55 KB/s], Decompressed: 65
Downloaded: 95 file(s) [attempted 95/8546 = 1%, 255 KB/s], Decompressed: 92
Downloaded: 136 file(s) [attempted 136/8546 = 1%, 915 KB/s], Decompressed: 129
Downloaded: 173 file(s) [attempted 173/8546 = 2%, 391 KB/s], Decompressed: 163
Downloaded: 201 file(s) [attempted 201/8546 = 2%, 82 KB/s], Decompressed: 197
Downloaded: 234 file(s) [attempted 234/8546 = 2%, 609 KB/s], Decompressed: 231
Downloaded: 275 file(s) [attempted 275/8546 = 3%, 795 KB/s], Decompressed: 268
Downloaded: 319 file(s) [attempted 319/8546 = 3%, 520 KB/s], Decompressed: 312
Downloaded: 363 file(s) [attempted 363/8546 = 4%, 1023 KB/s], Decompressed: 360
Downloaded: 400 file(s) [attempted 400/8546 = 4%, 225 KB/s], Decompressed: 397
Downloaded: 441 file(s) [attempted 441/8546 = 5%, 92 KB/s], Decompressed: 431
Downloaded: 478 file(s) [attempted 478/8546 = 5%, 435 KB/s], Decompressed: 471
Downloaded: 519 file(s) [attempted 519/8546 = 6%, 666 KB/s], Decompressed: 515
Downloaded: 563 file(s) [attempted 563/8546 = 6%, 254 KB/s], Decompressed: 559
Downloaded: 601 file(s) [attempted 601/8546 = 7%, 266 KB/s], Decompressed: 597
Downloaded: 641 file(s) [attempted 641/8546 = 7%, 168 KB/s], Decompressed: 637
Downloaded: 679 file(s) [attempted 679/8546 = 7%, 167 KB/s], Decompressed: 674
Downloaded: 722 file(s) [attempted 722/8546 = 8%, 385 KB/s], Decompressed: 718
Downloaded: 762 file(s) [attempted 762/8546 = 8%, 124 KB/s], Decompressed: 752
Downloaded: 800 file(s) [attempted 800/8546 = 9%, 131 KB/s], Decompressed: 796
Downloaded: 844 file(s) [attempted 844/8546 = 9%, 1203 KB/s], Decompressed: 837
Downloaded: 888 file(s) [attempted 888/8546 = 10%, 152 KB/s], Decompressed: 884
Downloaded: 925 file(s) [attempted 925/8546 = 10%, 1284 KB/s], Decompressed: 922
Downloaded: 949 file(s) [attempted 949/8546 = 11%, 377 KB/s], Decompressed: 945
Downloaded: 969 file(s) [attempted 969/8546 = 11%, 522 KB/s], Decompressed: 966
Downloaded: 984 file(s) [attempted 984/8546 = 11%, 27 KB/s], Decompressed: 979
Downloaded: 996 file(s) [attempted 996/8546 = 11%, 243 KB/s], Decompressed: 993
Downloaded: 1043 file(s) [attempted 1043/8546 = 12%, 719 KB/s], Decompressed: 1040
Downloaded: 1094 file(s) [attempted 1094/8546 = 12%, 41 KB/s], Decompressed: 1087
Downloaded: 1141 file(s) [attempted 1141/8546 = 13%, 491 KB/s], Decompressed: 1138
Downloaded: 1192 file(s) [attempted 1192/8546 = 13%, 144 KB/s], Decompressed: 1185
Downloaded: 1240 file(s) [attempted 1240/8546 = 14%, 421 KB/s], Decompressed: 1236
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 256 KB/s], Decompressed: 1273
Downloaded: 1317 file(s) [attempted 1317/8546 = 15%, 127 KB/s], Decompressed: 1311
Downloaded: 1355 file(s) [attempted 1355/8546 = 15%, 44 KB/s], Decompressed: 1351
Downloaded: 1402 file(s) [attempted 1402/8546 = 16%, 491 KB/s], Decompressed: 1395
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 85 KB/s], Decompressed: 1439
Downloaded: 1485 file(s) [attempted 1485/8546 = 17%, 267 KB/s], Decompressed: 1480
Downloaded: 1525 file(s) [attempted 1525/8546 = 17%, 56 KB/s], Decompressed: 1517
Downloaded: 1563 file(s) [attempted 1563/8546 = 18%, 172 KB/s], Decompressed: 1554
Downloaded: 1605 file(s) [attempted 1605/8546 = 18%, 136 KB/s], Decompressed: 1602
Downloaded: 1646 file(s) [attempted 1646/8546 = 19%, 1072 KB/s], Decompressed: 1639
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 64 KB/s], Decompressed: 1676
Downloaded: 1723 file(s) [attempted 1723/8546 = 20%, 76 KB/s], Decompressed: 1717
Downloaded: 1764 file(s) [attempted 1764/8546 = 20%, 299 KB/s], Decompressed: 1761
Downloaded: 1804 file(s) [attempted 1804/8546 = 21%, 256 KB/s], Decompressed: 1801
Downloaded: 1848 file(s) [attempted 1848/8546 = 21%, 714 KB/s], Decompressed: 1845
Downloaded: 1886 file(s) [attempted 1886/8546 = 22%, 281 KB/s], Decompressed: 1882
Downloaded: 1926 file(s) [attempted 1926/8546 = 22%, 152 KB/s], Decompressed: 1916
Downloaded: 1967 file(s) [attempted 1967/8546 = 23%, 446 KB/s], Decompressed: 1953
Downloaded: 2004 file(s) [attempted 2004/8546 = 23%, 1118 KB/s], Decompressed: 1997
Downloaded: 2048 file(s) [attempted 2048/8546 = 23%, 269 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8546 = 24%, 65 KB/s], Decompressed: 2085
Downloaded: 2129 file(s) [attempted 2129/8546 = 24%, 832 KB/s], Decompressed: 2126
Downloaded: 2173 file(s) [attempted 2173/8546 = 25%, 132 KB/s], Decompressed: 2170
Downloaded: 2214 file(s) [attempted 2214/8546 = 25%, 502 KB/s], Decompressed: 2207
Downloaded: 2258 file(s) [attempted 2258/8546 = 26%, 542 KB/s], Decompressed: 2251
Downloaded: 2302 file(s) [attempted 2302/8546 = 26%, 227 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8546 = 27%, 39 KB/s], Decompressed: 2339
Downloaded: 2383 file(s) [attempted 2383/8546 = 27%, 208 KB/s], Decompressed: 2376
Downloaded: 2420 file(s) [attempted 2420/8546 = 28%, 38 KB/s], Decompressed: 2413
Downloaded: 2461 file(s) [attempted 2461/8546 = 28%, 181 KB/s], Decompressed: 2457
Downloaded: 2507 file(s) [attempted 2507/8546 = 29%, 146 KB/s], Decompressed: 2498
Downloaded: 2546 file(s) [attempted 2546/8546 = 29%, 515 KB/s], Decompressed: 2535
Downloaded: 2586 file(s) [attempted 2586/8546 = 30%, 200 KB/s], Decompressed: 2569
Downloaded: 2623 file(s) [attempted 2623/8546 = 30%, 113 KB/s], Decompressed: 2616
Downloaded: 2667 file(s) [attempted 2667/8546 = 31%, 416 KB/s], Decompressed: 2664
Downloaded: 2714 file(s) [attempted 2714/8546 = 31%, 133 KB/s], Decompressed: 2711
Downloaded: 2752 file(s) [attempted 2752/8546 = 32%, 301 KB/s], Decompressed: 2748
Downloaded: 2796 file(s) [attempted 2796/8546 = 32%, 219 KB/s], Decompressed: 2789
Downloaded: 2836 file(s) [attempted 2836/8546 = 33%, 103 KB/s], Decompressed: 2833
Downloaded: 2878 file(s) [attempted 2878/8546 = 33%, 279 KB/s], Decompressed: 2873
Downloaded: 2914 file(s) [attempted 2914/8546 = 34%, 145 KB/s], Decompressed: 2911
Downloaded: 2958 file(s) [attempted 2958/8546 = 34%, 740 KB/s], Decompressed: 2951
Downloaded: 2999 file(s) [attempted 2999/8546 = 35%, 285 KB/s], Decompressed: 2995
Downloaded: 3043 file(s) [attempted 3043/8546 = 35%, 610 KB/s], Decompressed: 3039
Downloaded: 3087 file(s) [attempted 3087/8546 = 36%, 115 KB/s], Decompressed: 3080
Downloaded: 3127 file(s) [attempted 3127/8546 = 36%, 238 KB/s], Decompressed: 3120
Downloaded: 3166 file(s) [attempted 3166/8546 = 37%, 84 KB/s], Decompressed: 3154
Downloaded: 3205 file(s) [attempted 3205/8546 = 37%, 1276 KB/s], Decompressed: 3198
Downloaded: 3249 file(s) [attempted 3249/8546 = 38%, 53 KB/s], Decompressed: 3246
Downloaded: 3289 file(s) [attempted 3289/8546 = 38%, 101 KB/s], Decompressed: 3286
Downloaded: 3337 file(s) [attempted 3337/8546 = 39%, 399 KB/s], Decompressed: 3333
Downloaded: 3381 file(s) [attempted 3381/8546 = 39%, 488 KB/s], Decompressed: 3371
Downloaded: 3425 file(s) [attempted 3425/8546 = 40%, 62 KB/s], Decompressed: 3405
Downloaded: 3465 file(s) [attempted 3465/8546 = 40%, 448 KB/s], Decompressed: 3462
Downloaded: 3503 file(s) [attempted 3503/8546 = 40%, 192 KB/s], Decompressed: 3499
Downloaded: 3541 file(s) [attempted 3541/8546 = 41%, 284 KB/s], Decompressed: 3536
Downloaded: 3587 file(s) [attempted 3587/8546 = 41%, 228 KB/s], Decompressed: 3584
Downloaded: 3632 file(s) [attempted 3632/8546 = 42%, 118 KB/s], Decompressed: 3628
Downloaded: 3668 file(s) [attempted 3668/8546 = 42%, 108 KB/s], Decompressed: 3658
Downloaded: 3712 file(s) [attempted 3712/8546 = 43%, 35 KB/s], Decompressed: 3706
Downloaded: 3756 file(s) [attempted 3756/8546 = 43%, 251 KB/s], Decompressed: 3753
Downloaded: 3804 file(s) [attempted 3804/8546 = 44%, 313 KB/s], Decompressed: 3800
Downloaded: 3851 file(s) [attempted 3851/8546 = 45%, 63 KB/s], Decompressed: 3844
Downloaded: 3892 file(s) [attempted 3892/8546 = 45%, 146 KB/s], Decompressed: 3888
Downloaded: 3925 file(s) [attempted 3925/8546 = 45%, 555 KB/s], Decompressed: 3915
Downloaded: 3966 file(s) [attempted 3966/8546 = 46%, 241 KB/s], Decompressed: 3963
Downloaded: 4010 file(s) [attempted 4010/8546 = 46%, 354 KB/s], Decompressed: 4007
Downloaded: 4057 file(s) [attempted 4057/8546 = 47%, 241 KB/s], Decompressed: 4051
Downloaded: 4105 file(s) [attempted 4105/8546 = 48%, 1281 KB/s], Decompressed: 4098
Downloaded: 4145 file(s) [attempted 4145/8546 = 48%, 468 KB/s], Decompressed: 4142
Downloaded: 4183 file(s) [attempted 4183/8546 = 48%, 795 KB/s], Decompressed: 4176
Downloaded: 4223 file(s) [attempted 4223/8546 = 49%, 450 KB/s], Decompressed: 4220
Downloaded: 4267 file(s) [attempted 4267/8546 = 49%, 378 KB/s], Decompressed: 4260
Downloaded: 4311 file(s) [attempted 4311/8546 = 50%, 78 KB/s], Decompressed: 4308
Downloaded: 4355 file(s) [attempted 4355/8546 = 50%, 447 KB/s], Decompressed: 4351
Downloaded: 4392 file(s) [attempted 4392/8546 = 51%, 358 KB/s], Decompressed: 4389
Downloaded: 4434 file(s) [attempted 4434/8546 = 51%, 36 KB/s], Decompressed: 4429
Downloaded: 4473 file(s) [attempted 4473/8546 = 52%, 88 KB/s], Decompressed: 4463
Downloaded: 4516 file(s) [attempted 4516/8546 = 52%, 411 KB/s], Decompressed: 4511
Downloaded: 4555 file(s) [attempted 4555/8546 = 53%, 269 KB/s], Decompressed: 4541
Downloaded: 4592 file(s) [attempted 4592/8546 = 53%, 140 KB/s], Decompressed: 4585
Downloaded: 4636 file(s) [attempted 4636/8546 = 54%, 505 KB/s], Decompressed: 4632
Downloaded: 4680 file(s) [attempted 4680/8546 = 54%, 1098 KB/s], Decompressed: 4670
Downloaded: 4717 file(s) [attempted 4717/8546 = 55%, 722 KB/s], Decompressed: 4710
Downloaded: 4754 file(s) [attempted 4754/8546 = 55%, 169 KB/s], Decompressed: 4751
Downloaded: 4798 file(s) [attempted 4798/8546 = 56%, 23 KB/s], Decompressed: 4791
Downloaded: 4839 file(s) [attempted 4839/8546 = 56%, 52 KB/s], Decompressed: 4835
Downloaded: 4883 file(s) [attempted 4883/8546 = 57%, 197 KB/s], Decompressed: 4879
Downloaded: 4928 file(s) [attempted 4928/8546 = 57%, 93 KB/s], Decompressed: 4923
Downloaded: 4967 file(s) [attempted 4967/8546 = 58%, 766 KB/s], Decompressed: 4961
Downloaded: 5005 file(s) [attempted 5005/8546 = 58%, 218 KB/s], Decompressed: 4994
Downloaded: 5043 file(s) [attempted 5043/8546 = 59%, 107 KB/s], Decompressed: 5038
Downloaded: 5082 file(s) [attempted 5082/8546 = 59%, 333 KB/s], Decompressed: 5079
Downloaded: 5126 file(s) [attempted 5126/8546 = 59%, 492 KB/s], Decompressed: 5120
Downloaded: 5170 file(s) [attempted 5170/8546 = 60%, 112 KB/s], Decompressed: 5167
Downloaded: 5208 file(s) [attempted 5208/8546 = 60%, 1336 KB/s], Decompressed: 5204
Downloaded: 5249 file(s) [attempted 5249/8546 = 61%, 102 KB/s], Decompressed: 5245
Downloaded: 5292 file(s) [attempted 5292/8546 = 61%, 327 KB/s], Decompressed: 5285
Downloaded: 5333 file(s) [attempted 5333/8546 = 62%, 447 KB/s], Decompressed: 5329
Downloaded: 5380 file(s) [attempted 5380/8546 = 62%, 232 KB/s], Decompressed: 5377
Downloaded: 5427 file(s) [attempted 5427/8546 = 63%, 320 KB/s], Decompressed: 5411
Downloaded: 5461 file(s) [attempted 5461/8546 = 63%, 285 KB/s], Decompressed: 5455
Downloaded: 5502 file(s) [attempted 5502/8546 = 64%, 529 KB/s], Decompressed: 5498
Downloaded: 5542 file(s) [attempted 5542/8546 = 64%, 258 KB/s], Decompressed: 5536
Downloaded: 5586 file(s) [attempted 5586/8546 = 65%, 88 KB/s], Decompressed: 5580
Downloaded: 5634 file(s) [attempted 5634/8546 = 65%, 98 KB/s], Decompressed: 5627
Downloaded: 5674 file(s) [attempted 5674/8546 = 66%, 1260 KB/s], Decompressed: 5671
Downloaded: 5715 file(s) [attempted 5715/8546 = 66%, 914 KB/s], Decompressed: 5708
Downloaded: 5753 file(s) [attempted 5753/8546 = 67%, 110 KB/s], Decompressed: 5745
Downloaded: 5790 file(s) [attempted 5790/8546 = 67%, 1807 KB/s], Decompressed: 5783
Downloaded: 5833 file(s) [attempted 5833/8546 = 68%, 238 KB/s], Decompressed: 5830
Downloaded: 5874 file(s) [attempted 5874/8546 = 68%, 271 KB/s], Decompressed: 5871
Downloaded: 5918 file(s) [attempted 5918/8546 = 69%, 590 KB/s], Decompressed: 5908
Downloaded: 5959 file(s) [attempted 5959/8546 = 69%, 721 KB/s], Decompressed: 5948
Downloaded: 5998 file(s) [attempted 5998/8546 = 70%, 152 KB/s], Decompressed: 5969
Downloaded: 6036 file(s) [attempted 6036/8546 = 70%, 224 KB/s], Decompressed: 6033
Downloaded: 6080 file(s) [attempted 6080/8546 = 71%, 295 KB/s], Decompressed: 6077
Downloaded: 6124 file(s) [attempted 6124/8546 = 71%, 225 KB/s], Decompressed: 6118
Downloaded: 6158 file(s) [attempted 6158/8546 = 72%, 1986 KB/s], Decompressed: 6151
Downloaded: 6205 file(s) [attempted 6205/8546 = 72%, 277 KB/s], Decompressed: 6202
Downloaded: 6243 file(s) [attempted 6243/8546 = 73%, 284 KB/s], Decompressed: 6233
Downloaded: 6283 file(s) [attempted 6283/8546 = 73%, 491 KB/s], Decompressed: 6280
Downloaded: 6322 file(s) [attempted 6322/8546 = 73%, 1012 KB/s], Decompressed: 6310
Downloaded: 6358 file(s) [attempted 6358/8546 = 74%, 345 KB/s], Decompressed: 6354
Downloaded: 6402 file(s) [attempted 6402/8546 = 74%, 372 KB/s], Decompressed: 6398
Downloaded: 6446 file(s) [attempted 6446/8546 = 75%, 498 KB/s], Decompressed: 6442
Downloaded: 6486 file(s) [attempted 6486/8546 = 75%, 507 KB/s], Decompressed: 6483
Downloaded: 6523 file(s) [attempted 6523/8546 = 76%, 1730 KB/s], Decompressed: 6518
Downloaded: 6564 file(s) [attempted 6564/8546 = 76%, 759 KB/s], Decompressed: 6561
Downloaded: 6608 file(s) [attempted 6608/8546 = 77%, 452 KB/s], Decompressed: 6605
Downloaded: 6652 file(s) [attempted 6652/8546 = 77%, 396 KB/s], Decompressed: 6649
Downloaded: 6696 file(s) [attempted 6696/8546 = 78%, 53 KB/s], Decompressed: 6686
Downloaded: 6733 file(s) [attempted 6733/8546 = 78%, 75 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8546 = 79%, 127 KB/s], Decompressed: 6770
Downloaded: 6814 file(s) [attempted 6814/8546 = 79%, 288 KB/s], Decompressed: 6811
Downloaded: 6858 file(s) [attempted 6858/8546 = 80%, 81 KB/s], Decompressed: 6855
Downloaded: 6902 file(s) [attempted 6902/8546 = 80%, 43 KB/s], Decompressed: 6892
Downloaded: 6943 file(s) [attempted 6943/8546 = 81%, 109 KB/s], Decompressed: 6936
Downloaded: 6987 file(s) [attempted 6987/8546 = 81%, 450 KB/s], Decompressed: 6980
Downloaded: 7027 file(s) [attempted 7027/8546 = 82%, 213 KB/s], Decompressed: 7017
Downloaded: 7065 file(s) [attempted 7065/8546 = 82%, 1699 KB/s], Decompressed: 7058
Downloaded: 7105 file(s) [attempted 7105/8546 = 83%, 353 KB/s], Decompressed: 7102
Downloaded: 7149 file(s) [attempted 7149/8546 = 83%, 304 KB/s], Decompressed: 7146
Downloaded: 7197 file(s) [attempted 7197/8546 = 84%, 526 KB/s], Decompressed: 7188
Downloaded: 7244 file(s) [attempted 7244/8546 = 84%, 704 KB/s], Decompressed: 7234
Downloaded: 7281 file(s) [attempted 7281/8546 = 85%, 79 KB/s], Decompressed: 7278
Downloaded: 7322 file(s) [attempted 7322/8546 = 85%, 92 KB/s], Decompressed: 7315
Downloaded: 7362 file(s) [attempted 7362/8546 = 86%, 165 KB/s], Decompressed: 7359
Downloaded: 7406 file(s) [attempted 7406/8546 = 86%, 738 KB/s], Decompressed: 7396
Downloaded: 7450 file(s) [attempted 7450/8546 = 87%, 74 KB/s], Decompressed: 7447
Downloaded: 7494 file(s) [attempted 7494/8546 = 87%, 24 KB/s], Decompressed: 7477
Downloaded: 7530 file(s) [attempted 7530/8546 = 88%, 327 KB/s], Decompressed: 7521
Downloaded: 7569 file(s) [attempted 7569/8546 = 88%, 424 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8546 = 89%, 131 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8546 = 89%, 72 KB/s], Decompressed: 7650
Downloaded: 7701 file(s) [attempted 7701/8546 = 90%, 178 KB/s], Decompressed: 7694
Downloaded: 7734 file(s) [attempted 7734/8546 = 90%, 44 KB/s], Decompressed: 7731
Downloaded: 7773 file(s) [attempted 7773/8546 = 90%, 484 KB/s], Decompressed: 7768
Downloaded: 7816 file(s) [attempted 7816/8546 = 91%, 139 KB/s], Decompressed: 7812
Downloaded: 7861 file(s) [attempted 7861/8546 = 91%, 194 KB/s], Decompressed: 7856
Downloaded: 7900 file(s) [attempted 7900/8546 = 92%, 22 KB/s], Decompressed: 7893
Downloaded: 7941 file(s) [attempted 7941/8546 = 92%, 2377 KB/s], Decompressed: 7927
Downloaded: 7978 file(s) [attempted 7978/8546 = 93%, 62 KB/s], Decompressed: 7975
Downloaded: 8022 file(s) [attempted 8022/8546 = 93%, 278 KB/s], Decompressed: 8015
Downloaded: 8063 file(s) [attempted 8063/8546 = 94%, 1028 KB/s], Decompressed: 8056
Downloaded: 8110 file(s) [attempted 8110/8546 = 94%, 166 KB/s], Decompressed: 8103
Downloaded: 8154 file(s) [attempted 8154/8546 = 95%, 252 KB/s], Decompressed: 8150
Downloaded: 8194 file(s) [attempted 8194/8546 = 95%, 313 KB/s], Decompressed: 8181
Downloaded: 8232 file(s) [attempted 8232/8546 = 96%, 355 KB/s], Decompressed: 8228
Downloaded: 8276 file(s) [attempted 8276/8546 = 96%, 39 KB/s], Decompressed: 8272
Downloaded: 8316 file(s) [attempted 8316/8546 = 97%, 293 KB/s], Decompressed: 8309
Downloaded: 8360 file(s) [attempted 8360/8546 = 97%, 562 KB/s], Decompressed: 8350
Downloaded: 8401 file(s) [attempted 8401/8546 = 98%, 2756 KB/s], Decompressed: 8387
Downloaded: 8443 file(s) [attempted 8443/8546 = 98%, 570 KB/s], Decompressed: 8438
Downloaded: 8482 file(s) [attempted 8482/8546 = 99%, 556 KB/s], Decompressed: 8472
Downloaded: 8523 file(s) [attempted 8523/8546 = 99%, 750 KB/s], Decompressed: 8519
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 750 KB/s], Decompressed: 8540


$ lake build
exit_code=None duration_ms=7200010
stdout:
ℹ [3628/3638] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3651/3667] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
⚠ [3778/3799] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3895/3910] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3965/3986] 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`
⚠ [3967/3986] 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`
⚠ [3968/3986] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4109/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`
⚠ [4110/4114] 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`
⚠ [4112/4154] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4113/4154] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4155/4165] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4158/4165] 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`
⚠ [4161/4165] Built PrimeNumberTheoremAnd.IEANTN.Dusart (244s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
ℹ [4167/4175] 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.
⚠ [4169/4175] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4200/4210] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4201/4210] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4222/4262] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (210s)
⚠ [4240/4277] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (204s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
⚠ [4247/4277] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (205s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
⚠ [4256/4284] 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`
✔ [4259/4284] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (6049s)

stderr:
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 7200s
podman cleanup removed verifier container apx-verifier-job-741-runtime-lean_checker-2850807-1782696279415263621-1

$ lake build :blueprint
exit_code=Some(0) duration_ms=743455
stdout:
✔ [27/35] Built Cli.Basic:c.o (4.7s)
✔ [30/35] Built Cli.Extensions:c.o (528ms)
✔ [33/35] Built Cli:c.o (70ms)
ℹ [3682/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3715/3734] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
⚠ [3849/3864] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4045/4070] 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`
⚠ [4048/4070] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4064/4080] 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`
⚠ [4198/4213] 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`
⚠ [4202/4269] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4207/4269] 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`
⚠ [4211/4269] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4274/4302] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4280/4302] 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`
⚠ [4282/4302] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
✔ [4289/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (406s)
ℹ [4297/4310] 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.
⚠ [4300/4310] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4349/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4351/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4395/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (117s)
⚠ [4396/4482] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
⚠ [4423/4492] 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`
✔ [4425/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (52s)
⚠ [4426/4493] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4445/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.7s)
✔ [4449/4493] Built PrimeNumberTheoremAnd.IEANTN.Lcm (33s)
⚠ [4450/4493] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (9.2s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4460/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.1s)
✔ [4462/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4464/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (16s)
⚠ [4488/4493] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1442:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1529:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1612:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2842:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2868:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3474:8: declaration uses `sorry`
✔ [4490/4493] Built PrimeNumberTheoremAnd (8.7s)
✔ [4491/4494] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.4s)
ℹ [4492/4494] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4494 jobs).

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

Command runs

git_clone exit 0 duration 947 ms · created 6/29/2026, 3:37:14 AM

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

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

git_checkout exit 0 duration 53 ms · created 6/29/2026, 3:37:14 AM

git checkout 6f8a0637eeaf00e35b6c4715decc8da160b18cc2

Note: switching to '6f8a0637eeaf00e35b6c4715decc8da160b18cc2'.

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 6f8a063 fix: use nth_prime' k in Dusart lemma_5_10a (#1627)

lake_cache exit 0 duration 1m 4s · created 6/29/2026, 3:37:14 AM

lake exe cache get

Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8546 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Decompressed 8546 file(s)
Already decompressed 8546 file(s)

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

Downloaded: 1 file(s) [attempted 1/8546 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 17 file(s) [attempted 17/8546 = 0%, 12 KB/s], Decompressed: 15
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 119 KB/s], Decompressed: 40
Downloaded: 67 file(s) [attempted 67/8546 = 0%, 55 KB/s], Decompressed: 65
Downloaded: 95 file(s) [attempted 95/8546 = 1%, 255 KB/s], Decompressed: 92
Downloaded: 136 file(s) [attempted 136/8546 = 1%, 915 KB/s], Decompressed: 129
Downloaded: 173 file(s) [attempted 173/8546 = 2%, 391 KB/s], Decompressed: 163
Downloaded: 201 file(s) [attempted 201/8546 = 2%, 82 KB/s], Decompressed: 197
Downloaded: 234 file(s) [attempted 234/8546 = 2%, 609 KB/s], Decompressed: 231
Downloaded: 275 file(s) [attempted 275/8546 = 3%, 795 KB/s], Decompressed: 268
Downloaded: 319 file(s) [attempted 319/8546 = 3%, 520 KB/s], Decompressed: 312
Downloaded: 363 file(s) [attempted 363/8546 = 4%, 1023 KB/s], Decompressed: 360
Downloaded: 400 file(s) [attempted 400/8546 = 4%, 225 KB/s], Decompressed: 397
Downloaded: 441 file(s) [attempted 441/8546 = 5%, 92 KB/s], Decompressed: 431
Downloaded: 478 file(s) [attempted 478/8546 = 5%, 435 KB/s], Decompressed: 471
Downloaded: 519 file(s) [attempted 519/8546 = 6%, 666 KB/s], Decompressed: 515
Downloaded: 563 file(s) [attempted 563/8546 = 6%, 254 KB/s], Decompressed: 559
Downloaded: 601 file(s) [attempted 601/8546 = 7%, 266 KB/s], Decompressed: 597
Downloaded: 641 file(s) [attempted 641/8546 = 7%, 168 KB/s], Decompressed: 637
Downloaded: 679 file(s) [attempted 679/8546 = 7%, 167 KB/s], Decompressed: 674
Downloaded: 722 file(s) [attempted 722/8546 = 8%, 385 KB/s], Decompressed: 718
Downloaded: 762 file(s) [attempted 762/8546 = 8%, 124 KB/s], Decompressed: 752
Downloaded: 800 file(s) [attempted 800/8546 = 9%, 131 KB/s], Decompressed: 796
Downloaded: 844 file(s) [attempted 844/8546 = 9%, 1203 KB/s], Decompressed: 837
Downloaded: 888 file(s) [attempted 888/8546 = 10%, 152 KB/s], Decompressed: 884
Downloaded: 925 file(s) [attempted 925/8546 = 10%, 1284 KB/s], Decompressed: 922
Downloaded: 949 file(s) [attempted 949/8546 = 11%, 377 KB/s], Decompressed: 945
Downloaded: 969 file(s) [attempted 969/8546 = 11%, 522 KB/s], Decompressed: 966
Downloaded: 984 file(s) [attempted 984/8546 = 11%, 27 KB/s], Decompressed: 979
Downloaded: 996 file(s) [attempted 996/8546 = 11%, 243 KB/s], Decompressed: 993
Downloaded: 1043 file(s) [attempted 1043/8546 = 12%, 719 KB/s], Decompressed: 1040
Downloaded: 1094 file(s) [attempted 1094/8546 = 12%, 41 KB/s], Decompressed: 1087
Downloaded: 1141 file(s) [attempted 1141/8546 = 13%, 491 KB/s], Decompressed: 1138
Downloaded: 1192 file(s) [attempted 1192/8546 = 13%, 144 KB/s], Decompressed: 1185
Downloaded: 1240 file(s) [attempted 1240/8546 = 14%, 421 KB/s], Decompressed: 1236
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 256 KB/s], Decompressed: 1273
Downloaded: 1317 file(s) [attempted 1317/8546 = 15%, 127 KB/s], Decompressed: 1311
Downloaded: 1355 file(s) [attempted 1355/8546 = 15%, 44 KB/s], Decompressed: 1351
Downloaded: 1402 file(s) [attempted 1402/8546 = 16%, 491 KB/s], Decompressed: 1395
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 85 KB/s], Decompressed: 1439
Downloaded: 1485 file(s) [attempted 1485/8546 = 17%, 267 KB/s], Decompressed: 1480
Downloaded: 1525 file(s) [attempted 1525/8546 = 17%, 56 KB/s], Decompressed: 1517
Downloaded: 1563 file(s) [attempted 1563/8546 = 18%, 172 KB/s], Decompressed: 1554
Downloaded: 1605 file(s) [attempted 1605/8546 = 18%, 136 KB/s], Decompressed: 1602
Downloaded: 1646 file(s) [attempted 1646/8546 = 19%, 1072 KB/s], Decompressed: 1639
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 64 KB/s], Decompressed: 1676
Downloaded: 1723 file(s) [attempted 1723/8546 = 20%, 76 KB/s], Decompressed: 1717
Downloaded: 1764 file(s) [attempted 1764/8546 = 20%, 299 KB/s], Decompressed: 1761
Downloaded: 1804 file(s) [attempted 1804/8546 = 21%, 256 KB/s], Decompressed: 1801
Downloaded: 1848 file(s) [attempted 1848/8546 = 21%, 714 KB/s], Decompressed: 1845
Downloaded: 1886 file(s) [attempted 1886/8546 = 22%, 281 KB/s], Decompressed: 1882
Downloaded: 1926 file(s) [attempted 1926/8546 = 22%, 152 KB/s], Decompressed: 1916
Downloaded: 1967 file(s) [attempted 1967/8546 = 23%, 446 KB/s], Decompressed: 1953
Downloaded: 2004 file(s) [attempted 2004/8546 = 23%, 1118 KB/s], Decompressed: 1997
Downloaded: 2048 file(s) [attempted 2048/8546 = 23%, 269 KB/s], Decompressed: 2045
Downloaded: 2089 file(s) [attempted 2089/8546 = 24%, 65 KB/s], Decompressed: 2085
Downloaded: 2129 file(s) [attempted 2129/8546 = 24%, 832 KB/s], Decompressed: 2126
Downloaded: 2173 file(s) [attempted 2173/8546 = 25%, 132 KB/s], Decompressed: 2170
Downloaded: 2214 file(s) [attempted 2214/8546 = 25%, 502 KB/s], Decompressed: 2207
Downloaded: 2258 file(s) [attempted 2258/8546 = 26%, 542 KB/s], Decompressed: 2251
Downloaded: 2302 file(s) [attempted 2302/8546 = 26%, 227 KB/s], Decompressed: 2298
Downloaded: 2342 file(s) [attempted 2342/8546 = 27%, 39 KB/s], Decompressed: 2339
Downloaded: 2383 file(s) [attempted 2383/8546 = 27%, 208 KB/s], Decompressed: 2376
Downloaded: 2420 file(s) [attempted 2420/8546 = 28%, 38 KB/s], Decompressed: 2413
Downloaded: 2461 file(s) [attempted 2461/8546 = 28%, 181 KB/s], Decompressed: 2457
Downloaded: 2507 file(s) [attempted 2507/8546 = 29%, 146 KB/s], Decompressed: 2498
Downloaded: 2546 file(s) [attempted 2546/8546 = 29%, 515 KB/s], Decompressed: 2535
Downloaded: 2586 file(s) [attempted 2586/8546 = 30%, 200 KB/s], Decompressed: 2569
Downloaded: 2623 file(s) [attempted 2623/8546 = 30%, 113 KB/s], Decompressed: 2616
Downloaded: 2667 file(s) [attempted 2667/8546 = 31%, 416 KB/s], Decompressed: 2664
Downloaded: 2714 file(s) [attempted 2714/8546 = 31%, 133 KB/s], Decompressed: 2711
Downloaded: 2752 file(s) [attempted 2752/8546 = 32%, 301 KB/s], Decompressed: 2748
Downloaded: 2796 file(s) [attempted 2796/8546 = 32%, 219 KB/s], Decompressed: 2789
Downloaded: 2836 file(s) [attempted 2836/8546 = 33%, 103 KB/s], Decompressed: 2833
Downloaded: 2878 file(s) [attempted 2878/8546 = 33%, 279 KB/s], Decompressed: 2873
Downloaded: 2914 file(s) [attempted 2914/8546 = 34%, 145 KB/s], Decompressed: 2911
Downloaded: 2958 file(s) [attempted 2958/8546 = 34%, 740 KB/s], Decompressed: 2951
Downloaded: 2999 file(s) [attempted 2999/8546 = 35%, 285 KB/s], Decompressed: 2995
Downloaded: 3043 file(s) [attempted 3043/8546 = 35%, 610 KB/s], Decompressed: 3039
Downloaded: 3087 file(s) [attempted 3087/8546 = 36%, 115 KB/s], Decompressed: 3080
Downloaded: 3127 file(s) [attempted 3127/8546 = 36%, 238 KB/s], Decompressed: 3120
Downloaded: 3166 file(s) [attempted 3166/8546 = 37%, 84 KB/s], Decompressed: 3154
Downloaded: 3205 file(s) [attempted 3205/8546 = 37%, 1276 KB/s], Decompressed: 3198
Downloaded: 3249 file(s) [attempted 3249/8546 = 38%, 53 KB/s], Decompressed: 3246
Downloaded: 3289 file(s) [attempted 3289/8546 = 38%, 101 KB/s], Decompressed: 3286
Downloaded: 3337 file(s) [attempted 3337/8546 = 39%, 399 KB/s], Decompressed: 3333
Downloaded: 3381 file(s) [attempted 3381/8546 = 39%, 488 KB/s], Decompressed: 3371
Downloaded: 3425 file(s) [attempted 3425/8546 = 40%, 62 KB/s], Decompressed: 3405
Downloaded: 3465 file(s) [attempted 3465/8546 = 40%, 448 KB/s], Decompressed: 3462
Downloaded: 3503 file(s) [attempted 3503/8546 = 40%, 192 KB/s], Decompressed: 3499
Downloaded: 3541 file(s) [attempted 3541/8546 = 41%, 284 KB/s], Decompressed: 3536
Downloaded: 3587 file(s) [attempted 3587/8546 = 41%, 228 KB/s], Decompressed: 3584
Downloaded: 3632 file(s) [attempted 3632/8546 = 42%, 118 KB/s], Decompressed: 3628
Downloaded: 3668 file(s) [attempted 3668/8546 = 42%, 108 KB/s], Decompressed: 3658
Downloaded: 3712 file(s) [attempted 3712/8546 = 43%, 35 KB/s], Decompressed: 3706
Downloaded: 3756 file(s) [attempted 3756/8546 = 43%, 251 KB/s], Decompressed: 3753
Downloaded: 3804 file(s) [attempted 3804/8546 = 44%, 313 KB/s], Decompressed: 3800
Downloaded: 3851 file(s) [attempted 3851/8546 = 45%, 63 KB/s], Decompressed: 3844
Downloaded: 3892 file(s) [attempted 3892/8546 = 45%, 146 KB/s], Decompressed: 3888
Downloaded: 3925 file(s) [attempted 3925/8546 = 45%, 555 KB/s], Decompressed: 3915
Downloaded: 3966 file(s) [attempted 3966/8546 = 46%, 241 KB/s], Decompressed: 3963
Downloaded: 4010 file(s) [attempted 4010/8546 = 46%, 354 KB/s], Decompressed: 4007
Downloaded: 4057 file(s) [attempted 4057/8546 = 47%, 241 KB/s], Decompressed: 4051
Downloaded: 4105 file(s) [attempted 4105/8546 = 48%, 1281 KB/s], Decompressed: 4098
Downloaded: 4145 file(s) [attempted 4145/8546 = 48%, 468 KB/s], Decompressed: 4142
Downloaded: 4183 file(s) [attempted 4183/8546 = 48%, 795 KB/s], Decompressed: 4176
Downloaded: 4223 file(s) [attempted 4223/8546 = 49%, 450 KB/s], Decompressed: 4220
Downloaded: 4267 file(s) [attempted 4267/8546 = 49%, 378 KB/s], Decompressed: 4260
Downloaded: 4311 file(s) [attempted 4311/8546 = 50%, 78 KB/s], Decompressed: 4308
Downloaded: 4355 file(s) [attempted 4355/8546 = 50%, 447 KB/s], Decompressed: 4351
Downloaded: 4392 file(s) [attempted 4392/8546 = 51%, 358 KB/s], Decompressed: 4389
Downloaded: 4434 file(s) [attempted 4434/8546 = 51%, 36 KB/s], Decompressed: 4429
Downloaded: 4473 file(s) [attempted 4473/8546 = 52%, 88 KB/s], Decompressed: 4463
Downloaded: 4516 file(s) [attempted 4516/8546 = 52%, 411 KB/s], Decompressed: 4511
Downloaded: 4555 file(s) [attempted 4555/8546 = 53%, 269 KB/s], Decompressed: 4541
Downloaded: 4592 file(s) [attempted 4592/8546 = 53%, 140 KB/s], Decompressed: 4585
Downloaded: 4636 file(s) [attempted 4636/8546 = 54%, 505 KB/s], Decompressed: 4632
Downloaded: 4680 file(s) [attempted 4680/8546 = 54%, 1098 KB/s], Decompressed: 4670
Downloaded: 4717 file(s) [attempted 4717/8546 = 55%, 722 KB/s], Decompressed: 4710
Downloaded: 4754 file(s) [attempted 4754/8546 = 55%, 169 KB/s], Decompressed: 4751
Downloaded: 4798 file(s) [attempted 4798/8546 = 56%, 23 KB/s], Decompressed: 4791
Downloaded: 4839 file(s) [attempted 4839/8546 = 56%, 52 KB/s], Decompressed: 4835
Downloaded: 4883 file(s) [attempted 4883/8546 = 57%, 197 KB/s], Decompressed: 4879
Downloaded: 4928 file(s) [attempted 4928/8546 = 57%, 93 KB/s], Decompressed: 4923
Downloaded: 4967 file(s) [attempted 4967/8546 = 58%, 766 KB/s], Decompressed: 4961
Downloaded: 5005 file(s) [attempted 5005/8546 = 58%, 218 KB/s], Decompressed: 4994
Downloaded: 5043 file(s) [attempted 5043/8546 = 59%, 107 KB/s], Decompressed: 5038
Downloaded: 5082 file(s) [attempted 5082/8546 = 59%, 333 KB/s], Decompressed: 5079
Downloaded: 5126 file(s) [attempted 5126/8546 = 59%, 492 KB/s], Decompressed: 5120
Downloaded: 5170 file(s) [attempted 5170/8546 = 60%, 112 KB/s], Decompressed: 5167
Downloaded: 5208 file(s) [attempted 5208/8546 = 60%, 1336 KB/s], Decompressed: 5204
Downloaded: 5249 file(s) [attempted 5249/8546 = 61%, 102 KB/s], Decompressed: 5245
Downloaded: 5292 file(s) [attempted 5292/8546 = 61%, 327 KB/s], Decompressed: 5285
Downloaded: 5333 file(s) [attempted 5333/8546 = 62%, 447 KB/s], Decompressed: 5329
Downloaded: 5380 file(s) [attempted 5380/8546 = 62%, 232 KB/s], Decompressed: 5377
Downloaded: 5427 file(s) [attempted 5427/8546 = 63%, 320 KB/s], Decompressed: 5411
Downloaded: 5461 file(s) [attempted 5461/8546 = 63%, 285 KB/s], Decompressed: 5455
Downloaded: 5502 file(s) [attempted 5502/8546 = 64%, 529 KB/s], Decompressed: 5498
Downloaded: 5542 file(s) [attempted 5542/8546 = 64%, 258 KB/s], Decompressed: 5536
Downloaded: 5586 file(s) [attempted 5586/8546 = 65%, 88 KB/s], Decompressed: 5580
Downloaded: 5634 file(s) [attempted 5634/8546 = 65%, 98 KB/s], Decompressed: 5627
Downloaded: 5674 file(s) [attempted 5674/8546 = 66%, 1260 KB/s], Decompressed: 5671
Downloaded: 5715 file(s) [attempted 5715/8546 = 66%, 914 KB/s], Decompressed: 5708
Downloaded: 5753 file(s) [attempted 5753/8546 = 67%, 110 KB/s], Decompressed: 5745
Downloaded: 5790 file(s) [attempted 5790/8546 = 67%, 1807 KB/s], Decompressed: 5783
Downloaded: 5833 file(s) [attempted 5833/8546 = 68%, 238 KB/s], Decompressed: 5830
Downloaded: 5874 file(s) [attempted 5874/8546 = 68%, 271 KB/s], Decompressed: 5871
Downloaded: 5918 file(s) [attempted 5918/8546 = 69%, 590 KB/s], Decompressed: 5908
Downloaded: 5959 file(s) [attempted 5959/8546 = 69%, 721 KB/s], Decompressed: 5948
Downloaded: 5998 file(s) [attempted 5998/8546 = 70%, 152 KB/s], Decompressed: 5969
Downloaded: 6036 file(s) [attempted 6036/8546 = 70%, 224 KB/s], Decompressed: 6033
Downloaded: 6080 file(s) [attempted 6080/8546 = 71%, 295 KB/s], Decompressed: 6077
Downloaded: 6124 file(s) [attempted 6124/8546 = 71%, 225 KB/s], Decompressed: 6118
Downloaded: 6158 file(s) [attempted 6158/8546 = 72%, 1986 KB/s], Decompressed: 6151
Downloaded: 6205 file(s) [attempted 6205/8546 = 72%, 277 KB/s], Decompressed: 6202
Downloaded: 6243 file(s) [attempted 6243/8546 = 73%, 284 KB/s], Decompressed: 6233
Downloaded: 6283 file(s) [attempted 6283/8546 = 73%, 491 KB/s], Decompressed: 6280
Downloaded: 6322 file(s) [attempted 6322/8546 = 73%, 1012 KB/s], Decompressed: 6310
Downloaded: 6358 file(s) [attempted 6358/8546 = 74%, 345 KB/s], Decompressed: 6354
Downloaded: 6402 file(s) [attempted 6402/8546 = 74%, 372 KB/s], Decompressed: 6398
Downloaded: 6446 file(s) [attempted 6446/8546 = 75%, 498 KB/s], Decompressed: 6442
Downloaded: 6486 file(s) [attempted 6486/8546 = 75%, 507 KB/s], Decompressed: 6483
Downloaded: 6523 file(s) [attempted 6523/8546 = 76%, 1730 KB/s], Decompressed: 6518
Downloaded: 6564 file(s) [attempted 6564/8546 = 76%, 759 KB/s], Decompressed: 6561
Downloaded: 6608 file(s) [attempted 6608/8546 = 77%, 452 KB/s], Decompressed: 6605
Downloaded: 6652 file(s) [attempted 6652/8546 = 77%, 396 KB/s], Decompressed: 6649
Downloaded: 6696 file(s) [attempted 6696/8546 = 78%, 53 KB/s], Decompressed: 6686
Downloaded: 6733 file(s) [attempted 6733/8546 = 78%, 75 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8546 = 79%, 127 KB/s], Decompressed: 6770
Downloaded: 6814 file(s) [attempted 6814/8546 = 79%, 288 KB/s], Decompressed: 6811
Downloaded: 6858 file(s) [attempted 6858/8546 = 80%, 81 KB/s], Decompressed: 6855
Downloaded: 6902 file(s) [attempted 6902/8546 = 80%, 43 KB/s], Decompressed: 6892
Downloaded: 6943 file(s) [attempted 6943/8546 = 81%, 109 KB/s], Decompressed: 6936
Downloaded: 6987 file(s) [attempted 6987/8546 = 81%, 450 KB/s], Decompressed: 6980
Downloaded: 7027 file(s) [attempted 7027/8546 = 82%, 213 KB/s], Decompressed: 7017
Downloaded: 7065 file(s) [attempted 7065/8546 = 82%, 1699 KB/s], Decompressed: 7058
Downloaded: 7105 file(s) [attempted 7105/8546 = 83%, 353 KB/s], Decompressed: 7102
Downloaded: 7149 file(s) [attempted 7149/8546 = 83%, 304 KB/s], Decompressed: 7146
Downloaded: 7197 file(s) [attempted 7197/8546 = 84%, 526 KB/s], Decompressed: 7188
Downloaded: 7244 file(s) [attempted 7244/8546 = 84%, 704 KB/s], Decompressed: 7234
Downloaded: 7281 file(s) [attempted 7281/8546 = 85%, 79 KB/s], Decompressed: 7278
Downloaded: 7322 file(s) [attempted 7322/8546 = 85%, 92 KB/s], Decompressed: 7315
Downloaded: 7362 file(s) [attempted 7362/8546 = 86%, 165 KB/s], Decompressed: 7359
Downloaded: 7406 file(s) [attempted 7406/8546 = 86%, 738 KB/s], Decompressed: 7396
Downloaded: 7450 file(s) [attempted 7450/8546 = 87%, 74 KB/s], Decompressed: 7447
Downloaded: 7494 file(s) [attempted 7494/8546 = 87%, 24 KB/s], Decompressed: 7477
Downloaded: 7530 file(s) [attempted 7530/8546 = 88%, 327 KB/s], Decompressed: 7521
Downloaded: 7569 file(s) [attempted 7569/8546 = 88%, 424 KB/s], Decompressed: 7565
Downloaded: 7613 file(s) [attempted 7613/8546 = 89%, 131 KB/s], Decompressed: 7609
Downloaded: 7657 file(s) [attempted 7657/8546 = 89%, 72 KB/s], Decompressed: 7650
Downloaded: 7701 file(s) [attempted 7701/8546 = 90%, 178 KB/s], Decompressed: 7694
Downloaded: 7734 file(s) [attempted 7734/8546 = 90%, 44 KB/s], Decompressed: 7731
Downloaded: 7773 file(s) [attempted 7773/8546 = 90%, 484 KB/s], Decompressed: 7768
Downloaded: 7816 file(s) [attempted 7816/8546 = 91%, 139 KB/s], Decompressed: 7812
Downloaded: 7861 file(s) [attempted 7861/8546 = 91%, 194 KB/s], Decompressed: 7856
Downloaded: 7900 file(s) [attempted 7900/8546 = 92%, 22 KB/s], Decompressed: 7893
Downloaded: 7941 file(s) [attempted 7941/8546 = 92%, 2377 KB/s], Decompressed: 7927
Downloaded: 7978 file(s) [attempted 7978/8546 = 93%, 62 KB/s], Decompressed: 7975
Downloaded: 8022 file(s) [attempted 8022/8546 = 93%, 278 KB/s], Decompressed: 8015
Downloaded: 8063 file(s) [attempted 8063/8546 = 94%, 1028 KB/s], Decompressed: 8056
Downloaded: 8110 file(s) [attempted 8110/8546 = 94%, 166 KB/s], Decompressed: 8103
Downloaded: 8154 file(s) [attempted 8154/8546 = 95%, 252 KB/s], Decompressed: 8150
Downloaded: 8194 file(s) [attempted 8194/8546 = 95%, 313 KB/s], Decompressed: 8181
Downloaded: 8232 file(s) [attempted 8232/8546 = 96%, 355 KB/s], Decompressed: 8228
Downloaded: 8276 file(s) [attempted 8276/8546 = 96%, 39 KB/s], Decompressed: 8272
Downloaded: 8316 file(s) [attempted 8316/8546 = 97%, 293 KB/s], Decompressed: 8309
Downloaded: 8360 file(s) [attempted 8360/8546 = 97%, 562 KB/s], Decompressed: 8350
Downloaded: 8401 file(s) [attempted 8401/8546 = 98%, 2756 KB/s], Decompressed: 8387
Downloaded: 8443 file(s) [attempted 8443/8546 = 98%, 570 KB/s], Decompressed: 8438
Downloaded: 8482 file(s) [attempted 8482/8546 = 99%, 556 KB/s], Decompressed: 8472
Downloaded: 8523 file(s) [attempted 8523/8546 = 99%, 750 KB/s], Decompressed: 8519
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 750 KB/s], Decompressed: 8540

lean_checker exit - duration 2h 0m · created 6/29/2026, 3:37:14 AM

lake build

ℹ [3628/3638] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3651/3667] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
⚠ [3778/3799] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3895/3910] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3965/3986] 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`
⚠ [3967/3986] 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`
⚠ [3968/3986] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4109/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`
⚠ [4110/4114] 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`
⚠ [4112/4154] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4113/4154] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4155/4165] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4158/4165] 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`
⚠ [4161/4165] Built PrimeNumberTheoremAnd.IEANTN.Dusart (244s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
ℹ [4167/4175] 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.
⚠ [4169/4175] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4200/4210] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4201/4210] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4222/4262] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (210s)
⚠ [4240/4277] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (204s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
⚠ [4247/4277] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (205s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
⚠ [4256/4284] 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`
✔ [4259/4284] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (6049s)

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 7200s
podman cleanup removed verifier container apx-verifier-job-741-runtime-lean_checker-2850807-1782696279415263621-1

blueprint_build exit 0 duration 12m 23s · created 6/29/2026, 3:37:14 AM

lake build :blueprint

✔ [27/35] Built Cli.Basic:c.o (4.7s)
✔ [30/35] Built Cli.Extensions:c.o (528ms)
✔ [33/35] Built Cli:c.o (70ms)
ℹ [3682/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3715/3734] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
⚠ [3849/3864] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4045/4070] 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`
⚠ [4048/4070] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4064/4080] 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`
⚠ [4198/4213] 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`
⚠ [4202/4269] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4207/4269] 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`
⚠ [4211/4269] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4274/4302] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4280/4302] 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`
⚠ [4282/4302] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
✔ [4289/4302] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (406s)
ℹ [4297/4310] 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.
⚠ [4300/4310] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4349/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4351/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4395/4482] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (117s)
⚠ [4396/4482] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
⚠ [4423/4492] 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`
✔ [4425/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (52s)
⚠ [4426/4493] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4445/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.7s)
✔ [4449/4493] Built PrimeNumberTheoremAnd.IEANTN.Lcm (33s)
⚠ [4450/4493] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (9.2s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4460/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.1s)
✔ [4462/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4464/4493] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (16s)
⚠ [4488/4493] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1442:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1529:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1612:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2842:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2868:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3474:8: declaration uses `sorry`
✔ [4490/4493] Built PrimeNumberTheoremAnd (8.7s)
✔ [4491/4494] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.4s)
ℹ [4492/4494] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4494 jobs).

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