Verification run

Run 154

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via manual

succeeded commit 6739793850d3 toolchain lean-v4-31-0 prover lean took 6m 40s · finished 4d ago

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

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


$ git checkout 6739793850d3eaa031e3543ed72d7f026f8080f5
exit_code=Some(0) duration_ms=41
stderr:
Note: switching to '6739793850d3eaa031e3543ed72d7f026f8080f5'.

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 6739793 feat(FKS2): Corollary 23 — all 9 Table-6 rows (#722) (#1629)

Resolved source revision: 6739793850d3eaa031e3543ed72d7f026f8080f5

Detected prover: lean
Detected requested toolchain: lean-v4-31-0
Materialized Lean semantic helper assets
Prepared source: revision=6739793850d3eaa031e3543ed72d7f026f8080f5 provenance={"branch":"main","checked_out_revision":"6739793850d3eaa031e3543ed72d7f026f8080f5","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"6739793850d3eaa031e3543ed72d7f026f8080f5","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: computed 192 best-effort Rust module fact(s) for cache lookup
Lean semantic module cache: 192/192 module hit(s), 0 miss(es); wrote full cached semantic response; skipping semantic_extract

$ lake exe cache get
exit_code=Some(0) duration_ms=74455
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%, 10 KB/s], Decompressed: 0
Downloaded: 18 file(s) [attempted 18/8546 = 0%, 11 KB/s], Decompressed: 17
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 270 KB/s], Decompressed: 40
Downloaded: 66 file(s) [attempted 66/8546 = 0%, 202 KB/s], Decompressed: 60
Downloaded: 84 file(s) [attempted 84/8546 = 0%, 163 KB/s], Decompressed: 78
Downloaded: 119 file(s) [attempted 119/8546 = 1%, 253 KB/s], Decompressed: 116
Downloaded: 156 file(s) [attempted 156/8546 = 1%, 616 KB/s], Decompressed: 150
Downloaded: 194 file(s) [attempted 194/8546 = 2%, 184 KB/s], Decompressed: 190
Downloaded: 224 file(s) [attempted 224/8546 = 2%, 214 KB/s], Decompressed: 221
Downloaded: 258 file(s) [attempted 258/8546 = 3%, 795 KB/s], Decompressed: 241
Downloaded: 292 file(s) [attempted 292/8546 = 3%, 65 KB/s], Decompressed: 288
Downloaded: 332 file(s) [attempted 332/8546 = 3%, 307 KB/s], Decompressed: 329
Downloaded: 370 file(s) [attempted 370/8546 = 4%, 191 KB/s], Decompressed: 366
Downloaded: 410 file(s) [attempted 410/8546 = 4%, 182 KB/s], Decompressed: 407
Downloaded: 448 file(s) [attempted 448/8546 = 5%, 257 KB/s], Decompressed: 444
Downloaded: 481 file(s) [attempted 481/8546 = 5%, 676 KB/s], Decompressed: 478
Downloaded: 525 file(s) [attempted 525/8546 = 6%, 762 KB/s], Decompressed: 519
Downloaded: 566 file(s) [attempted 566/8546 = 6%, 569 KB/s], Decompressed: 563
Downloaded: 607 file(s) [attempted 607/8546 = 7%, 351 KB/s], Decompressed: 603
Downloaded: 647 file(s) [attempted 647/8546 = 7%, 92 KB/s], Decompressed: 637
Downloaded: 685 file(s) [attempted 685/8546 = 8%, 152 KB/s], Decompressed: 674
Downloaded: 729 file(s) [attempted 729/8546 = 8%, 419 KB/s], Decompressed: 722
Downloaded: 769 file(s) [attempted 769/8546 = 8%, 765 KB/s], Decompressed: 762
Downloaded: 806 file(s) [attempted 806/8546 = 9%, 289 KB/s], Decompressed: 800
Downloaded: 847 file(s) [attempted 847/8546 = 9%, 505 KB/s], Decompressed: 844
Downloaded: 884 file(s) [attempted 884/8546 = 10%, 370 KB/s], Decompressed: 878
Downloaded: 926 file(s) [attempted 926/8546 = 10%, 203 KB/s], Decompressed: 922
Downloaded: 966 file(s) [attempted 966/8546 = 11%, 409 KB/s], Decompressed: 962
Downloaded: 1008 file(s) [attempted 1008/8546 = 11%, 210 KB/s], Decompressed: 999
Downloaded: 1043 file(s) [attempted 1043/8546 = 12%, 636 KB/s], Decompressed: 1038
Downloaded: 1081 file(s) [attempted 1081/8546 = 12%, 231 KB/s], Decompressed: 1077
Downloaded: 1121 file(s) [attempted 1121/8546 = 13%, 362 KB/s], Decompressed: 1118
Downloaded: 1165 file(s) [attempted 1165/8546 = 13%, 108 KB/s], Decompressed: 1164
Downloaded: 1206 file(s) [attempted 1206/8546 = 14%, 531 KB/s], Decompressed: 1202
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 407 KB/s], Decompressed: 1240
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 57 KB/s], Decompressed: 1273
Downloaded: 1323 file(s) [attempted 1323/8546 = 15%, 452 KB/s], Decompressed: 1317
Downloaded: 1368 file(s) [attempted 1368/8546 = 16%, 218 KB/s], Decompressed: 1365
Downloaded: 1409 file(s) [attempted 1409/8546 = 16%, 106 KB/s], Decompressed: 1405
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 85 KB/s], Decompressed: 1443
Downloaded: 1483 file(s) [attempted 1483/8546 = 17%, 1712 KB/s], Decompressed: 1480
Downloaded: 1525 file(s) [attempted 1525/8546 = 17%, 259 KB/s], Decompressed: 1520
Downloaded: 1571 file(s) [attempted 1571/8546 = 18%, 66 KB/s], Decompressed: 1554
Downloaded: 1615 file(s) [attempted 1615/8546 = 18%, 469 KB/s], Decompressed: 1605
Downloaded: 1649 file(s) [attempted 1649/8546 = 19%, 239 KB/s], Decompressed: 1646
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 1051 KB/s], Decompressed: 1683
Downloaded: 1727 file(s) [attempted 1727/8546 = 20%, 164 KB/s], Decompressed: 1723
Downloaded: 1771 file(s) [attempted 1771/8546 = 20%, 944 KB/s], Decompressed: 1767
Downloaded: 1808 file(s) [attempted 1808/8546 = 21%, 147 KB/s], Decompressed: 1804
Downloaded: 1844 file(s) [attempted 1844/8546 = 21%, 110 KB/s], Decompressed: 1838
Downloaded: 1879 file(s) [attempted 1879/8546 = 21%, 1268 KB/s], Decompressed: 1876
Downloaded: 1923 file(s) [attempted 1923/8546 = 22%, 42 KB/s], Decompressed: 1916
Downloaded: 1963 file(s) [attempted 1963/8546 = 22%, 404 KB/s], Decompressed: 1957
Downloaded: 1997 file(s) [attempted 1997/8546 = 23%, 39 KB/s], Decompressed: 1991
Downloaded: 2038 file(s) [attempted 2038/8546 = 23%, 181 KB/s], Decompressed: 2031
Downloaded: 2075 file(s) [attempted 2075/8546 = 24%, 466 KB/s], Decompressed: 2072
Downloaded: 2119 file(s) [attempted 2119/8546 = 24%, 301 KB/s], Decompressed: 2116
Downloaded: 2157 file(s) [attempted 2157/8546 = 25%, 134 KB/s], Decompressed: 2153
Downloaded: 2190 file(s) [attempted 2190/8546 = 25%, 55 KB/s], Decompressed: 2188
Downloaded: 2237 file(s) [attempted 2237/8546 = 26%, 185 KB/s], Decompressed: 2234
Downloaded: 2282 file(s) [attempted 2282/8546 = 26%, 72 KB/s], Decompressed: 2278
Downloaded: 2325 file(s) [attempted 2325/8546 = 27%, 328 KB/s], Decompressed: 2319
Downloaded: 2363 file(s) [attempted 2363/8546 = 27%, 371 KB/s], Decompressed: 2336
Downloaded: 2403 file(s) [attempted 2403/8546 = 28%, 127 KB/s], Decompressed: 2393
Downloaded: 2437 file(s) [attempted 2437/8546 = 28%, 521 KB/s], Decompressed: 2434
Downloaded: 2482 file(s) [attempted 2482/8546 = 29%, 320 KB/s], Decompressed: 2474
Downloaded: 2524 file(s) [attempted 2524/8546 = 29%, 1438 KB/s], Decompressed: 2515
Downloaded: 2559 file(s) [attempted 2559/8546 = 29%, 580 KB/s], Decompressed: 2549
Downloaded: 2596 file(s) [attempted 2596/8546 = 30%, 165 KB/s], Decompressed: 2593
Downloaded: 2639 file(s) [attempted 2639/8546 = 30%, 106 KB/s], Decompressed: 2633
Downloaded: 2681 file(s) [attempted 2681/8546 = 31%, 60 KB/s], Decompressed: 2677
Downloaded: 2725 file(s) [attempted 2725/8546 = 31%, 935 KB/s], Decompressed: 2704
Downloaded: 2758 file(s) [attempted 2758/8546 = 32%, 124 KB/s], Decompressed: 2752
Downloaded: 2797 file(s) [attempted 2797/8546 = 32%, 250 KB/s], Decompressed: 2792
Downloaded: 2840 file(s) [attempted 2840/8546 = 33%, 556 KB/s], Decompressed: 2829
Downloaded: 2884 file(s) [attempted 2884/8546 = 33%, 247 KB/s], Decompressed: 2880
Downloaded: 2928 file(s) [attempted 2928/8546 = 34%, 962 KB/s], Decompressed: 2917
Downloaded: 2965 file(s) [attempted 2965/8546 = 34%, 1025 KB/s], Decompressed: 2961
Downloaded: 3002 file(s) [attempted 3002/8546 = 35%, 633 KB/s], Decompressed: 2995
Downloaded: 3041 file(s) [attempted 3041/8546 = 35%, 200 KB/s], Decompressed: 3032
Downloaded: 3083 file(s) [attempted 3083/8546 = 36%, 2110 KB/s], Decompressed: 3080
Downloaded: 3121 file(s) [attempted 3121/8546 = 36%, 531 KB/s], Decompressed: 3117
Downloaded: 3163 file(s) [attempted 3163/8546 = 37%, 52 KB/s], Decompressed: 3154
Downloaded: 3205 file(s) [attempted 3205/8546 = 37%, 472 KB/s], Decompressed: 3191
Downloaded: 3246 file(s) [attempted 3246/8546 = 37%, 169 KB/s], Decompressed: 3239
Downloaded: 3286 file(s) [attempted 3286/8546 = 38%, 541 KB/s], Decompressed: 3283
Downloaded: 3333 file(s) [attempted 3333/8546 = 39%, 1210 KB/s], Decompressed: 3330
Downloaded: 3373 file(s) [attempted 3373/8546 = 39%, 54 KB/s], Decompressed: 3367
Downloaded: 3410 file(s) [attempted 3410/8546 = 39%, 1435 KB/s], Decompressed: 3401
Downloaded: 3448 file(s) [attempted 3448/8546 = 40%, 1929 KB/s], Decompressed: 3438
Downloaded: 3489 file(s) [attempted 3489/8546 = 40%, 220 KB/s], Decompressed: 3486
Downloaded: 3536 file(s) [attempted 3536/8546 = 41%, 23 KB/s], Decompressed: 3533
Downloaded: 3584 file(s) [attempted 3584/8546 = 41%, 117 KB/s], Decompressed: 3567
Downloaded: 3623 file(s) [attempted 3623/8546 = 42%, 442 KB/s], Decompressed: 3607
Downloaded: 3659 file(s) [attempted 3659/8546 = 42%, 625 KB/s], Decompressed: 3651
Downloaded: 3695 file(s) [attempted 3695/8546 = 43%, 323 KB/s], Decompressed: 3689
Downloaded: 3739 file(s) [attempted 3739/8546 = 43%, 485 KB/s], Decompressed: 3736
Downloaded: 3787 file(s) [attempted 3787/8546 = 44%, 46 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8546 = 44%, 101 KB/s], Decompressed: 3800
Downloaded: 3852 file(s) [attempted 3852/8546 = 45%, 59 KB/s], Decompressed: 3848
Downloaded: 3898 file(s) [attempted 3898/8546 = 45%, 361 KB/s], Decompressed: 3885
Downloaded: 3942 file(s) [attempted 3942/8546 = 46%, 133 KB/s], Decompressed: 3932
Downloaded: 3980 file(s) [attempted 3980/8546 = 46%, 284 KB/s], Decompressed: 3969
Downloaded: 4017 file(s) [attempted 4017/8546 = 47%, 120 KB/s], Decompressed: 4013
Downloaded: 4061 file(s) [attempted 4061/8546 = 47%, 799 KB/s], Decompressed: 4057
Downloaded: 4105 file(s) [attempted 4105/8546 = 48%, 329 KB/s], Decompressed: 4098
Downloaded: 4142 file(s) [attempted 4142/8546 = 48%, 155 KB/s], Decompressed: 4125
Downloaded: 4180 file(s) [attempted 4180/8546 = 48%, 970 KB/s], Decompressed: 4176
Downloaded: 4220 file(s) [attempted 4220/8546 = 49%, 323 KB/s], Decompressed: 4216
Downloaded: 4264 file(s) [attempted 4264/8546 = 49%, 322 KB/s], Decompressed: 4260
Downloaded: 4304 file(s) [attempted 4304/8546 = 50%, 393 KB/s], Decompressed: 4298
Downloaded: 4338 file(s) [attempted 4338/8546 = 50%, 113 KB/s], Decompressed: 4335
Downloaded: 4379 file(s) [attempted 4379/8546 = 51%, 141 KB/s], Decompressed: 4375
Downloaded: 4423 file(s) [attempted 4423/8546 = 51%, 921 KB/s], Decompressed: 4416
Downloaded: 4463 file(s) [attempted 4463/8546 = 52%, 140 KB/s], Decompressed: 4460
Downloaded: 4507 file(s) [attempted 4507/8546 = 52%, 136 KB/s], Decompressed: 4504
Downloaded: 4541 file(s) [attempted 4541/8546 = 53%, 233 KB/s], Decompressed: 4538
Downloaded: 4582 file(s) [attempted 4582/8546 = 53%, 41 KB/s], Decompressed: 4575
Downloaded: 4622 file(s) [attempted 4622/8546 = 54%, 226 KB/s], Decompressed: 4616
Downloaded: 4666 file(s) [attempted 4666/8546 = 54%, 699 KB/s], Decompressed: 4660
Downloaded: 4706 file(s) [attempted 4706/8546 = 55%, 20 KB/s], Decompressed: 4693
Downloaded: 4737 file(s) [attempted 4737/8546 = 55%, 69 KB/s], Decompressed: 4734
Downloaded: 4778 file(s) [attempted 4778/8546 = 55%, 84 KB/s], Decompressed: 4775
Downloaded: 4825 file(s) [attempted 4825/8546 = 56%, 529 KB/s], Decompressed: 4822
Downloaded: 4869 file(s) [attempted 4869/8546 = 56%, 272 KB/s], Decompressed: 4829
Downloaded: 4910 file(s) [attempted 4910/8546 = 57%, 369 KB/s], Decompressed: 4896
Downloaded: 4944 file(s) [attempted 4944/8546 = 57%, 114 KB/s], Decompressed: 4923
Downloaded: 4984 file(s) [attempted 4984/8546 = 58%, 507 KB/s], Decompressed: 4981
Downloaded: 5028 file(s) [attempted 5028/8546 = 58%, 394 KB/s], Decompressed: 5022
Downloaded: 5072 file(s) [attempted 5072/8546 = 59%, 40 KB/s], Decompressed: 5069
Downloaded: 5116 file(s) [attempted 5116/8546 = 59%, 380 KB/s], Decompressed: 5113
Downloaded: 5160 file(s) [attempted 5160/8546 = 60%, 110 KB/s], Decompressed: 5153
Downloaded: 5191 file(s) [attempted 5191/8546 = 60%, 38 KB/s], Decompressed: 5187
Downloaded: 5238 file(s) [attempted 5238/8546 = 61%, 100 KB/s], Decompressed: 5231
Downloaded: 5279 file(s) [attempted 5279/8546 = 61%, 62 KB/s], Decompressed: 5275
Downloaded: 5323 file(s) [attempted 5323/8546 = 62%, 550 KB/s], Decompressed: 5319
Downloaded: 5364 file(s) [attempted 5364/8546 = 62%, 27 KB/s], Decompressed: 5356
Downloaded: 5397 file(s) [attempted 5397/8546 = 63%, 198 KB/s], Decompressed: 5394
Downloaded: 5441 file(s) [attempted 5441/8546 = 63%, 777 KB/s], Decompressed: 5438
Downloaded: 5482 file(s) [attempted 5482/8546 = 64%, 120 KB/s], Decompressed: 5478
Downloaded: 5522 file(s) [attempted 5522/8546 = 64%, 486 KB/s], Decompressed: 5509
Downloaded: 5569 file(s) [attempted 5569/8546 = 65%, 366 KB/s], Decompressed: 5556
Downloaded: 5603 file(s) [attempted 5603/8546 = 65%, 39 KB/s], Decompressed: 5597
Downloaded: 5644 file(s) [attempted 5644/8546 = 66%, 170 KB/s], Decompressed: 5641
Downloaded: 5681 file(s) [attempted 5681/8546 = 66%, 194 KB/s], Decompressed: 5678
Downloaded: 5725 file(s) [attempted 5725/8546 = 66%, 43 KB/s], Decompressed: 5718
Downloaded: 5766 file(s) [attempted 5766/8546 = 67%, 311 KB/s], Decompressed: 5759
Downloaded: 5804 file(s) [attempted 5804/8546 = 67%, 104 KB/s], Decompressed: 5800
Downloaded: 5847 file(s) [attempted 5847/8546 = 68%, 153 KB/s], Decompressed: 5844
Downloaded: 5888 file(s) [attempted 5888/8546 = 68%, 108 KB/s], Decompressed: 5884
Downloaded: 5931 file(s) [attempted 5931/8546 = 69%, 401 KB/s], Decompressed: 5925
Downloaded: 5969 file(s) [attempted 5969/8546 = 69%, 338 KB/s], Decompressed: 5955
Downloaded: 6006 file(s) [attempted 6006/8546 = 70%, 666 KB/s], Decompressed: 5975
Downloaded: 6047 file(s) [attempted 6047/8546 = 70%, 776 KB/s], Decompressed: 6040
Downloaded: 6090 file(s) [attempted 6090/8546 = 71%, 283 KB/s], Decompressed: 6087
Downloaded: 6134 file(s) [attempted 6134/8546 = 71%, 482 KB/s], Decompressed: 6124
Downloaded: 6167 file(s) [attempted 6167/8546 = 72%, 224 KB/s], Decompressed: 6162
Downloaded: 6209 file(s) [attempted 6209/8546 = 72%, 765 KB/s], Decompressed: 6205
Downloaded: 6253 file(s) [attempted 6253/8546 = 73%, 2517 KB/s], Decompressed: 6246
Downloaded: 6293 file(s) [attempted 6293/8546 = 73%, 57 KB/s], Decompressed: 6283
Downloaded: 6327 file(s) [attempted 6327/8546 = 74%, 94 KB/s], Decompressed: 6321
Downloaded: 6364 file(s) [attempted 6364/8546 = 74%, 2475 KB/s], Decompressed: 6361
Downloaded: 6408 file(s) [attempted 6408/8546 = 74%, 569 KB/s], Decompressed: 6405
Downloaded: 6452 file(s) [attempted 6452/8546 = 75%, 895 KB/s], Decompressed: 6439
Downloaded: 6496 file(s) [attempted 6496/8546 = 76%, 144 KB/s], Decompressed: 6479
Downloaded: 6530 file(s) [attempted 6530/8546 = 76%, 295 KB/s], Decompressed: 6523
Downloaded: 6574 file(s) [attempted 6574/8546 = 76%, 169 KB/s], Decompressed: 6567
Downloaded: 6618 file(s) [attempted 6618/8546 = 77%, 57 KB/s], Decompressed: 6611
Downloaded: 6659 file(s) [attempted 6659/8546 = 77%, 426 KB/s], Decompressed: 6649
Downloaded: 6699 file(s) [attempted 6699/8546 = 78%, 110 KB/s], Decompressed: 6686
Downloaded: 6734 file(s) [attempted 6734/8546 = 78%, 327 KB/s], Decompressed: 6730
Downloaded: 6774 file(s) [attempted 6774/8546 = 79%, 1390 KB/s], Decompressed: 6770
Downloaded: 6818 file(s) [attempted 6818/8546 = 79%, 64 KB/s], Decompressed: 6811
Downloaded: 6855 file(s) [attempted 6855/8546 = 80%, 24 KB/s], Decompressed: 6852
Downloaded: 6896 file(s) [attempted 6896/8546 = 80%, 337 KB/s], Decompressed: 6889
Downloaded: 6934 file(s) [attempted 6934/8546 = 81%, 183 KB/s], Decompressed: 6926
Downloaded: 6972 file(s) [attempted 6972/8546 = 81%, 992 KB/s], Decompressed: 6963
Downloaded: 7014 file(s) [attempted 7014/8546 = 82%, 276 KB/s], Decompressed: 6994
Downloaded: 7055 file(s) [attempted 7055/8546 = 82%, 409 KB/s], Decompressed: 7051
Downloaded: 7095 file(s) [attempted 7095/8546 = 83%, 204 KB/s], Decompressed: 7092
Downloaded: 7136 file(s) [attempted 7136/8546 = 83%, 168 KB/s], Decompressed: 7126
Downloaded: 7176 file(s) [attempted 7176/8546 = 83%, 1036 KB/s], Decompressed: 7170
Downloaded: 7217 file(s) [attempted 7217/8546 = 84%, 102 KB/s], Decompressed: 7214
Downloaded: 7254 file(s) [attempted 7254/8546 = 84%, 1657 KB/s], Decompressed: 7251
Downloaded: 7298 file(s) [attempted 7298/8546 = 85%, 157 KB/s], Decompressed: 7295
Downloaded: 7335 file(s) [attempted 7335/8546 = 85%, 37 KB/s], Decompressed: 7333
Downloaded: 7373 file(s) [attempted 7373/8546 = 86%, 33 KB/s], Decompressed: 7369
Downloaded: 7413 file(s) [attempted 7413/8546 = 86%, 374 KB/s], Decompressed: 7410
Downloaded: 7450 file(s) [attempted 7450/8546 = 87%, 69 KB/s], Decompressed: 7447
Downloaded: 7493 file(s) [attempted 7493/8546 = 87%, 171 KB/s], Decompressed: 7481
Downloaded: 7528 file(s) [attempted 7528/8546 = 88%, 217 KB/s], Decompressed: 7525
Downloaded: 7569 file(s) [attempted 7569/8546 = 88%, 167 KB/s], Decompressed: 7562
Downloaded: 7609 file(s) [attempted 7609/8546 = 89%, 67 KB/s], Decompressed: 7603
Downloaded: 7653 file(s) [attempted 7653/8546 = 89%, 439 KB/s], Decompressed: 7650
Downloaded: 7694 file(s) [attempted 7694/8546 = 90%, 45 KB/s], Decompressed: 7680
Downloaded: 7734 file(s) [attempted 7734/8546 = 90%, 243 KB/s], Decompressed: 7728
Downloaded: 7772 file(s) [attempted 7772/8546 = 90%, 23 KB/s], Decompressed: 7768
Downloaded: 7812 file(s) [attempted 7812/8546 = 91%, 79 KB/s], Decompressed: 7809
Downloaded: 7856 file(s) [attempted 7856/8546 = 91%, 340 KB/s], Decompressed: 7853
Downloaded: 7900 file(s) [attempted 7900/8546 = 92%, 22 KB/s], Decompressed: 7897
Downloaded: 7938 file(s) [attempted 7938/8546 = 92%, 309 KB/s], Decompressed: 7931
Downloaded: 7975 file(s) [attempted 7975/8546 = 93%, 1124 KB/s], Decompressed: 7968
Downloaded: 8015 file(s) [attempted 8015/8546 = 93%, 230 KB/s], Decompressed: 8012
Downloaded: 8056 file(s) [attempted 8056/8546 = 94%, 1974 KB/s], Decompressed: 8052
Downloaded: 8100 file(s) [attempted 8100/8546 = 94%, 145 KB/s], Decompressed: 8093
Downloaded: 8140 file(s) [attempted 8140/8546 = 95%, 112 KB/s], Decompressed: 8134
Downloaded: 8176 file(s) [attempted 8176/8546 = 95%, 53 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8546 = 96%, 252 KB/s], Decompressed: 8205
Downloaded: 8255 file(s) [attempted 8255/8546 = 96%, 817 KB/s], Decompressed: 8249
Downloaded: 8299 file(s) [attempted 8299/8546 = 97%, 423 KB/s], Decompressed: 8296
Downloaded: 8343 file(s) [attempted 8343/8546 = 97%, 1154 KB/s], Decompressed: 8337
Downloaded: 8378 file(s) [attempted 8378/8546 = 98%, 564 KB/s], Decompressed: 8374
Downloaded: 8422 file(s) [attempted 8422/8546 = 98%, 86 KB/s], Decompressed: 8414
Downloaded: 8458 file(s) [attempted 8458/8546 = 98%, 463 KB/s], Decompressed: 8455
Downloaded: 8499 file(s) [attempted 8499/8546 = 99%, 209 KB/s], Decompressed: 8496
Downloaded: 8536 file(s) [attempted 8536/8546 = 99%, 217 KB/s], Decompressed: 8529
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 217 KB/s], Decompressed: 8543


