Verification run

Run 153

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via manual

succeeded commit 6739793850d3 toolchain lean-v4-31-0 prover lean took 18m 7s · 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-1218-source
exit_code=Some(0) duration_ms=1229
stderr:
Cloning into '/var/lib/apodeixis/repos/job-1218-source'...


$ git checkout 6739793850d3eaa031e3543ed72d7f026f8080f5
exit_code=Some(0) duration_ms=28
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=86101
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%, 11 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8546 = 0%, 10 KB/s], Decompressed: 13
Downloaded: 40 file(s) [attempted 40/8546 = 0%, 23 KB/s], Decompressed: 23
Downloaded: 67 file(s) [attempted 67/8546 = 0%, 98 KB/s], Decompressed: 23
Downloaded: 95 file(s) [attempted 95/8546 = 1%, 26 KB/s], Decompressed: 28
Downloaded: 126 file(s) [attempted 126/8546 = 1%, 51 KB/s], Decompressed: 28
Downloaded: 150 file(s) [attempted 150/8546 = 1%, 127 KB/s], Decompressed: 143
Downloaded: 177 file(s) [attempted 177/8546 = 2%, 153 KB/s], Decompressed: 173
Downloaded: 213 file(s) [attempted 213/8546 = 2%, 356 KB/s], Decompressed: 204
Downloaded: 245 file(s) [attempted 245/8546 = 2%, 127 KB/s], Decompressed: 214
Downloaded: 278 file(s) [attempted 278/8546 = 3%, 335 KB/s], Decompressed: 214
Downloaded: 319 file(s) [attempted 319/8546 = 3%, 720 KB/s], Decompressed: 305
Downloaded: 360 file(s) [attempted 360/8546 = 4%, 207 KB/s], Decompressed: 305
Downloaded: 390 file(s) [attempted 390/8546 = 4%, 60 KB/s], Decompressed: 305
Downloaded: 434 file(s) [attempted 434/8546 = 5%, 933 KB/s], Decompressed: 397
Downloaded: 475 file(s) [attempted 475/8546 = 5%, 90 KB/s], Decompressed: 397
Downloaded: 522 file(s) [attempted 522/8546 = 6%, 634 KB/s], Decompressed: 505
Downloaded: 559 file(s) [attempted 559/8546 = 6%, 598 KB/s], Decompressed: 505
Downloaded: 600 file(s) [attempted 600/8546 = 7%, 194 KB/s], Decompressed: 522
Downloaded: 641 file(s) [attempted 641/8546 = 7%, 807 KB/s], Decompressed: 522
Downloaded: 681 file(s) [attempted 681/8546 = 7%, 154 KB/s], Decompressed: 522
Downloaded: 725 file(s) [attempted 725/8546 = 8%, 178 KB/s], Decompressed: 600
Downloaded: 766 file(s) [attempted 766/8546 = 8%, 168 KB/s], Decompressed: 600
Downloaded: 803 file(s) [attempted 803/8546 = 9%, 144 KB/s], Decompressed: 688
Downloaded: 847 file(s) [attempted 847/8546 = 9%, 180 KB/s], Decompressed: 688
Downloaded: 884 file(s) [attempted 884/8546 = 10%, 1657 KB/s], Decompressed: 871
Downloaded: 928 file(s) [attempted 928/8546 = 10%, 526 KB/s], Decompressed: 922
Downloaded: 969 file(s) [attempted 969/8546 = 11%, 391 KB/s], Decompressed: 955
Downloaded: 1006 file(s) [attempted 1006/8546 = 11%, 203 KB/s], Decompressed: 955
Downloaded: 1045 file(s) [attempted 1045/8546 = 12%, 968 KB/s], Decompressed: 962
Downloaded: 1087 file(s) [attempted 1087/8546 = 12%, 356 KB/s], Decompressed: 962
Downloaded: 1131 file(s) [attempted 1131/8546 = 13%, 402 KB/s], Decompressed: 962
Downloaded: 1169 file(s) [attempted 1169/8546 = 13%, 274 KB/s], Decompressed: 1043
Downloaded: 1202 file(s) [attempted 1202/8546 = 14%, 902 KB/s], Decompressed: 1043
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 83 KB/s], Decompressed: 1141
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 327 KB/s], Decompressed: 1280
Downloaded: 1331 file(s) [attempted 1331/8546 = 15%, 77 KB/s], Decompressed: 1328
Downloaded: 1372 file(s) [attempted 1372/8546 = 16%, 148 KB/s], Decompressed: 1355
Downloaded: 1412 file(s) [attempted 1412/8546 = 16%, 112 KB/s], Decompressed: 1355
Downloaded: 1453 file(s) [attempted 1453/8546 = 17%, 62 KB/s], Decompressed: 1361
Downloaded: 1485 file(s) [attempted 1485/8546 = 17%, 360 KB/s], Decompressed: 1476
Downloaded: 1527 file(s) [attempted 1527/8546 = 17%, 146 KB/s], Decompressed: 1476
Downloaded: 1568 file(s) [attempted 1568/8546 = 18%, 106 KB/s], Decompressed: 1476
Downloaded: 1608 file(s) [attempted 1608/8546 = 18%, 22 KB/s], Decompressed: 1483
Downloaded: 1642 file(s) [attempted 1642/8546 = 19%, 199 KB/s], Decompressed: 1483
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 120 KB/s], Decompressed: 1571
Downloaded: 1727 file(s) [attempted 1727/8546 = 20%, 215 KB/s], Decompressed: 1571
Downloaded: 1764 file(s) [attempted 1764/8546 = 20%, 294 KB/s], Decompressed: 1662
Downloaded: 1801 file(s) [attempted 1801/8546 = 21%, 447 KB/s], Decompressed: 1764
Downloaded: 1842 file(s) [attempted 1842/8546 = 21%, 116 KB/s], Decompressed: 1764
Downloaded: 1882 file(s) [attempted 1882/8546 = 22%, 129 KB/s], Decompressed: 1872
Downloaded: 1923 file(s) [attempted 1923/8546 = 22%, 42 KB/s], Decompressed: 1916
Downloaded: 1967 file(s) [attempted 1967/8546 = 23%, 431 KB/s], Decompressed: 1923
Downloaded: 2007 file(s) [attempted 2007/8546 = 23%, 135 KB/s], Decompressed: 1923
Downloaded: 2041 file(s) [attempted 2041/8546 = 23%, 1035 KB/s], Decompressed: 1926
Downloaded: 2082 file(s) [attempted 2082/8546 = 24%, 338 KB/s], Decompressed: 1926
Downloaded: 2119 file(s) [attempted 2119/8546 = 24%, 57 KB/s], Decompressed: 1926
Downloaded: 2166 file(s) [attempted 2166/8546 = 25%, 242 KB/s], Decompressed: 1926
Downloaded: 2214 file(s) [attempted 2214/8546 = 25%, 91 KB/s], Decompressed: 1926
Downloaded: 2251 file(s) [attempted 2251/8546 = 26%, 567 KB/s], Decompressed: 1926
Downloaded: 2288 file(s) [attempted 2288/8546 = 26%, 609 KB/s], Decompressed: 2014
Downloaded: 2325 file(s) [attempted 2325/8546 = 27%, 329 KB/s], Decompressed: 2014
Downloaded: 2366 file(s) [attempted 2366/8546 = 27%, 336 KB/s], Decompressed: 2268
Downloaded: 2413 file(s) [attempted 2413/8546 = 28%, 636 KB/s], Decompressed: 2268
Downloaded: 2461 file(s) [attempted 2461/8546 = 28%, 403 KB/s], Decompressed: 2363
Downloaded: 2502 file(s) [attempted 2502/8546 = 29%, 984 KB/s], Decompressed: 2495
Downloaded: 2545 file(s) [attempted 2545/8546 = 29%, 83 KB/s], Decompressed: 2539
Downloaded: 2589 file(s) [attempted 2589/8546 = 30%, 365 KB/s], Decompressed: 2552
Downloaded: 2627 file(s) [attempted 2627/8546 = 30%, 22 KB/s], Decompressed: 2559
Downloaded: 2670 file(s) [attempted 2670/8546 = 31%, 608 KB/s], Decompressed: 2559
Downloaded: 2711 file(s) [attempted 2711/8546 = 31%, 45 KB/s], Decompressed: 2620
Downloaded: 2755 file(s) [attempted 2755/8546 = 32%, 68 KB/s], Decompressed: 2620
Downloaded: 2792 file(s) [attempted 2792/8546 = 32%, 1355 KB/s], Decompressed: 2620
Downloaded: 2829 file(s) [attempted 2829/8546 = 33%, 67 KB/s], Decompressed: 2809
Downloaded: 2870 file(s) [attempted 2870/8546 = 33%, 73 KB/s], Decompressed: 2826
Downloaded: 2914 file(s) [attempted 2914/8546 = 34%, 144 KB/s], Decompressed: 2826
Downloaded: 2955 file(s) [attempted 2955/8546 = 34%, 377 KB/s], Decompressed: 2948
Downloaded: 2995 file(s) [attempted 2995/8546 = 35%, 39 KB/s], Decompressed: 2975
Downloaded: 3032 file(s) [attempted 3032/8546 = 35%, 892 KB/s], Decompressed: 2975
Downloaded: 3070 file(s) [attempted 3070/8546 = 35%, 1296 KB/s], Decompressed: 2978
Downloaded: 3110 file(s) [attempted 3110/8546 = 36%, 242 KB/s], Decompressed: 2978
Downloaded: 3154 file(s) [attempted 3154/8546 = 36%, 33 KB/s], Decompressed: 2978
Downloaded: 3195 file(s) [attempted 3195/8546 = 37%, 71 KB/s], Decompressed: 2978
Downloaded: 3239 file(s) [attempted 3239/8546 = 37%, 170 KB/s], Decompressed: 2978
Downloaded: 3273 file(s) [attempted 3273/8546 = 38%, 113 KB/s], Decompressed: 2978
Downloaded: 3313 file(s) [attempted 3313/8546 = 38%, 877 KB/s], Decompressed: 3063
Downloaded: 3355 file(s) [attempted 3355/8546 = 39%, 204 KB/s], Decompressed: 3063
Downloaded: 3391 file(s) [attempted 3391/8546 = 39%, 121 KB/s], Decompressed: 3063
Downloaded: 3435 file(s) [attempted 3435/8546 = 40%, 198 KB/s], Decompressed: 3313
Downloaded: 3479 file(s) [attempted 3479/8546 = 40%, 344 KB/s], Decompressed: 3313
Downloaded: 3520 file(s) [attempted 3520/8546 = 41%, 1903 KB/s], Decompressed: 3425
Downloaded: 3564 file(s) [attempted 3564/8546 = 41%, 73 KB/s], Decompressed: 3425
Downloaded: 3601 file(s) [attempted 3601/8546 = 42%, 53 KB/s], Decompressed: 3425
Downloaded: 3635 file(s) [attempted 3635/8546 = 42%, 112 KB/s], Decompressed: 3516
Downloaded: 3675 file(s) [attempted 3675/8546 = 43%, 338 KB/s], Decompressed: 3665
Downloaded: 3719 file(s) [attempted 3719/8546 = 43%, 51 KB/s], Decompressed: 3712
Downloaded: 3763 file(s) [attempted 3763/8546 = 44%, 286 KB/s], Decompressed: 3712
Downloaded: 3807 file(s) [attempted 3807/8546 = 44%, 307 KB/s], Decompressed: 3712
Downloaded: 3844 file(s) [attempted 3844/8546 = 44%, 104 KB/s], Decompressed: 3824
Downloaded: 3878 file(s) [attempted 3878/8546 = 45%, 744 KB/s], Decompressed: 3824
Downloaded: 3915 file(s) [attempted 3915/8546 = 45%, 218 KB/s], Decompressed: 3831
Downloaded: 3959 file(s) [attempted 3959/8546 = 46%, 80 KB/s], Decompressed: 3831
Downloaded: 4000 file(s) [attempted 4000/8546 = 46%, 125 KB/s], Decompressed: 3831
Downloaded: 4037 file(s) [attempted 4037/8546 = 47%, 48 KB/s], Decompressed: 3831
Downloaded: 4068 file(s) [attempted 4068/8546 = 47%, 960 KB/s], Decompressed: 3831
Downloaded: 4108 file(s) [attempted 4108/8546 = 48%, 274 KB/s], Decompressed: 3831
Downloaded: 4152 file(s) [attempted 4152/8546 = 48%, 36 KB/s], Decompressed: 3831
Downloaded: 4200 file(s) [attempted 4200/8546 = 49%, 174 KB/s], Decompressed: 3912
Downloaded: 4240 file(s) [attempted 4240/8546 = 49%, 1427 KB/s], Decompressed: 3912
Downloaded: 4274 file(s) [attempted 4274/8546 = 50%, 865 KB/s], Decompressed: 3912
Downloaded: 4311 file(s) [attempted 4311/8546 = 50%, 223 KB/s], Decompressed: 4159
Downloaded: 4355 file(s) [attempted 4355/8546 = 50%, 65 KB/s], Decompressed: 4159
Downloaded: 4402 file(s) [attempted 4402/8546 = 51%, 97 KB/s], Decompressed: 4159
Downloaded: 4453 file(s) [attempted 4453/8546 = 52%, 550 KB/s], Decompressed: 4291
Downloaded: 4501 file(s) [attempted 4501/8546 = 52%, 96 KB/s], Decompressed: 4291
Downloaded: 4548 file(s) [attempted 4548/8546 = 53%, 173 KB/s], Decompressed: 4291
Downloaded: 4585 file(s) [attempted 4585/8546 = 53%, 141 KB/s], Decompressed: 4446
Downloaded: 4622 file(s) [attempted 4622/8546 = 54%, 486 KB/s], Decompressed: 4446
Downloaded: 4656 file(s) [attempted 4656/8546 = 54%, 765 KB/s], Decompressed: 4446
Downloaded: 4693 file(s) [attempted 4693/8546 = 54%, 35 KB/s], Decompressed: 4446
Downloaded: 4734 file(s) [attempted 4734/8546 = 55%, 45 KB/s], Decompressed: 4551
Downloaded: 4771 file(s) [attempted 4771/8546 = 55%, 38 KB/s], Decompressed: 4551
Downloaded: 4812 file(s) [attempted 4812/8546 = 56%, 469 KB/s], Decompressed: 4714
Downloaded: 4856 file(s) [attempted 4856/8546 = 56%, 123 KB/s], Decompressed: 4852
Downloaded: 4896 file(s) [attempted 4896/8546 = 57%, 455 KB/s], Decompressed: 4863
Downloaded: 4930 file(s) [attempted 4930/8546 = 57%, 118 KB/s], Decompressed: 4863
Downloaded: 4967 file(s) [attempted 4967/8546 = 58%, 50 KB/s], Decompressed: 4869
Downloaded: 5011 file(s) [attempted 5011/8546 = 58%, 512 KB/s], Decompressed: 4957
Downloaded: 5055 file(s) [attempted 5055/8546 = 59%, 697 KB/s], Decompressed: 4957
Downloaded: 5096 file(s) [attempted 5096/8546 = 59%, 448 KB/s], Decompressed: 4974
Downloaded: 5133 file(s) [attempted 5133/8546 = 60%, 110 KB/s], Decompressed: 4974
Downloaded: 5174 file(s) [attempted 5174/8546 = 60%, 336 KB/s], Decompressed: 5059
Downloaded: 5211 file(s) [attempted 5211/8546 = 60%, 673 KB/s], Decompressed: 5059
Downloaded: 5241 file(s) [attempted 5241/8546 = 61%, 967 KB/s], Decompressed: 5153
Downloaded: 5289 file(s) [attempted 5289/8546 = 61%, 960 KB/s], Decompressed: 5282
Downloaded: 5329 file(s) [attempted 5329/8546 = 62%, 138 KB/s], Decompressed: 5326
Downloaded: 5360 file(s) [attempted 5360/8546 = 62%, 686 KB/s], Decompressed: 5356
Downloaded: 5404 file(s) [attempted 5404/8546 = 63%, 28 KB/s], Decompressed: 5390
Downloaded: 5441 file(s) [attempted 5441/8546 = 63%, 483 KB/s], Decompressed: 5434
Downloaded: 5482 file(s) [attempted 5482/8546 = 64%, 637 KB/s], Decompressed: 5478
Downloaded: 5521 file(s) [attempted 5521/8546 = 64%, 65 KB/s], Decompressed: 5515
Downloaded: 5556 file(s) [attempted 5556/8546 = 65%, 1297 KB/s], Decompressed: 5522
Downloaded: 5586 file(s) [attempted 5586/8546 = 65%, 168 KB/s], Decompressed: 5522
Downloaded: 5627 file(s) [attempted 5627/8546 = 65%, 116 KB/s], Decompressed: 5624
Downloaded: 5671 file(s) [attempted 5671/8546 = 66%, 863 KB/s], Decompressed: 5661
Downloaded: 5712 file(s) [attempted 5712/8546 = 66%, 1351 KB/s], Decompressed: 5661
Downloaded: 5752 file(s) [attempted 5752/8546 = 67%, 573 KB/s], Decompressed: 5664
Downloaded: 5789 file(s) [attempted 5789/8546 = 67%, 496 KB/s], Decompressed: 5664
Downloaded: 5833 file(s) [attempted 5833/8546 = 68%, 115 KB/s], Decompressed: 5664
Downloaded: 5871 file(s) [attempted 5871/8546 = 68%, 684 KB/s], Decompressed: 5752
Downloaded: 5911 file(s) [attempted 5911/8546 = 69%, 903 KB/s], Decompressed: 5752
Downloaded: 5952 file(s) [attempted 5952/8546 = 69%, 50 KB/s], Decompressed: 5840
Downloaded: 5989 file(s) [attempted 5989/8546 = 70%, 62 KB/s], Decompressed: 5945
Downloaded: 6033 file(s) [attempted 6033/8546 = 70%, 378 KB/s], Decompressed: 5945
Downloaded: 6077 file(s) [attempted 6077/8546 = 71%, 1140 KB/s], Decompressed: 5965
Downloaded: 6124 file(s) [attempted 6124/8546 = 71%, 226 KB/s], Decompressed: 5965
Downloaded: 6172 file(s) [attempted 6172/8546 = 72%, 27 KB/s], Decompressed: 6047
Downloaded: 6216 file(s) [attempted 6216/8546 = 72%, 1047 KB/s], Decompressed: 6047
Downloaded: 6246 file(s) [attempted 6246/8546 = 73%, 43 KB/s], Decompressed: 6145
Downloaded: 6283 file(s) [attempted 6283/8546 = 73%, 292 KB/s], Decompressed: 6145
Downloaded: 6327 file(s) [attempted 6327/8546 = 74%, 84 KB/s], Decompressed: 6234
Downloaded: 6369 file(s) [attempted 6369/8546 = 74%, 141 KB/s], Decompressed: 6361
Downloaded: 6408 file(s) [attempted 6408/8546 = 74%, 524 KB/s], Decompressed: 6405
Downloaded: 6449 file(s) [attempted 6449/8546 = 75%, 140 KB/s], Decompressed: 6443
Downloaded: 6486 file(s) [attempted 6486/8546 = 75%, 41 KB/s], Decompressed: 6483
Downloaded: 6527 file(s) [attempted 6527/8546 = 76%, 964 KB/s], Decompressed: 6520
Downloaded: 6567 file(s) [attempted 6567/8546 = 76%, 1261 KB/s], Decompressed: 6564
Downloaded: 6611 file(s) [attempted 6611/8546 = 77%, 384 KB/s], Decompressed: 6601
Downloaded: 6645 file(s) [attempted 6645/8546 = 77%, 471 KB/s], Decompressed: 6639
Downloaded: 6686 file(s) [attempted 6686/8546 = 78%, 297 KB/s], Decompressed: 6682
Downloaded: 6726 file(s) [attempted 6726/8546 = 78%, 227 KB/s], Decompressed: 6720
Downloaded: 6770 file(s) [attempted 6770/8546 = 79%, 1447 KB/s], Decompressed: 6767
Downloaded: 6806 file(s) [attempted 6806/8546 = 79%, 69 KB/s], Decompressed: 6798
Downloaded: 6848 file(s) [attempted 6848/8546 = 80%, 59 KB/s], Decompressed: 6825
Downloaded: 6889 file(s) [attempted 6889/8546 = 80%, 43 KB/s], Decompressed: 6825
Downloaded: 6933 file(s) [attempted 6933/8546 = 81%, 101 KB/s], Decompressed: 6831
Downloaded: 6973 file(s) [attempted 6973/8546 = 81%, 126 KB/s], Decompressed: 6831
Downloaded: 7017 file(s) [attempted 7017/8546 = 82%, 246 KB/s], Decompressed: 6913
Downloaded: 7055 file(s) [attempted 7055/8546 = 82%, 606 KB/s], Decompressed: 7051
Downloaded: 7095 file(s) [attempted 7095/8546 = 83%, 118 KB/s], Decompressed: 7065
Downloaded: 7132 file(s) [attempted 7132/8546 = 83%, 1328 KB/s], Decompressed: 7065
Downloaded: 7173 file(s) [attempted 7173/8546 = 83%, 95 KB/s], Decompressed: 7156
Downloaded: 7214 file(s) [attempted 7214/8546 = 84%, 1690 KB/s], Decompressed: 7190
Downloaded: 7254 file(s) [attempted 7254/8546 = 84%, 1024 KB/s], Decompressed: 7190
Downloaded: 7288 file(s) [attempted 7288/8546 = 85%, 329 KB/s], Decompressed: 7195
Downloaded: 7332 file(s) [attempted 7332/8546 = 85%, 169 KB/s], Decompressed: 7195
Downloaded: 7376 file(s) [attempted 7376/8546 = 86%, 410 KB/s], Decompressed: 7274
Downloaded: 7418 file(s) [attempted 7418/8546 = 86%, 898 KB/s], Decompressed: 7410
Downloaded: 7454 file(s) [attempted 7454/8546 = 87%, 69 KB/s], Decompressed: 7447
Downloaded: 7488 file(s) [attempted 7488/8546 = 87%, 409 KB/s], Decompressed: 7484
Downloaded: 7535 file(s) [attempted 7535/8546 = 88%, 234 KB/s], Decompressed: 7532
Downloaded: 7576 file(s) [attempted 7576/8546 = 88%, 474 KB/s], Decompressed: 7572
Downloaded: 7620 file(s) [attempted 7620/8546 = 89%, 2380 KB/s], Decompressed: 7603
Downloaded: 7660 file(s) [attempted 7660/8546 = 89%, 1018 KB/s], Decompressed: 7603
Downloaded: 7697 file(s) [attempted 7697/8546 = 90%, 176 KB/s], Decompressed: 7609
Downloaded: 7738 file(s) [attempted 7738/8546 = 90%, 480 KB/s], Decompressed: 7687
Downloaded: 7775 file(s) [attempted 7775/8546 = 90%, 117 KB/s], Decompressed: 7687
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 132 KB/s], Decompressed: 7816
Downloaded: 7860 file(s) [attempted 7860/8546 = 91%, 184 KB/s], Decompressed: 7819
Downloaded: 7897 file(s) [attempted 7897/8546 = 92%, 179 KB/s], Decompressed: 7819
Downloaded: 7934 file(s) [attempted 7934/8546 = 92%, 102 KB/s], Decompressed: 7931
Downloaded: 7978 file(s) [attempted 7978/8546 = 93%, 295 KB/s], Decompressed: 7934
Downloaded: 8023 file(s) [attempted 8023/8546 = 93%, 143 KB/s], Decompressed: 7934
Downloaded: 8059 file(s) [attempted 8059/8546 = 94%, 157 KB/s], Decompressed: 8052
Downloaded: 8093 file(s) [attempted 8093/8546 = 94%, 202 KB/s], Decompressed: 8090
Downloaded: 8134 file(s) [attempted 8134/8546 = 95%, 351 KB/s], Decompressed: 8093
Downloaded: 8178 file(s) [attempted 8178/8546 = 95%, 556 KB/s], Decompressed: 8093
Downloaded: 8211 file(s) [attempted 8211/8546 = 96%, 709 KB/s], Decompressed: 8100
Downloaded: 8255 file(s) [attempted 8255/8546 = 96%, 486 KB/s], Decompressed: 8100
Downloaded: 8303 file(s) [attempted 8303/8546 = 97%, 222 KB/s], Decompressed: 8293
Downloaded: 8343 file(s) [attempted 8343/8546 = 97%, 143 KB/s], Decompressed: 8337
Downloaded: 8377 file(s) [attempted 8377/8546 = 98%, 581 KB/s], Decompressed: 8367
Downloaded: 8421 file(s) [attempted 8421/8546 = 98%, 130 KB/s], Decompressed: 8367
Downloaded: 8462 file(s) [attempted 8462/8546 = 99%, 91 KB/s], Decompressed: 8374
Downloaded: 8502 file(s) [attempted 8502/8546 = 99%, 120 KB/s], Decompressed: 8499
Downloaded: 8536 file(s) [attempted 8536/8546 = 99%, 560 KB/s], Decompressed: 8529
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 560 KB/s], Decompressed: 8536