$ lake build
exit_code=Some(0) duration_ms=36576
stdout:
ℹ [3627/3638] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3649/3666] 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/3905] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3960/3976] 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`
⚠ [3964/3976] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3972/3990] 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`
⚠ [4107/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`
⚠ [4109/4151] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4111/4151] 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`
⚠ [4113/4151] 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`
⚠ [4154/4170] 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`
⚠ [4159/4170] 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`
⚠ [4160/4170] 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`
ℹ [4167/4170] 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/4204] 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/4226] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4201/4226] 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`
⚠ [4232/4280] 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`
⚠ [4247/4288] 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`
⚠ [4248/4288] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4263/4288] 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`
⚠ [4286/4288] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:465:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1319:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1406:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2719:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3351:8: declaration uses `sorry`
Build completed successfully (4288 jobs).

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


$ lake build :blueprint
exit_code=Some(0) duration_ms=38377
stdout:
✔ [27/35] Built Cli.Basic:c.o (4.4s)
✔ [30/35] Built Cli.Extensions:c.o (486ms)
✔ [33/44] Built Cli:c.o (71ms)
ℹ [3683/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3709/3731] 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/3867] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3970/3983] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4045/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4053/4078] 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`
⚠ [4057/4078] 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`
⚠ [4201/4221] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4204/4221] 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`
⚠ [4206/4221] 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`
⚠ [4213/4290] 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`
⚠ [4269/4295] 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`
⚠ [4276/4295] 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`
⚠ [4288/4309] 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`
ℹ [4297/4309] 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/4309] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4348/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4350/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/4488] 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/4501] 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`
⚠ [4440/4501] 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`
⚠ [4449/4501] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4495/4502] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:465:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1319:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1406:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2719:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3351:8: declaration uses `sorry`
ℹ [4500/4502] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4502 jobs).

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

Stored Lean workspace build cache
Validated merged Lean semantic artifact receipt: 159229615 bytes, 17033 declarations, 162802 dependencies, 143745 edges, helper checksum af5c2c131b58bf01133340909c6171a1d43fe3637744e20d11490115e108d7d3

Command runs

git_clone exit 0 duration 957 ms · created 7/12/2026, 1:22:47 AM

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

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

git_checkout exit 0 duration 41 ms · created 7/12/2026, 1:22:47 AM

git checkout 6739793850d3eaa031e3543ed72d7f026f8080f5

Note: switching to '6739793850d3eaa031e3543ed72d7f026f8080f5'.

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 6739793 feat(FKS2): Corollary 23 — all 9 Table-6 rows (#722) (#1629)

lake_cache exit 0 duration 1m 14s · created 7/12/2026, 1:22:47 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%, 10 KB/s], Decompressed: 0
Downloaded: 18 file(s) [attempted 18/8546 = 0%, 11 KB/s], Decompressed: 17
Downloaded: 41 file(s) [attempted 41/8546 = 0%, 270 KB/s], Decompressed: 40
Downloaded: 66 file(s) [attempted 66/8546 = 0%, 202 KB/s], Decompressed: 60
Downloaded: 84 file(s) [attempted 84/8546 = 0%, 163 KB/s], Decompressed: 78
Downloaded: 119 file(s) [attempted 119/8546 = 1%, 253 KB/s], Decompressed: 116
Downloaded: 156 file(s) [attempted 156/8546 = 1%, 616 KB/s], Decompressed: 150
Downloaded: 194 file(s) [attempted 194/8546 = 2%, 184 KB/s], Decompressed: 190
Downloaded: 224 file(s) [attempted 224/8546 = 2%, 214 KB/s], Decompressed: 221
Downloaded: 258 file(s) [attempted 258/8546 = 3%, 795 KB/s], Decompressed: 241
Downloaded: 292 file(s) [attempted 292/8546 = 3%, 65 KB/s], Decompressed: 288
Downloaded: 332 file(s) [attempted 332/8546 = 3%, 307 KB/s], Decompressed: 329
Downloaded: 370 file(s) [attempted 370/8546 = 4%, 191 KB/s], Decompressed: 366
Downloaded: 410 file(s) [attempted 410/8546 = 4%, 182 KB/s], Decompressed: 407
Downloaded: 448 file(s) [attempted 448/8546 = 5%, 257 KB/s], Decompressed: 444
Downloaded: 481 file(s) [attempted 481/8546 = 5%, 676 KB/s], Decompressed: 478
Downloaded: 525 file(s) [attempted 525/8546 = 6%, 762 KB/s], Decompressed: 519
Downloaded: 566 file(s) [attempted 566/8546 = 6%, 569 KB/s], Decompressed: 563
Downloaded: 607 file(s) [attempted 607/8546 = 7%, 351 KB/s], Decompressed: 603
Downloaded: 647 file(s) [attempted 647/8546 = 7%, 92 KB/s], Decompressed: 637
Downloaded: 685 file(s) [attempted 685/8546 = 8%, 152 KB/s], Decompressed: 674
Downloaded: 729 file(s) [attempted 729/8546 = 8%, 419 KB/s], Decompressed: 722
Downloaded: 769 file(s) [attempted 769/8546 = 8%, 765 KB/s], Decompressed: 762
Downloaded: 806 file(s) [attempted 806/8546 = 9%, 289 KB/s], Decompressed: 800
Downloaded: 847 file(s) [attempted 847/8546 = 9%, 505 KB/s], Decompressed: 844
Downloaded: 884 file(s) [attempted 884/8546 = 10%, 370 KB/s], Decompressed: 878
Downloaded: 926 file(s) [attempted 926/8546 = 10%, 203 KB/s], Decompressed: 922
Downloaded: 966 file(s) [attempted 966/8546 = 11%, 409 KB/s], Decompressed: 962
Downloaded: 1008 file(s) [attempted 1008/8546 = 11%, 210 KB/s], Decompressed: 999
Downloaded: 1043 file(s) [attempted 1043/8546 = 12%, 636 KB/s], Decompressed: 1038
Downloaded: 1081 file(s) [attempted 1081/8546 = 12%, 231 KB/s], Decompressed: 1077
Downloaded: 1121 file(s) [attempted 1121/8546 = 13%, 362 KB/s], Decompressed: 1118
Downloaded: 1165 file(s) [attempted 1165/8546 = 13%, 108 KB/s], Decompressed: 1164
Downloaded: 1206 file(s) [attempted 1206/8546 = 14%, 531 KB/s], Decompressed: 1202
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 407 KB/s], Decompressed: 1240
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 57 KB/s], Decompressed: 1273
Downloaded: 1323 file(s) [attempted 1323/8546 = 15%, 452 KB/s], Decompressed: 1317
Downloaded: 1368 file(s) [attempted 1368/8546 = 16%, 218 KB/s], Decompressed: 1365
Downloaded: 1409 file(s) [attempted 1409/8546 = 16%, 106 KB/s], Decompressed: 1405
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 85 KB/s], Decompressed: 1443
Downloaded: 1483 file(s) [attempted 1483/8546 = 17%, 1712 KB/s], Decompressed: 1480
Downloaded: 1525 file(s) [attempted 1525/8546 = 17%, 259 KB/s], Decompressed: 1520
Downloaded: 1571 file(s) [attempted 1571/8546 = 18%, 66 KB/s], Decompressed: 1554
Downloaded: 1615 file(s) [attempted 1615/8546 = 18%, 469 KB/s], Decompressed: 1605
Downloaded: 1649 file(s) [attempted 1649/8546 = 19%, 239 KB/s], Decompressed: 1646
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 1051 KB/s], Decompressed: 1683
Downloaded: 1727 file(s) [attempted 1727/8546 = 20%, 164 KB/s], Decompressed: 1723
Downloaded: 1771 file(s) [attempted 1771/8546 = 20%, 944 KB/s], Decompressed: 1767
Downloaded: 1808 file(s) [attempted 1808/8546 = 21%, 147 KB/s], Decompressed: 1804
Downloaded: 1844 file(s) [attempted 1844/8546 = 21%, 110 KB/s], Decompressed: 1838
Downloaded: 1879 file(s) [attempted 1879/8546 = 21%, 1268 KB/s], Decompressed: 1876
Downloaded: 1923 file(s) [attempted 1923/8546 = 22%, 42 KB/s], Decompressed: 1916
Downloaded: 1963 file(s) [attempted 1963/8546 = 22%, 404 KB/s], Decompressed: 1957
Downloaded: 1997 file(s) [attempted 1997/8546 = 23%, 39 KB/s], Decompressed: 1991
Downloaded: 2038 file(s) [attempted 2038/8546 = 23%, 181 KB/s], Decompressed: 2031
Downloaded: 2075 file(s) [attempted 2075/8546 = 24%, 466 KB/s], Decompressed: 2072
Downloaded: 2119 file(s) [attempted 2119/8546 = 24%, 301 KB/s], Decompressed: 2116
Downloaded: 2157 file(s) [attempted 2157/8546 = 25%, 134 KB/s], Decompressed: 2153
Downloaded: 2190 file(s) [attempted 2190/8546 = 25%, 55 KB/s], Decompressed: 2188
Downloaded: 2237 file(s) [attempted 2237/8546 = 26%, 185 KB/s], Decompressed: 2234
Downloaded: 2282 file(s) [attempted 2282/8546 = 26%, 72 KB/s], Decompressed: 2278
Downloaded: 2325 file(s) [attempted 2325/8546 = 27%, 328 KB/s], Decompressed: 2319
Downloaded: 2363 file(s) [attempted 2363/8546 = 27%, 371 KB/s], Decompressed: 2336
Downloaded: 2403 file(s) [attempted 2403/8546 = 28%, 127 KB/s], Decompressed: 2393
Downloaded: 2437 file(s) [attempted 2437/8546 = 28%, 521 KB/s], Decompressed: 2434
Downloaded: 2482 file(s) [attempted 2482/8546 = 29%, 320 KB/s], Decompressed: 2474
Downloaded: 2524 file(s) [attempted 2524/8546 = 29%, 1438 KB/s], Decompressed: 2515
Downloaded: 2559 file(s) [attempted 2559/8546 = 29%, 580 KB/s], Decompressed: 2549
Downloaded: 2596 file(s) [attempted 2596/8546 = 30%, 165 KB/s], Decompressed: 2593
Downloaded: 2639 file(s) [attempted 2639/8546 = 30%, 106 KB/s], Decompressed: 2633
Downloaded: 2681 file(s) [attempted 2681/8546 = 31%, 60 KB/s], Decompressed: 2677
Downloaded: 2725 file(s) [attempted 2725/8546 = 31%, 935 KB/s], Decompressed: 2704
Downloaded: 2758 file(s) [attempted 2758/8546 = 32%, 124 KB/s], Decompressed: 2752
Downloaded: 2797 file(s) [attempted 2797/8546 = 32%, 250 KB/s], Decompressed: 2792
Downloaded: 2840 file(s) [attempted 2840/8546 = 33%, 556 KB/s], Decompressed: 2829
Downloaded: 2884 file(s) [attempted 2884/8546 = 33%, 247 KB/s], Decompressed: 2880
Downloaded: 2928 file(s) [attempted 2928/8546 = 34%, 962 KB/s], Decompressed: 2917
Downloaded: 2965 file(s) [attempted 2965/8546 = 34%, 1025 KB/s], Decompressed: 2961
Downloaded: 3002 file(s) [attempted 3002/8546 = 35%, 633 KB/s], Decompressed: 2995
Downloaded: 3041 file(s) [attempted 3041/8546 = 35%, 200 KB/s], Decompressed: 3032
Downloaded: 3083 file(s) [attempted 3083/8546 = 36%, 2110 KB/s], Decompressed: 3080
Downloaded: 3121 file(s) [attempted 3121/8546 = 36%, 531 KB/s], Decompressed: 3117
Downloaded: 3163 file(s) [attempted 3163/8546 = 37%, 52 KB/s], Decompressed: 3154
Downloaded: 3205 file(s) [attempted 3205/8546 = 37%, 472 KB/s], Decompressed: 3191
Downloaded: 3246 file(s) [attempted 3246/8546 = 37%, 169 KB/s], Decompressed: 3239
Downloaded: 3286 file(s) [attempted 3286/8546 = 38%, 541 KB/s], Decompressed: 3283
Downloaded: 3333 file(s) [attempted 3333/8546 = 39%, 1210 KB/s], Decompressed: 3330
Downloaded: 3373 file(s) [attempted 3373/8546 = 39%, 54 KB/s], Decompressed: 3367
Downloaded: 3410 file(s) [attempted 3410/8546 = 39%, 1435 KB/s], Decompressed: 3401
Downloaded: 3448 file(s) [attempted 3448/8546 = 40%, 1929 KB/s], Decompressed: 3438
Downloaded: 3489 file(s) [attempted 3489/8546 = 40%, 220 KB/s], Decompressed: 3486
Downloaded: 3536 file(s) [attempted 3536/8546 = 41%, 23 KB/s], Decompressed: 3533
Downloaded: 3584 file(s) [attempted 3584/8546 = 41%, 117 KB/s], Decompressed: 3567
Downloaded: 3623 file(s) [attempted 3623/8546 = 42%, 442 KB/s], Decompressed: 3607
Downloaded: 3659 file(s) [attempted 3659/8546 = 42%, 625 KB/s], Decompressed: 3651
Downloaded: 3695 file(s) [attempted 3695/8546 = 43%, 323 KB/s], Decompressed: 3689
Downloaded: 3739 file(s) [attempted 3739/8546 = 43%, 485 KB/s], Decompressed: 3736
Downloaded: 3787 file(s) [attempted 3787/8546 = 44%, 46 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8546 = 44%, 101 KB/s], Decompressed: 3800
Downloaded: 3852 file(s) [attempted 3852/8546 = 45%, 59 KB/s], Decompressed: 3848
Downloaded: 3898 file(s) [attempted 3898/8546 = 45%, 361 KB/s], Decompressed: 3885
Downloaded: 3942 file(s) [attempted 3942/8546 = 46%, 133 KB/s], Decompressed: 3932
Downloaded: 3980 file(s) [attempted 3980/8546 = 46%, 284 KB/s], Decompressed: 3969
Downloaded: 4017 file(s) [attempted 4017/8546 = 47%, 120 KB/s], Decompressed: 4013
Downloaded: 4061 file(s) [attempted 4061/8546 = 47%, 799 KB/s], Decompressed: 4057
Downloaded: 4105 file(s) [attempted 4105/8546 = 48%, 329 KB/s], Decompressed: 4098
Downloaded: 4142 file(s) [attempted 4142/8546 = 48%, 155 KB/s], Decompressed: 4125
Downloaded: 4180 file(s) [attempted 4180/8546 = 48%, 970 KB/s], Decompressed: 4176
Downloaded: 4220 file(s) [attempted 4220/8546 = 49%, 323 KB/s], Decompressed: 4216
Downloaded: 4264 file(s) [attempted 4264/8546 = 49%, 322 KB/s], Decompressed: 4260
Downloaded: 4304 file(s) [attempted 4304/8546 = 50%, 393 KB/s], Decompressed: 4298
Downloaded: 4338 file(s) [attempted 4338/8546 = 50%, 113 KB/s], Decompressed: 4335
Downloaded: 4379 file(s) [attempted 4379/8546 = 51%, 141 KB/s], Decompressed: 4375
Downloaded: 4423 file(s) [attempted 4423/8546 = 51%, 921 KB/s], Decompressed: 4416
Downloaded: 4463 file(s) [attempted 4463/8546 = 52%, 140 KB/s], Decompressed: 4460
Downloaded: 4507 file(s) [attempted 4507/8546 = 52%, 136 KB/s], Decompressed: 4504
Downloaded: 4541 file(s) [attempted 4541/8546 = 53%, 233 KB/s], Decompressed: 4538
Downloaded: 4582 file(s) [attempted 4582/8546 = 53%, 41 KB/s], Decompressed: 4575
Downloaded: 4622 file(s) [attempted 4622/8546 = 54%, 226 KB/s], Decompressed: 4616
Downloaded: 4666 file(s) [attempted 4666/8546 = 54%, 699 KB/s], Decompressed: 4660
Downloaded: 4706 file(s) [attempted 4706/8546 = 55%, 20 KB/s], Decompressed: 4693
Downloaded: 4737 file(s) [attempted 4737/8546 = 55%, 69 KB/s], Decompressed: 4734
Downloaded: 4778 file(s) [attempted 4778/8546 = 55%, 84 KB/s], Decompressed: 4775
Downloaded: 4825 file(s) [attempted 4825/8546 = 56%, 529 KB/s], Decompressed: 4822
Downloaded: 4869 file(s) [attempted 4869/8546 = 56%, 272 KB/s], Decompressed: 4829
Downloaded: 4910 file(s) [attempted 4910/8546 = 57%, 369 KB/s], Decompressed: 4896
Downloaded: 4944 file(s) [attempted 4944/8546 = 57%, 114 KB/s], Decompressed: 4923
Downloaded: 4984 file(s) [attempted 4984/8546 = 58%, 507 KB/s], Decompressed: 4981
Downloaded: 5028 file(s) [attempted 5028/8546 = 58%, 394 KB/s], Decompressed: 5022
Downloaded: 5072 file(s) [attempted 5072/8546 = 59%, 40 KB/s], Decompressed: 5069
Downloaded: 5116 file(s) [attempted 5116/8546 = 59%, 380 KB/s], Decompressed: 5113
Downloaded: 5160 file(s) [attempted 5160/8546 = 60%, 110 KB/s], Decompressed: 5153
Downloaded: 5191 file(s) [attempted 5191/8546 = 60%, 38 KB/s], Decompressed: 5187
Downloaded: 5238 file(s) [attempted 5238/8546 = 61%, 100 KB/s], Decompressed: 5231
Downloaded: 5279 file(s) [attempted 5279/8546 = 61%, 62 KB/s], Decompressed: 5275
Downloaded: 5323 file(s) [attempted 5323/8546 = 62%, 550 KB/s], Decompressed: 5319
Downloaded: 5364 file(s) [attempted 5364/8546 = 62%, 27 KB/s], Decompressed: 5356
Downloaded: 5397 file(s) [attempted 5397/8546 = 63%, 198 KB/s], Decompressed: 5394
Downloaded: 5441 file(s) [attempted 5441/8546 = 63%, 777 KB/s], Decompressed: 5438
Downloaded: 5482 file(s) [attempted 5482/8546 = 64%, 120 KB/s], Decompressed: 5478
Downloaded: 5522 file(s) [attempted 5522/8546 = 64%, 486 KB/s], Decompressed: 5509
Downloaded: 5569 file(s) [attempted 5569/8546 = 65%, 366 KB/s], Decompressed: 5556
Downloaded: 5603 file(s) [attempted 5603/8546 = 65%, 39 KB/s], Decompressed: 5597
Downloaded: 5644 file(s) [attempted 5644/8546 = 66%, 170 KB/s], Decompressed: 5641
Downloaded: 5681 file(s) [attempted 5681/8546 = 66%, 194 KB/s], Decompressed: 5678
Downloaded: 5725 file(s) [attempted 5725/8546 = 66%, 43 KB/s], Decompressed: 5718
Downloaded: 5766 file(s) [attempted 5766/8546 = 67%, 311 KB/s], Decompressed: 5759
Downloaded: 5804 file(s) [attempted 5804/8546 = 67%, 104 KB/s], Decompressed: 5800
Downloaded: 5847 file(s) [attempted 5847/8546 = 68%, 153 KB/s], Decompressed: 5844
Downloaded: 5888 file(s) [attempted 5888/8546 = 68%, 108 KB/s], Decompressed: 5884
Downloaded: 5931 file(s) [attempted 5931/8546 = 69%, 401 KB/s], Decompressed: 5925
Downloaded: 5969 file(s) [attempted 5969/8546 = 69%, 338 KB/s], Decompressed: 5955
Downloaded: 6006 file(s) [attempted 6006/8546 = 70%, 666 KB/s], Decompressed: 5975
Downloaded: 6047 file(s) [attempted 6047/8546 = 70%, 776 KB/s], Decompressed: 6040
Downloaded: 6090 file(s) [attempted 6090/8546 = 71%, 283 KB/s], Decompressed: 6087
Downloaded: 6134 file(s) [attempted 6134/8546 = 71%, 482 KB/s], Decompressed: 6124
Downloaded: 6167 file(s) [attempted 6167/8546 = 72%, 224 KB/s], Decompressed: 6162
Downloaded: 6209 file(s) [attempted 6209/8546 = 72%, 765 KB/s], Decompressed: 6205
Downloaded: 6253 file(s) [attempted 6253/8546 = 73%, 2517 KB/s], Decompressed: 6246
Downloaded: 6293 file(s) [attempted 6293/8546 = 73%, 57 KB/s], Decompressed: 6283
Downloaded: 6327 file(s) [attempted 6327/8546 = 74%, 94 KB/s], Decompressed: 6321
Downloaded: 6364 file(s) [attempted 6364/8546 = 74%, 2475 KB/s], Decompressed: 6361
Downloaded: 6408 file(s) [attempted 6408/8546 = 74%, 569 KB/s], Decompressed: 6405
Downloaded: 6452 file(s) [attempted 6452/8546 = 75%, 895 KB/s], Decompressed: 6439
Downloaded: 6496 file(s) [attempted 6496/8546 = 76%, 144 KB/s], Decompressed: 6479
Downloaded: 6530 file(s) [attempted 6530/8546 = 76%, 295 KB/s], Decompressed: 6523
Downloaded: 6574 file(s) [attempted 6574/8546 = 76%, 169 KB/s], Decompressed: 6567
Downloaded: 6618 file(s) [attempted 6618/8546 = 77%, 57 KB/s], Decompressed: 6611
Downloaded: 6659 file(s) [attempted 6659/8546 = 77%, 426 KB/s], Decompressed: 6649
Downloaded: 6699 file(s) [attempted 6699/8546 = 78%, 110 KB/s], Decompressed: 6686
Downloaded: 6734 file(s) [attempted 6734/8546 = 78%, 327 KB/s], Decompressed: 6730
Downloaded: 6774 file(s) [attempted 6774/8546 = 79%, 1390 KB/s], Decompressed: 6770
Downloaded: 6818 file(s) [attempted 6818/8546 = 79%, 64 KB/s], Decompressed: 6811
Downloaded: 6855 file(s) [attempted 6855/8546 = 80%, 24 KB/s], Decompressed: 6852
Downloaded: 6896 file(s) [attempted 6896/8546 = 80%, 337 KB/s], Decompressed: 6889
Downloaded: 6934 file(s) [attempted 6934/8546 = 81%, 183 KB/s], Decompressed: 6926
Downloaded: 6972 file(s) [attempted 6972/8546 = 81%, 992 KB/s], Decompressed: 6963
Downloaded: 7014 file(s) [attempted 7014/8546 = 82%, 276 KB/s], Decompressed: 6994
Downloaded: 7055 file(s) [attempted 7055/8546 = 82%, 409 KB/s], Decompressed: 7051
Downloaded: 7095 file(s) [attempted 7095/8546 = 83%, 204 KB/s], Decompressed: 7092
Downloaded: 7136 file(s) [attempted 7136/8546 = 83%, 168 KB/s], Decompressed: 7126
Downloaded: 7176 file(s) [attempted 7176/8546 = 83%, 1036 KB/s], Decompressed: 7170
Downloaded: 7217 file(s) [attempted 7217/8546 = 84%, 102 KB/s], Decompressed: 7214
Downloaded: 7254 file(s) [attempted 7254/8546 = 84%, 1657 KB/s], Decompressed: 7251
Downloaded: 7298 file(s) [attempted 7298/8546 = 85%, 157 KB/s], Decompressed: 7295
Downloaded: 7335 file(s) [attempted 7335/8546 = 85%, 37 KB/s], Decompressed: 7333
Downloaded: 7373 file(s) [attempted 7373/8546 = 86%, 33 KB/s], Decompressed: 7369
Downloaded: 7413 file(s) [attempted 7413/8546 = 86%, 374 KB/s], Decompressed: 7410
Downloaded: 7450 file(s) [attempted 7450/8546 = 87%, 69 KB/s], Decompressed: 7447
Downloaded: 7493 file(s) [attempted 7493/8546 = 87%, 171 KB/s], Decompressed: 7481
Downloaded: 7528 file(s) [attempted 7528/8546 = 88%, 217 KB/s], Decompressed: 7525
Downloaded: 7569 file(s) [attempted 7569/8546 = 88%, 167 KB/s], Decompressed: 7562
Downloaded: 7609 file(s) [attempted 7609/8546 = 89%, 67 KB/s], Decompressed: 7603
Downloaded: 7653 file(s) [attempted 7653/8546 = 89%, 439 KB/s], Decompressed: 7650
Downloaded: 7694 file(s) [attempted 7694/8546 = 90%, 45 KB/s], Decompressed: 7680
Downloaded: 7734 file(s) [attempted 7734/8546 = 90%, 243 KB/s], Decompressed: 7728
Downloaded: 7772 file(s) [attempted 7772/8546 = 90%, 23 KB/s], Decompressed: 7768
Downloaded: 7812 file(s) [attempted 7812/8546 = 91%, 79 KB/s], Decompressed: 7809
Downloaded: 7856 file(s) [attempted 7856/8546 = 91%, 340 KB/s], Decompressed: 7853
Downloaded: 7900 file(s) [attempted 7900/8546 = 92%, 22 KB/s], Decompressed: 7897
Downloaded: 7938 file(s) [attempted 7938/8546 = 92%, 309 KB/s], Decompressed: 7931
Downloaded: 7975 file(s) [attempted 7975/8546 = 93%, 1124 KB/s], Decompressed: 7968
Downloaded: 8015 file(s) [attempted 8015/8546 = 93%, 230 KB/s], Decompressed: 8012
Downloaded: 8056 file(s) [attempted 8056/8546 = 94%, 1974 KB/s], Decompressed: 8052
Downloaded: 8100 file(s) [attempted 8100/8546 = 94%, 145 KB/s], Decompressed: 8093
Downloaded: 8140 file(s) [attempted 8140/8546 = 95%, 112 KB/s], Decompressed: 8134
Downloaded: 8176 file(s) [attempted 8176/8546 = 95%, 53 KB/s], Decompressed: 8167
Downloaded: 8215 file(s) [attempted 8215/8546 = 96%, 252 KB/s], Decompressed: 8205
Downloaded: 8255 file(s) [attempted 8255/8546 = 96%, 817 KB/s], Decompressed: 8249
Downloaded: 8299 file(s) [attempted 8299/8546 = 97%, 423 KB/s], Decompressed: 8296
Downloaded: 8343 file(s) [attempted 8343/8546 = 97%, 1154 KB/s], Decompressed: 8337
Downloaded: 8378 file(s) [attempted 8378/8546 = 98%, 564 KB/s], Decompressed: 8374
Downloaded: 8422 file(s) [attempted 8422/8546 = 98%, 86 KB/s], Decompressed: 8414
Downloaded: 8458 file(s) [attempted 8458/8546 = 98%, 463 KB/s], Decompressed: 8455
Downloaded: 8499 file(s) [attempted 8499/8546 = 99%, 209 KB/s], Decompressed: 8496
Downloaded: 8536 file(s) [attempted 8536/8546 = 99%, 217 KB/s], Decompressed: 8529
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 217 KB/s], Decompressed: 8543