$ lake build
exit_code=Some(0) duration_ms=110107
stdout:
ℹ [3625/3636] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3647/3656] 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`
⚠ [3779/3797] 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/3977] 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`
⚠ [3962/3977] 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`
⚠ [3965/3977] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4109/4114] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4110/4114] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4111/4114] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4113/4154] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4151/4165] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4157/4165] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
⚠ [4162/4202] 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/4202] 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/4202] 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`
⚠ [4231/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`
⚠ [4241/4280] 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`
⚠ [4251/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=108705
stdout:
✔ [27/35] Built Cli.Basic:c.o (3.3s)
✔ [30/35] Built Cli.Extensions:c.o (518ms)
✔ [33/41] Built Cli:c.o (69ms)
ℹ [3683/3701] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3707/3727] 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`
⚠ [3965/3981] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4048/4069] 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`
⚠ [4049/4069] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4065/4074] 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/4278] 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`
⚠ [4272/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`
⚠ [4285/4302] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
ℹ [4297/4352] 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/4352] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4349/4385] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4351/4385] 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`
⚠ [4396/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`
⚠ [4424/4488] 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`
⚠ [4427/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`
⚠ [4448/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`
⚠ [4496/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: 394230356 bytes, 17033 declarations, 162802 dependencies, 143745 edges, helper checksum 262612bfe6b92f8688136dae327a763801e5c0c1c675fc86e58abdbd1ca9e2b7

Command runs

git_clone exit 0 duration 1s · created 7/11/2026, 10:50:55 PM

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

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

git_checkout exit 0 duration 28 ms · created 7/11/2026, 10:50:55 PM

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 26s · created 7/11/2026, 10:50:55 PM

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%, 11 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8546 = 0%, 10 KB/s], Decompressed: 13
Downloaded: 40 file(s) [attempted 40/8546 = 0%, 23 KB/s], Decompressed: 23
Downloaded: 67 file(s) [attempted 67/8546 = 0%, 98 KB/s], Decompressed: 23
Downloaded: 95 file(s) [attempted 95/8546 = 1%, 26 KB/s], Decompressed: 28
Downloaded: 126 file(s) [attempted 126/8546 = 1%, 51 KB/s], Decompressed: 28
Downloaded: 150 file(s) [attempted 150/8546 = 1%, 127 KB/s], Decompressed: 143
Downloaded: 177 file(s) [attempted 177/8546 = 2%, 153 KB/s], Decompressed: 173
Downloaded: 213 file(s) [attempted 213/8546 = 2%, 356 KB/s], Decompressed: 204
Downloaded: 245 file(s) [attempted 245/8546 = 2%, 127 KB/s], Decompressed: 214
Downloaded: 278 file(s) [attempted 278/8546 = 3%, 335 KB/s], Decompressed: 214
Downloaded: 319 file(s) [attempted 319/8546 = 3%, 720 KB/s], Decompressed: 305
Downloaded: 360 file(s) [attempted 360/8546 = 4%, 207 KB/s], Decompressed: 305
Downloaded: 390 file(s) [attempted 390/8546 = 4%, 60 KB/s], Decompressed: 305
Downloaded: 434 file(s) [attempted 434/8546 = 5%, 933 KB/s], Decompressed: 397
Downloaded: 475 file(s) [attempted 475/8546 = 5%, 90 KB/s], Decompressed: 397
Downloaded: 522 file(s) [attempted 522/8546 = 6%, 634 KB/s], Decompressed: 505
Downloaded: 559 file(s) [attempted 559/8546 = 6%, 598 KB/s], Decompressed: 505
Downloaded: 600 file(s) [attempted 600/8546 = 7%, 194 KB/s], Decompressed: 522
Downloaded: 641 file(s) [attempted 641/8546 = 7%, 807 KB/s], Decompressed: 522
Downloaded: 681 file(s) [attempted 681/8546 = 7%, 154 KB/s], Decompressed: 522
Downloaded: 725 file(s) [attempted 725/8546 = 8%, 178 KB/s], Decompressed: 600
Downloaded: 766 file(s) [attempted 766/8546 = 8%, 168 KB/s], Decompressed: 600
Downloaded: 803 file(s) [attempted 803/8546 = 9%, 144 KB/s], Decompressed: 688
Downloaded: 847 file(s) [attempted 847/8546 = 9%, 180 KB/s], Decompressed: 688
Downloaded: 884 file(s) [attempted 884/8546 = 10%, 1657 KB/s], Decompressed: 871
Downloaded: 928 file(s) [attempted 928/8546 = 10%, 526 KB/s], Decompressed: 922
Downloaded: 969 file(s) [attempted 969/8546 = 11%, 391 KB/s], Decompressed: 955
Downloaded: 1006 file(s) [attempted 1006/8546 = 11%, 203 KB/s], Decompressed: 955
Downloaded: 1045 file(s) [attempted 1045/8546 = 12%, 968 KB/s], Decompressed: 962
Downloaded: 1087 file(s) [attempted 1087/8546 = 12%, 356 KB/s], Decompressed: 962
Downloaded: 1131 file(s) [attempted 1131/8546 = 13%, 402 KB/s], Decompressed: 962
Downloaded: 1169 file(s) [attempted 1169/8546 = 13%, 274 KB/s], Decompressed: 1043
Downloaded: 1202 file(s) [attempted 1202/8546 = 14%, 902 KB/s], Decompressed: 1043
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 83 KB/s], Decompressed: 1141
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 327 KB/s], Decompressed: 1280
Downloaded: 1331 file(s) [attempted 1331/8546 = 15%, 77 KB/s], Decompressed: 1328
Downloaded: 1372 file(s) [attempted 1372/8546 = 16%, 148 KB/s], Decompressed: 1355
Downloaded: 1412 file(s) [attempted 1412/8546 = 16%, 112 KB/s], Decompressed: 1355
Downloaded: 1453 file(s) [attempted 1453/8546 = 17%, 62 KB/s], Decompressed: 1361
Downloaded: 1485 file(s) [attempted 1485/8546 = 17%, 360 KB/s], Decompressed: 1476
Downloaded: 1527 file(s) [attempted 1527/8546 = 17%, 146 KB/s], Decompressed: 1476
Downloaded: 1568 file(s) [attempted 1568/8546 = 18%, 106 KB/s], Decompressed: 1476
Downloaded: 1608 file(s) [attempted 1608/8546 = 18%, 22 KB/s], Decompressed: 1483
Downloaded: 1642 file(s) [attempted 1642/8546 = 19%, 199 KB/s], Decompressed: 1483
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 120 KB/s], Decompressed: 1571
Downloaded: 1727 file(s) [attempted 1727/8546 = 20%, 215 KB/s], Decompressed: 1571
Downloaded: 1764 file(s) [attempted 1764/8546 = 20%, 294 KB/s], Decompressed: 1662
Downloaded: 1801 file(s) [attempted 1801/8546 = 21%, 447 KB/s], Decompressed: 1764
Downloaded: 1842 file(s) [attempted 1842/8546 = 21%, 116 KB/s], Decompressed: 1764
Downloaded: 1882 file(s) [attempted 1882/8546 = 22%, 129 KB/s], Decompressed: 1872
Downloaded: 1923 file(s) [attempted 1923/8546 = 22%, 42 KB/s], Decompressed: 1916
Downloaded: 1967 file(s) [attempted 1967/8546 = 23%, 431 KB/s], Decompressed: 1923
Downloaded: 2007 file(s) [attempted 2007/8546 = 23%, 135 KB/s], Decompressed: 1923
Downloaded: 2041 file(s) [attempted 2041/8546 = 23%, 1035 KB/s], Decompressed: 1926
Downloaded: 2082 file(s) [attempted 2082/8546 = 24%, 338 KB/s], Decompressed: 1926
Downloaded: 2119 file(s) [attempted 2119/8546 = 24%, 57 KB/s], Decompressed: 1926
Downloaded: 2166 file(s) [attempted 2166/8546 = 25%, 242 KB/s], Decompressed: 1926
Downloaded: 2214 file(s) [attempted 2214/8546 = 25%, 91 KB/s], Decompressed: 1926
Downloaded: 2251 file(s) [attempted 2251/8546 = 26%, 567 KB/s], Decompressed: 1926
Downloaded: 2288 file(s) [attempted 2288/8546 = 26%, 609 KB/s], Decompressed: 2014
Downloaded: 2325 file(s) [attempted 2325/8546 = 27%, 329 KB/s], Decompressed: 2014
Downloaded: 2366 file(s) [attempted 2366/8546 = 27%, 336 KB/s], Decompressed: 2268
Downloaded: 2413 file(s) [attempted 2413/8546 = 28%, 636 KB/s], Decompressed: 2268
Downloaded: 2461 file(s) [attempted 2461/8546 = 28%, 403 KB/s], Decompressed: 2363
Downloaded: 2502 file(s) [attempted 2502/8546 = 29%, 984 KB/s], Decompressed: 2495
Downloaded: 2545 file(s) [attempted 2545/8546 = 29%, 83 KB/s], Decompressed: 2539
Downloaded: 2589 file(s) [attempted 2589/8546 = 30%, 365 KB/s], Decompressed: 2552
Downloaded: 2627 file(s) [attempted 2627/8546 = 30%, 22 KB/s], Decompressed: 2559
Downloaded: 2670 file(s) [attempted 2670/8546 = 31%, 608 KB/s], Decompressed: 2559
Downloaded: 2711 file(s) [attempted 2711/8546 = 31%, 45 KB/s], Decompressed: 2620
Downloaded: 2755 file(s) [attempted 2755/8546 = 32%, 68 KB/s], Decompressed: 2620
Downloaded: 2792 file(s) [attempted 2792/8546 = 32%, 1355 KB/s], Decompressed: 2620
Downloaded: 2829 file(s) [attempted 2829/8546 = 33%, 67 KB/s], Decompressed: 2809
Downloaded: 2870 file(s) [attempted 2870/8546 = 33%, 73 KB/s], Decompressed: 2826
Downloaded: 2914 file(s) [attempted 2914/8546 = 34%, 144 KB/s], Decompressed: 2826
Downloaded: 2955 file(s) [attempted 2955/8546 = 34%, 377 KB/s], Decompressed: 2948
Downloaded: 2995 file(s) [attempted 2995/8546 = 35%, 39 KB/s], Decompressed: 2975
Downloaded: 3032 file(s) [attempted 3032/8546 = 35%, 892 KB/s], Decompressed: 2975
Downloaded: 3070 file(s) [attempted 3070/8546 = 35%, 1296 KB/s], Decompressed: 2978
Downloaded: 3110 file(s) [attempted 3110/8546 = 36%, 242 KB/s], Decompressed: 2978
Downloaded: 3154 file(s) [attempted 3154/8546 = 36%, 33 KB/s], Decompressed: 2978
Downloaded: 3195 file(s) [attempted 3195/8546 = 37%, 71 KB/s], Decompressed: 2978
Downloaded: 3239 file(s) [attempted 3239/8546 = 37%, 170 KB/s], Decompressed: 2978
Downloaded: 3273 file(s) [attempted 3273/8546 = 38%, 113 KB/s], Decompressed: 2978
Downloaded: 3313 file(s) [attempted 3313/8546 = 38%, 877 KB/s], Decompressed: 3063
Downloaded: 3355 file(s) [attempted 3355/8546 = 39%, 204 KB/s], Decompressed: 3063
Downloaded: 3391 file(s) [attempted 3391/8546 = 39%, 121 KB/s], Decompressed: 3063
Downloaded: 3435 file(s) [attempted 3435/8546 = 40%, 198 KB/s], Decompressed: 3313
Downloaded: 3479 file(s) [attempted 3479/8546 = 40%, 344 KB/s], Decompressed: 3313
Downloaded: 3520 file(s) [attempted 3520/8546 = 41%, 1903 KB/s], Decompressed: 3425
Downloaded: 3564 file(s) [attempted 3564/8546 = 41%, 73 KB/s], Decompressed: 3425
Downloaded: 3601 file(s) [attempted 3601/8546 = 42%, 53 KB/s], Decompressed: 3425
Downloaded: 3635 file(s) [attempted 3635/8546 = 42%, 112 KB/s], Decompressed: 3516
Downloaded: 3675 file(s) [attempted 3675/8546 = 43%, 338 KB/s], Decompressed: 3665
Downloaded: 3719 file(s) [attempted 3719/8546 = 43%, 51 KB/s], Decompressed: 3712
Downloaded: 3763 file(s) [attempted 3763/8546 = 44%, 286 KB/s], Decompressed: 3712
Downloaded: 3807 file(s) [attempted 3807/8546 = 44%, 307 KB/s], Decompressed: 3712
Downloaded: 3844 file(s) [attempted 3844/8546 = 44%, 104 KB/s], Decompressed: 3824
Downloaded: 3878 file(s) [attempted 3878/8546 = 45%, 744 KB/s], Decompressed: 3824
Downloaded: 3915 file(s) [attempted 3915/8546 = 45%, 218 KB/s], Decompressed: 3831
Downloaded: 3959 file(s) [attempted 3959/8546 = 46%, 80 KB/s], Decompressed: 3831
Downloaded: 4000 file(s) [attempted 4000/8546 = 46%, 125 KB/s], Decompressed: 3831
Downloaded: 4037 file(s) [attempted 4037/8546 = 47%, 48 KB/s], Decompressed: 3831
Downloaded: 4068 file(s) [attempted 4068/8546 = 47%, 960 KB/s], Decompressed: 3831
Downloaded: 4108 file(s) [attempted 4108/8546 = 48%, 274 KB/s], Decompressed: 3831
Downloaded: 4152 file(s) [attempted 4152/8546 = 48%, 36 KB/s], Decompressed: 3831
Downloaded: 4200 file(s) [attempted 4200/8546 = 49%, 174 KB/s], Decompressed: 3912
Downloaded: 4240 file(s) [attempted 4240/8546 = 49%, 1427 KB/s], Decompressed: 3912
Downloaded: 4274 file(s) [attempted 4274/8546 = 50%, 865 KB/s], Decompressed: 3912
Downloaded: 4311 file(s) [attempted 4311/8546 = 50%, 223 KB/s], Decompressed: 4159
Downloaded: 4355 file(s) [attempted 4355/8546 = 50%, 65 KB/s], Decompressed: 4159
Downloaded: 4402 file(s) [attempted 4402/8546 = 51%, 97 KB/s], Decompressed: 4159
Downloaded: 4453 file(s) [attempted 4453/8546 = 52%, 550 KB/s], Decompressed: 4291
Downloaded: 4501 file(s) [attempted 4501/8546 = 52%, 96 KB/s], Decompressed: 4291
Downloaded: 4548 file(s) [attempted 4548/8546 = 53%, 173 KB/s], Decompressed: 4291
Downloaded: 4585 file(s) [attempted 4585/8546 = 53%, 141 KB/s], Decompressed: 4446
Downloaded: 4622 file(s) [attempted 4622/8546 = 54%, 486 KB/s], Decompressed: 4446
Downloaded: 4656 file(s) [attempted 4656/8546 = 54%, 765 KB/s], Decompressed: 4446
Downloaded: 4693 file(s) [attempted 4693/8546 = 54%, 35 KB/s], Decompressed: 4446
Downloaded: 4734 file(s) [attempted 4734/8546 = 55%, 45 KB/s], Decompressed: 4551
Downloaded: 4771 file(s) [attempted 4771/8546 = 55%, 38 KB/s], Decompressed: 4551
Downloaded: 4812 file(s) [attempted 4812/8546 = 56%, 469 KB/s], Decompressed: 4714
Downloaded: 4856 file(s) [attempted 4856/8546 = 56%, 123 KB/s], Decompressed: 4852
Downloaded: 4896 file(s) [attempted 4896/8546 = 57%, 455 KB/s], Decompressed: 4863
Downloaded: 4930 file(s) [attempted 4930/8546 = 57%, 118 KB/s], Decompressed: 4863
Downloaded: 4967 file(s) [attempted 4967/8546 = 58%, 50 KB/s], Decompressed: 4869
Downloaded: 5011 file(s) [attempted 5011/8546 = 58%, 512 KB/s], Decompressed: 4957
Downloaded: 5055 file(s) [attempted 5055/8546 = 59%, 697 KB/s], Decompressed: 4957
Downloaded: 5096 file(s) [attempted 5096/8546 = 59%, 448 KB/s], Decompressed: 4974
Downloaded: 5133 file(s) [attempted 5133/8546 = 60%, 110 KB/s], Decompressed: 4974
Downloaded: 5174 file(s) [attempted 5174/8546 = 60%, 336 KB/s], Decompressed: 5059
Downloaded: 5211 file(s) [attempted 5211/8546 = 60%, 673 KB/s], Decompressed: 5059
Downloaded: 5241 file(s) [attempted 5241/8546 = 61%, 967 KB/s], Decompressed: 5153
Downloaded: 5289 file(s) [attempted 5289/8546 = 61%, 960 KB/s], Decompressed: 5282
Downloaded: 5329 file(s) [attempted 5329/8546 = 62%, 138 KB/s], Decompressed: 5326
Downloaded: 5360 file(s) [attempted 5360/8546 = 62%, 686 KB/s], Decompressed: 5356
Downloaded: 5404 file(s) [attempted 5404/8546 = 63%, 28 KB/s], Decompressed: 5390
Downloaded: 5441 file(s) [attempted 5441/8546 = 63%, 483 KB/s], Decompressed: 5434
Downloaded: 5482 file(s) [attempted 5482/8546 = 64%, 637 KB/s], Decompressed: 5478
Downloaded: 5521 file(s) [attempted 5521/8546 = 64%, 65 KB/s], Decompressed: 5515
Downloaded: 5556 file(s) [attempted 5556/8546 = 65%, 1297 KB/s], Decompressed: 5522
Downloaded: 5586 file(s) [attempted 5586/8546 = 65%, 168 KB/s], Decompressed: 5522
Downloaded: 5627 file(s) [attempted 5627/8546 = 65%, 116 KB/s], Decompressed: 5624
Downloaded: 5671 file(s) [attempted 5671/8546 = 66%, 863 KB/s], Decompressed: 5661
Downloaded: 5712 file(s) [attempted 5712/8546 = 66%, 1351 KB/s], Decompressed: 5661
Downloaded: 5752 file(s) [attempted 5752/8546 = 67%, 573 KB/s], Decompressed: 5664
Downloaded: 5789 file(s) [attempted 5789/8546 = 67%, 496 KB/s], Decompressed: 5664
Downloaded: 5833 file(s) [attempted 5833/8546 = 68%, 115 KB/s], Decompressed: 5664
Downloaded: 5871 file(s) [attempted 5871/8546 = 68%, 684 KB/s], Decompressed: 5752
Downloaded: 5911 file(s) [attempted 5911/8546 = 69%, 903 KB/s], Decompressed: 5752
Downloaded: 5952 file(s) [attempted 5952/8546 = 69%, 50 KB/s], Decompressed: 5840
Downloaded: 5989 file(s) [attempted 5989/8546 = 70%, 62 KB/s], Decompressed: 5945
Downloaded: 6033 file(s) [attempted 6033/8546 = 70%, 378 KB/s], Decompressed: 5945
Downloaded: 6077 file(s) [attempted 6077/8546 = 71%, 1140 KB/s], Decompressed: 5965
Downloaded: 6124 file(s) [attempted 6124/8546 = 71%, 226 KB/s], Decompressed: 5965
Downloaded: 6172 file(s) [attempted 6172/8546 = 72%, 27 KB/s], Decompressed: 6047
Downloaded: 6216 file(s) [attempted 6216/8546 = 72%, 1047 KB/s], Decompressed: 6047
Downloaded: 6246 file(s) [attempted 6246/8546 = 73%, 43 KB/s], Decompressed: 6145
Downloaded: 6283 file(s) [attempted 6283/8546 = 73%, 292 KB/s], Decompressed: 6145
Downloaded: 6327 file(s) [attempted 6327/8546 = 74%, 84 KB/s], Decompressed: 6234
Downloaded: 6369 file(s) [attempted 6369/8546 = 74%, 141 KB/s], Decompressed: 6361
Downloaded: 6408 file(s) [attempted 6408/8546 = 74%, 524 KB/s], Decompressed: 6405
Downloaded: 6449 file(s) [attempted 6449/8546 = 75%, 140 KB/s], Decompressed: 6443
Downloaded: 6486 file(s) [attempted 6486/8546 = 75%, 41 KB/s], Decompressed: 6483
Downloaded: 6527 file(s) [attempted 6527/8546 = 76%, 964 KB/s], Decompressed: 6520
Downloaded: 6567 file(s) [attempted 6567/8546 = 76%, 1261 KB/s], Decompressed: 6564
Downloaded: 6611 file(s) [attempted 6611/8546 = 77%, 384 KB/s], Decompressed: 6601
Downloaded: 6645 file(s) [attempted 6645/8546 = 77%, 471 KB/s], Decompressed: 6639
Downloaded: 6686 file(s) [attempted 6686/8546 = 78%, 297 KB/s], Decompressed: 6682
Downloaded: 6726 file(s) [attempted 6726/8546 = 78%, 227 KB/s], Decompressed: 6720
Downloaded: 6770 file(s) [attempted 6770/8546 = 79%, 1447 KB/s], Decompressed: 6767
Downloaded: 6806 file(s) [attempted 6806/8546 = 79%, 69 KB/s], Decompressed: 6798
Downloaded: 6848 file(s) [attempted 6848/8546 = 80%, 59 KB/s], Decompressed: 6825
Downloaded: 6889 file(s) [attempted 6889/8546 = 80%, 43 KB/s], Decompressed: 6825
Downloaded: 6933 file(s) [attempted 6933/8546 = 81%, 101 KB/s], Decompressed: 6831
Downloaded: 6973 file(s) [attempted 6973/8546 = 81%, 126 KB/s], Decompressed: 6831
Downloaded: 7017 file(s) [attempted 7017/8546 = 82%, 246 KB/s], Decompressed: 6913
Downloaded: 7055 file(s) [attempted 7055/8546 = 82%, 606 KB/s], Decompressed: 7051
Downloaded: 7095 file(s) [attempted 7095/8546 = 83%, 118 KB/s], Decompressed: 7065
Downloaded: 7132 file(s) [attempted 7132/8546 = 83%, 1328 KB/s], Decompressed: 7065
Downloaded: 7173 file(s) [attempted 7173/8546 = 83%, 95 KB/s], Decompressed: 7156
Downloaded: 7214 file(s) [attempted 7214/8546 = 84%, 1690 KB/s], Decompressed: 7190
Downloaded: 7254 file(s) [attempted 7254/8546 = 84%, 1024 KB/s], Decompressed: 7190
Downloaded: 7288 file(s) [attempted 7288/8546 = 85%, 329 KB/s], Decompressed: 7195
Downloaded: 7332 file(s) [attempted 7332/8546 = 85%, 169 KB/s], Decompressed: 7195
Downloaded: 7376 file(s) [attempted 7376/8546 = 86%, 410 KB/s], Decompressed: 7274
Downloaded: 7418 file(s) [attempted 7418/8546 = 86%, 898 KB/s], Decompressed: 7410
Downloaded: 7454 file(s) [attempted 7454/8546 = 87%, 69 KB/s], Decompressed: 7447
Downloaded: 7488 file(s) [attempted 7488/8546 = 87%, 409 KB/s], Decompressed: 7484
Downloaded: 7535 file(s) [attempted 7535/8546 = 88%, 234 KB/s], Decompressed: 7532
Downloaded: 7576 file(s) [attempted 7576/8546 = 88%, 474 KB/s], Decompressed: 7572
Downloaded: 7620 file(s) [attempted 7620/8546 = 89%, 2380 KB/s], Decompressed: 7603
Downloaded: 7660 file(s) [attempted 7660/8546 = 89%, 1018 KB/s], Decompressed: 7603
Downloaded: 7697 file(s) [attempted 7697/8546 = 90%, 176 KB/s], Decompressed: 7609
Downloaded: 7738 file(s) [attempted 7738/8546 = 90%, 480 KB/s], Decompressed: 7687
Downloaded: 7775 file(s) [attempted 7775/8546 = 90%, 117 KB/s], Decompressed: 7687
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 132 KB/s], Decompressed: 7816
Downloaded: 7860 file(s) [attempted 7860/8546 = 91%, 184 KB/s], Decompressed: 7819
Downloaded: 7897 file(s) [attempted 7897/8546 = 92%, 179 KB/s], Decompressed: 7819
Downloaded: 7934 file(s) [attempted 7934/8546 = 92%, 102 KB/s], Decompressed: 7931
Downloaded: 7978 file(s) [attempted 7978/8546 = 93%, 295 KB/s], Decompressed: 7934
Downloaded: 8023 file(s) [attempted 8023/8546 = 93%, 143 KB/s], Decompressed: 7934
Downloaded: 8059 file(s) [attempted 8059/8546 = 94%, 157 KB/s], Decompressed: 8052
Downloaded: 8093 file(s) [attempted 8093/8546 = 94%, 202 KB/s], Decompressed: 8090
Downloaded: 8134 file(s) [attempted 8134/8546 = 95%, 351 KB/s], Decompressed: 8093
Downloaded: 8178 file(s) [attempted 8178/8546 = 95%, 556 KB/s], Decompressed: 8093
Downloaded: 8211 file(s) [attempted 8211/8546 = 96%, 709 KB/s], Decompressed: 8100
Downloaded: 8255 file(s) [attempted 8255/8546 = 96%, 486 KB/s], Decompressed: 8100
Downloaded: 8303 file(s) [attempted 8303/8546 = 97%, 222 KB/s], Decompressed: 8293
Downloaded: 8343 file(s) [attempted 8343/8546 = 97%, 143 KB/s], Decompressed: 8337
Downloaded: 8377 file(s) [attempted 8377/8546 = 98%, 581 KB/s], Decompressed: 8367
Downloaded: 8421 file(s) [attempted 8421/8546 = 98%, 130 KB/s], Decompressed: 8367
Downloaded: 8462 file(s) [attempted 8462/8546 = 99%, 91 KB/s], Decompressed: 8374
Downloaded: 8502 file(s) [attempted 8502/8546 = 99%, 120 KB/s], Decompressed: 8499
Downloaded: 8536 file(s) [attempted 8536/8546 = 99%, 560 KB/s], Decompressed: 8529
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 560 KB/s], Decompressed: 8536

lean_checker exit 0 duration 1m 50s · created 7/11/2026, 10:50:55 PM

lake build

ℹ [3625/3636] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3647/3656] 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`
⚠ [3779/3797] 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/3977] 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`
⚠ [3962/3977] 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`
⚠ [3965/3977] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4109/4114] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4110/4114] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4111/4114] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4113/4154] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4151/4165] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4157/4165] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
⚠ [4162/4202] 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/4202] 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/4202] 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`
⚠ [4231/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`
⚠ [4241/4280] 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`
⚠ [4251/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 1m 49s · created 7/11/2026, 10:50:55 PM

lake build :blueprint

✔ [27/35] Built Cli.Basic:c.o (3.3s)
✔ [30/35] Built Cli.Extensions:c.o (518ms)
✔ [33/41] Built Cli:c.o (69ms)
ℹ [3683/3701] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3707/3727] 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`
⚠ [3965/3981] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4048/4069] 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`
⚠ [4049/4069] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4065/4074] 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/4278] 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`
⚠ [4272/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`
⚠ [4285/4302] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
ℹ [4297/4352] 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/4352] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4349/4385] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4351/4385] 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`
⚠ [4396/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`
⚠ [4424/4488] 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`
⚠ [4427/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`
⚠ [4448/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`
⚠ [4496/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