lean_checker exit 0 duration 37s · created 7/12/2026, 1:22:47 AM

lake build

ℹ [3627/3638] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3649/3666] 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/3905] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3960/3976] 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`
⚠ [3964/3976] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3972/3990] 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`
⚠ [4107/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`
⚠ [4109/4151] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4111/4151] 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`
⚠ [4113/4151] 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`
⚠ [4154/4170] 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`
⚠ [4159/4170] 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`
⚠ [4160/4170] 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`
ℹ [4167/4170] 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/4204] 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/4226] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4201/4226] 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`
⚠ [4232/4280] 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`
⚠ [4247/4288] 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`
⚠ [4248/4288] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4263/4288] 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`
⚠ [4286/4288] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:465:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1319:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1406:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2719:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3351:8: declaration uses `sorry`
Build completed successfully (4288 jobs).

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

blueprint_build exit 0 duration 38s · created 7/12/2026, 1:22:47 AM

lake build :blueprint

✔ [27/35] Built Cli.Basic:c.o (4.4s)
✔ [30/35] Built Cli.Extensions:c.o (486ms)
✔ [33/44] Built Cli:c.o (71ms)
ℹ [3683/3699] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3709/3731] 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/3867] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3970/3983] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4045/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4053/4078] 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`
⚠ [4057/4078] 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`
⚠ [4201/4221] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4204/4221] 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`
⚠ [4206/4221] 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`
⚠ [4213/4290] 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`
⚠ [4269/4295] 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`
⚠ [4276/4295] 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`
⚠ [4288/4309] 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`
ℹ [4297/4309] 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/4309] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4348/4360] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4350/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/4488] 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/4501] 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`
⚠ [4440/4501] 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`
⚠ [4449/4501] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4495/4502] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:465:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1319:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1406:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2719:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3351:8: declaration uses `sorry`
ℹ [4500/4502] Replayed PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint
info: Blueprint indexing
Build completed successfully (4502 jobs).

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