Verification run

Run 38

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via manual_cache_retry

succeeded commit f94f3366fd0a toolchain lean-v4-30-0 prover lean took 5h 58m · finished 5w ago

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 819 ms · created 6/12/2026, 7:11:19 PM

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

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

git_checkout exit 0 duration 21 ms · created 6/12/2026, 7:11:19 PM

git checkout f94f3366fd0a2291df9bd3247cb19f5f9932ed75

Note: switching to 'f94f3366fd0a2291df9bd3247cb19f5f9932ed75'.

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 f94f336 put in sublemmas for proof of Theorem 3.1 (#1530)

lake_cache exit 0 duration 42s · created 6/12/2026, 7:11:19 PM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache
Decompressed 8459 file(s)
Already decompressed 8459 file(s)

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

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8459 = 0%, 5 KB/s], Decompressed: 13
Downloaded: 39 file(s) [attempted 39/8459 = 0%, 12 KB/s], Decompressed: 38
Downloaded: 69 file(s) [attempted 69/8459 = 0%, 26 KB/s], Decompressed: 67
Downloaded: 100 file(s) [attempted 100/8459 = 1%, 248 KB/s], Decompressed: 96
Downloaded: 127 file(s) [attempted 127/8459 = 1%, 246 KB/s], Decompressed: 124
Downloaded: 162 file(s) [attempted 162/8459 = 1%, 61 KB/s], Decompressed: 158
Downloaded: 199 file(s) [attempted 199/8459 = 2%, 156 KB/s], Decompressed: 196
Downloaded: 240 file(s) [attempted 240/8459 = 2%, 957 KB/s], Decompressed: 237
Downloaded: 282 file(s) [attempted 282/8459 = 3%, 187 KB/s], Decompressed: 281
Downloaded: 321 file(s) [attempted 321/8459 = 3%, 195 KB/s], Decompressed: 316
Downloaded: 357 file(s) [attempted 357/8459 = 4%, 955 KB/s], Decompressed: 353
Downloaded: 396 file(s) [attempted 396/8459 = 4%, 121 KB/s], Decompressed: 391
Downloaded: 439 file(s) [attempted 439/8459 = 5%, 85 KB/s], Decompressed: 436
Downloaded: 485 file(s) [attempted 485/8459 = 5%, 645 KB/s], Decompressed: 480
Downloaded: 525 file(s) [attempted 525/8459 = 6%, 254 KB/s], Decompressed: 521
Downloaded: 562 file(s) [attempted 562/8459 = 6%, 584 KB/s], Decompressed: 559
Downloaded: 603 file(s) [attempted 603/8459 = 7%, 27 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 849 KB/s], Decompressed: 638
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 761 KB/s], Decompressed: 682
Downloaded: 727 file(s) [attempted 727/8459 = 8%, 90 KB/s], Decompressed: 723
Downloaded: 765 file(s) [attempted 765/8459 = 9%, 205 KB/s], Decompressed: 761
Downloaded: 812 file(s) [attempted 812/8459 = 9%, 645 KB/s], Decompressed: 809
Downloaded: 860 file(s) [attempted 860/8459 = 10%, 212 KB/s], Decompressed: 854
Downloaded: 906 file(s) [attempted 906/8459 = 10%, 225 KB/s], Decompressed: 901
Downloaded: 946 file(s) [attempted 946/8459 = 11%, 476 KB/s], Decompressed: 943
Downloaded: 987 file(s) [attempted 987/8459 = 11%, 257 KB/s], Decompressed: 984
Downloaded: 1022 file(s) [attempted 1022/8459 = 12%, 830 KB/s], Decompressed: 1018
Downloaded: 1062 file(s) [attempted 1062/8459 = 12%, 721 KB/s], Decompressed: 1059
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 1807 KB/s], Decompressed: 1100
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 157 KB/s], Decompressed: 1145
Downloaded: 1189 file(s) [attempted 1189/8459 = 14%, 184 KB/s], Decompressed: 1182
Downloaded: 1223 file(s) [attempted 1223/8459 = 14%, 194 KB/s], Decompressed: 1220
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 28 KB/s], Decompressed: 1261
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 668 KB/s], Decompressed: 1305
Downloaded: 1350 file(s) [attempted 1350/8459 = 15%, 54 KB/s], Decompressed: 1346
Downloaded: 1394 file(s) [attempted 1394/8459 = 16%, 767 KB/s], Decompressed: 1388
Downloaded: 1432 file(s) [attempted 1432/8459 = 16%, 915 KB/s], Decompressed: 1422
Downloaded: 1471 file(s) [attempted 1471/8459 = 17%, 111 KB/s], Decompressed: 1466
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 253 KB/s], Decompressed: 1511
Downloaded: 1554 file(s) [attempted 1554/8459 = 18%, 369 KB/s], Decompressed: 1548
Downloaded: 1596 file(s) [attempted 1596/8459 = 18%, 22 KB/s], Decompressed: 1593
Downloaded: 1637 file(s) [attempted 1637/8459 = 19%, 1054 KB/s], Decompressed: 1631
Downloaded: 1675 file(s) [attempted 1675/8459 = 19%, 1060 KB/s], Decompressed: 1668
Downloaded: 1716 file(s) [attempted 1716/8459 = 20%, 166 KB/s], Decompressed: 1709
Downloaded: 1761 file(s) [attempted 1761/8459 = 20%, 72 KB/s], Decompressed: 1757
Downloaded: 1804 file(s) [attempted 1804/8459 = 21%, 202 KB/s], Decompressed: 1798
Downloaded: 1844 file(s) [attempted 1844/8459 = 21%, 225 KB/s], Decompressed: 1839
Downloaded: 1880 file(s) [attempted 1880/8459 = 22%, 252 KB/s], Decompressed: 1874
Downloaded: 1921 file(s) [attempted 1921/8459 = 22%, 375 KB/s], Decompressed: 1915
Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 292 KB/s], Decompressed: 1956
Downloaded: 2004 file(s) [attempted 2004/8459 = 23%, 814 KB/s], Decompressed: 2000
Downloaded: 2048 file(s) [attempted 2048/8459 = 24%, 119 KB/s], Decompressed: 2045
Downloaded: 2082 file(s) [attempted 2082/8459 = 24%, 93 KB/s], Decompressed: 2079
Downloaded: 2123 file(s) [attempted 2123/8459 = 25%, 291 KB/s], Decompressed: 2120
Downloaded: 2161 file(s) [attempted 2161/8459 = 25%, 221 KB/s], Decompressed: 2158
Downloaded: 2202 file(s) [attempted 2202/8459 = 26%, 521 KB/s], Decompressed: 2199
Downloaded: 2247 file(s) [attempted 2247/8459 = 26%, 398 KB/s], Decompressed: 2243
Downloaded: 2288 file(s) [attempted 2288/8459 = 27%, 305 KB/s], Decompressed: 2281
Downloaded: 2324 file(s) [attempted 2324/8459 = 27%, 1095 KB/s], Decompressed: 2318
Downloaded: 2366 file(s) [attempted 2366/8459 = 27%, 103 KB/s], Decompressed: 2363
Downloaded: 2405 file(s) [attempted 2405/8459 = 28%, 130 KB/s], Decompressed: 2401
Downloaded: 2439 file(s) [attempted 2439/8459 = 28%, 400 KB/s], Decompressed: 2435
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 127 KB/s], Decompressed: 2483
Downloaded: 2526 file(s) [attempted 2526/8459 = 29%, 128 KB/s], Decompressed: 2520
Downloaded: 2565 file(s) [attempted 2565/8459 = 30%, 672 KB/s], Decompressed: 2561
Downloaded: 2606 file(s) [attempted 2606/8459 = 30%, 142 KB/s], Decompressed: 2602
Downloaded: 2647 file(s) [attempted 2647/8459 = 31%, 121 KB/s], Decompressed: 2644
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 351 KB/s], Decompressed: 2688
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 157 KB/s], Decompressed: 2726
Downloaded: 2770 file(s) [attempted 2770/8459 = 32%, 65 KB/s], Decompressed: 2767
Downloaded: 2809 file(s) [attempted 2809/8459 = 33%, 554 KB/s], Decompressed: 2801
Downloaded: 2852 file(s) [attempted 2852/8459 = 33%, 208 KB/s], Decompressed: 2849
Downloaded: 2893 file(s) [attempted 2893/8459 = 34%, 866 KB/s], Decompressed: 2887
Downloaded: 2934 file(s) [attempted 2934/8459 = 34%, 826 KB/s], Decompressed: 2928
Downloaded: 2969 file(s) [attempted 2969/8459 = 35%, 175 KB/s], Decompressed: 2962
Downloaded: 3010 file(s) [attempted 3010/8459 = 35%, 665 KB/s], Decompressed: 3006
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 420 KB/s], Decompressed: 3051
Downloaded: 3095 file(s) [attempted 3095/8459 = 36%, 183 KB/s], Decompressed: 3088
Downloaded: 3136 file(s) [attempted 3136/8459 = 37%, 567 KB/s], Decompressed: 3133
Downloaded: 3177 file(s) [attempted 3177/8459 = 37%, 27 KB/s], Decompressed: 3174
Downloaded: 3218 file(s) [attempted 3218/8459 = 38%, 75 KB/s], Decompressed: 3215
Downloaded: 3260 file(s) [attempted 3260/8459 = 38%, 141 KB/s], Decompressed: 3256
Downloaded: 3297 file(s) [attempted 3297/8459 = 38%, 172 KB/s], Decompressed: 3290
Downloaded: 3342 file(s) [attempted 3342/8459 = 39%, 478 KB/s], Decompressed: 3338
Downloaded: 3379 file(s) [attempted 3379/8459 = 39%, 49 KB/s], Decompressed: 3376
Downloaded: 3420 file(s) [attempted 3420/8459 = 40%, 593 KB/s], Decompressed: 3417
Downloaded: 3463 file(s) [attempted 3463/8459 = 40%, 184 KB/s], Decompressed: 3458
Downloaded: 3505 file(s) [attempted 3505/8459 = 41%, 83 KB/s], Decompressed: 3499
Downloaded: 3542 file(s) [attempted 3542/8459 = 41%, 127 KB/s], Decompressed: 3533
Downloaded: 3581 file(s) [attempted 3581/8459 = 42%, 157 KB/s], Decompressed: 3574
Downloaded: 3622 file(s) [attempted 3622/8459 = 42%, 753 KB/s], Decompressed: 3615
Downloaded: 3664 file(s) [attempted 3664/8459 = 43%, 351 KB/s], Decompressed: 3660
Downloaded: 3701 file(s) [attempted 3701/8459 = 43%, 454 KB/s], Decompressed: 3698
Downloaded: 3742 file(s) [attempted 3742/8459 = 44%, 374 KB/s], Decompressed: 3739
Downloaded: 3784 file(s) [attempted 3784/8459 = 44%, 381 KB/s], Decompressed: 3780
Downloaded: 3824 file(s) [attempted 3824/8459 = 45%, 129 KB/s], Decompressed: 3821
Downloaded: 3865 file(s) [attempted 3865/8459 = 45%, 1228 KB/s], Decompressed: 3862
Downloaded: 3906 file(s) [attempted 3906/8459 = 46%, 390 KB/s], Decompressed: 3903
Downloaded: 3947 file(s) [attempted 3947/8459 = 46%, 267 KB/s], Decompressed: 3944
Downloaded: 3986 file(s) [attempted 3986/8459 = 47%, 27 KB/s], Decompressed: 3982
Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 1412 KB/s], Decompressed: 4023
Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 613 KB/s], Decompressed: 4060
Downloaded: 4105 file(s) [attempted 4105/8459 = 48%, 107 KB/s], Decompressed: 4098
Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 106 KB/s], Decompressed: 4146
Downloaded: 4191 file(s) [attempted 4191/8459 = 49%, 972 KB/s], Decompressed: 4187
Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 553 KB/s], Decompressed: 4228
Downloaded: 4269 file(s) [attempted 4269/8459 = 50%, 80 KB/s], Decompressed: 4266
Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 92 KB/s], Decompressed: 4303
Downloaded: 4351 file(s) [attempted 4351/8459 = 51%, 233 KB/s], Decompressed: 4344
Downloaded: 4396 file(s) [attempted 4396/8459 = 51%, 615 KB/s], Decompressed: 4392
Downloaded: 4438 file(s) [attempted 4438/8459 = 52%, 714 KB/s], Decompressed: 4433
Downloaded: 4478 file(s) [attempted 4478/8459 = 52%, 193 KB/s], Decompressed: 4474
Downloaded: 4516 file(s) [attempted 4516/8459 = 53%, 100 KB/s], Decompressed: 4512
Downloaded: 4560 file(s) [attempted 4560/8459 = 53%, 981 KB/s], Decompressed: 4557
Downloaded: 4600 file(s) [attempted 4600/8459 = 54%, 22 KB/s], Decompressed: 4591
Downloaded: 4639 file(s) [attempted 4639/8459 = 54%, 67 KB/s], Decompressed: 4635
Downloaded: 4680 file(s) [attempted 4680/8459 = 55%, 1078 KB/s], Decompressed: 4676
Downloaded: 4717 file(s) [attempted 4717/8459 = 55%, 1439 KB/s], Decompressed: 4714
Downloaded: 4765 file(s) [attempted 4765/8459 = 56%, 380 KB/s], Decompressed: 4759
Downloaded: 4810 file(s) [attempted 4810/8459 = 56%, 207 KB/s], Decompressed: 4806
Downloaded: 4851 file(s) [attempted 4851/8459 = 57%, 283 KB/s], Decompressed: 4848
Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 100 KB/s], Decompressed: 4885
Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 173 KB/s], Decompressed: 4926
Downloaded: 4973 file(s) [attempted 4973/8459 = 58%, 517 KB/s], Decompressed: 4967
Downloaded: 5013 file(s) [attempted 5013/8459 = 59%, 91 KB/s], Decompressed: 5008
Downloaded: 5056 file(s) [attempted 5056/8459 = 59%, 104 KB/s], Decompressed: 5049
Downloaded: 5097 file(s) [attempted 5097/8459 = 60%, 536 KB/s], Decompressed: 5094
Downloaded: 5138 file(s) [attempted 5138/8459 = 60%, 497 KB/s], Decompressed: 5132
Downloaded: 5176 file(s) [attempted 5176/8459 = 61%, 164 KB/s], Decompressed: 5169
Downloaded: 5216 file(s) [attempted 5216/8459 = 61%, 335 KB/s], Decompressed: 5210
Downloaded: 5257 file(s) [attempted 5257/8459 = 62%, 137 KB/s], Decompressed: 5251
Downloaded: 5299 file(s) [attempted 5299/8459 = 62%, 633 KB/s], Decompressed: 5296
Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 255 KB/s], Decompressed: 5334
Downloaded: 5380 file(s) [attempted 5380/8459 = 63%, 914 KB/s], Decompressed: 5371
Downloaded: 5419 file(s) [attempted 5419/8459 = 64%, 282 KB/s], Decompressed: 5416
Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 24 KB/s], Decompressed: 5453
Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 1058 KB/s], Decompressed: 5494
Downloaded: 5544 file(s) [attempted 5544/8459 = 65%, 422 KB/s], Decompressed: 5535
Downloaded: 5583 file(s) [attempted 5583/8459 = 66%, 327 KB/s], Decompressed: 5573
Downloaded: 5622 file(s) [attempted 5622/8459 = 66%, 197 KB/s], Decompressed: 5618
Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 1052 KB/s], Decompressed: 5655
Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 465 KB/s], Decompressed: 5700
Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 102 KB/s], Decompressed: 5741
Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 457 KB/s], Decompressed: 5785
Downloaded: 5828 file(s) [attempted 5828/8459 = 68%, 171 KB/s], Decompressed: 5819
Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 112 KB/s], Decompressed: 5857
Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 1969 KB/s], Decompressed: 5898
Downloaded: 5948 file(s) [attempted 5948/8459 = 70%, 202 KB/s], Decompressed: 5943
Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 55 KB/s], Decompressed: 5987
Downloaded: 6032 file(s) [attempted 6032/8459 = 71%, 390 KB/s], Decompressed: 6028
Downloaded: 6072 file(s) [attempted 6072/8459 = 71%, 237 KB/s], Decompressed: 6066
Downloaded: 6104 file(s) [attempted 6104/8459 = 72%, 332 KB/s], Decompressed: 6100
Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 363 KB/s], Decompressed: 6145
Downloaded: 6195 file(s) [attempted 6195/8459 = 73%, 923 KB/s], Decompressed: 6189
Downloaded: 6237 file(s) [attempted 6237/8459 = 73%, 377 KB/s], Decompressed: 6230
Downloaded: 6275 file(s) [attempted 6275/8459 = 74%, 279 KB/s], Decompressed: 6271
Downloaded: 6312 file(s) [attempted 6312/8459 = 74%, 503 KB/s], Decompressed: 6307
Downloaded: 6350 file(s) [attempted 6350/8459 = 75%, 31 KB/s], Decompressed: 6349
Downloaded: 6391 file(s) [attempted 6391/8459 = 75%, 694 KB/s], Decompressed: 6388
Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 115 KB/s], Decompressed: 6432
Downloaded: 6483 file(s) [attempted 6483/8459 = 76%, 411 KB/s], Decompressed: 6480
Downloaded: 6531 file(s) [attempted 6531/8459 = 77%, 58 KB/s], Decompressed: 6528
Downloaded: 6566 file(s) [attempted 6566/8459 = 77%, 754 KB/s], Decompressed: 6562
Downloaded: 6607 file(s) [attempted 6607/8459 = 78%, 172 KB/s], Decompressed: 6596
Downloaded: 6644 file(s) [attempted 6644/8459 = 78%, 294 KB/s], Decompressed: 6641
Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 80 KB/s], Decompressed: 6682
Downloaded: 6730 file(s) [attempted 6730/8459 = 79%, 31 KB/s], Decompressed: 6726
Downloaded: 6774 file(s) [attempted 6774/8459 = 80%, 146 KB/s], Decompressed: 6767
Downloaded: 6815 file(s) [attempted 6815/8459 = 80%, 629 KB/s], Decompressed: 6812
Downloaded: 6856 file(s) [attempted 6856/8459 = 81%, 296 KB/s], Decompressed: 6853
Downloaded: 6895 file(s) [attempted 6895/8459 = 81%, 232 KB/s], Decompressed: 6887
Downloaded: 6935 file(s) [attempted 6935/8459 = 81%, 318 KB/s], Decompressed: 6932
Downloaded: 6975 file(s) [attempted 6975/8459 = 82%, 114 KB/s], Decompressed: 6966
Downloaded: 7014 file(s) [attempted 7014/8459 = 82%, 494 KB/s], Decompressed: 7010
Downloaded: 7059 file(s) [attempted 7059/8459 = 83%, 303 KB/s], Decompressed: 7055
Downloaded: 7099 file(s) [attempted 7099/8459 = 83%, 70 KB/s], Decompressed: 7096
Downloaded: 7140 file(s) [attempted 7140/8459 = 84%, 140 KB/s], Decompressed: 7134
Downloaded: 7178 file(s) [attempted 7178/8459 = 84%, 32 KB/s], Decompressed: 7171
Downloaded: 7216 file(s) [attempted 7216/8459 = 85%, 652 KB/s], Decompressed: 7212
Downloaded: 7257 file(s) [attempted 7257/8459 = 85%, 38 KB/s], Decompressed: 7253
Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 280 KB/s], Decompressed: 7295
Downloaded: 7342 file(s) [attempted 7342/8459 = 86%, 573 KB/s], Decompressed: 7339
Downloaded: 7380 file(s) [attempted 7380/8459 = 87%, 383 KB/s], Decompressed: 7373
Downloaded: 7414 file(s) [attempted 7414/8459 = 87%, 167 KB/s], Decompressed: 7411
Downloaded: 7457 file(s) [attempted 7457/8459 = 88%, 92 KB/s], Decompressed: 7452
Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 165 KB/s], Decompressed: 7493
Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 189 KB/s], Decompressed: 7531
Downloaded: 7577 file(s) [attempted 7577/8459 = 89%, 244 KB/s], Decompressed: 7568
Downloaded: 7616 file(s) [attempted 7616/8459 = 90%, 539 KB/s], Decompressed: 7613
Downloaded: 7658 file(s) [attempted 7658/8459 = 90%, 1680 KB/s], Decompressed: 7654
Downloaded: 7698 file(s) [attempted 7698/8459 = 91%, 47 KB/s], Decompressed: 7695
Downloaded: 7739 file(s) [attempted 7739/8459 = 91%, 1612 KB/s], Decompressed: 7736
Downloaded: 7782 file(s) [attempted 7782/8459 = 91%, 659 KB/s], Decompressed: 7774
Downloaded: 7815 file(s) [attempted 7815/8459 = 92%, 1073 KB/s], Decompressed: 7811
Downloaded: 7859 file(s) [attempted 7859/8459 = 92%, 473 KB/s], Decompressed: 7852
Downloaded: 7900 file(s) [attempted 7900/8459 = 93%, 852 KB/s], Decompressed: 7897
Downloaded: 7945 file(s) [attempted 7945/8459 = 93%, 519 KB/s], Decompressed: 7941
Downloaded: 7986 file(s) [attempted 7986/8459 = 94%, 73 KB/s], Decompressed: 7982
Downloaded: 8023 file(s) [attempted 8023/8459 = 94%, 627 KB/s], Decompressed: 8017
Downloaded: 8064 file(s) [attempted 8064/8459 = 95%, 229 KB/s], Decompressed: 8058
Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 75 KB/s], Decompressed: 8095
Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 390 KB/s], Decompressed: 8140
Downloaded: 8188 file(s) [attempted 8188/8459 = 96%, 266 KB/s], Decompressed: 8184
Downloaded: 8224 file(s) [attempted 8224/8459 = 97%, 76 KB/s], Decompressed: 8215
Downloaded: 8266 file(s) [attempted 8266/8459 = 97%, 226 KB/s], Decompressed: 8263
Downloaded: 8305 file(s) [attempted 8305/8459 = 98%, 24 KB/s], Decompressed: 8301
Downloaded: 8345 file(s) [attempted 8345/8459 = 98%, 995 KB/s], Decompressed: 8342
Downloaded: 8386 file(s) [attempted 8386/8459 = 99%, 172 KB/s], Decompressed: 8383
Downloaded: 8424 file(s) [attempted 8424/8459 = 99%, 690 KB/s], Decompressed: 8417
Downloaded: 8458 file(s) [attempted 8458/8459 = 99%, 121 KB/s], Decompressed: 8455
Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 121 KB/s], Decompressed: 8455

lean_checker exit 0 duration 26m 30s · created 6/12/2026, 7:11:19 PM

lake build

ℹ [3536/3546] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3547/3571] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (38s)
⚠ [3555/3571] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3695/3704] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3699/3730] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3760/3792] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3761/3792] 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`
⚠ [3867/3876] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3872/3887] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (6.3s)
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`
⚠ [4001/4011] 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`
✔ [4003/4012] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (46s)
⚠ [4005/4012] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (16s)
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`
⚠ [4006/4012] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4007/4012] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (92s)
⚠ [4009/4040] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
⚠ [4010/4040] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [4011/4040] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [4012/4040] Built LeanCert.Engine.FinSumDyadic (2.0s)
✔ [4014/4042] Built LeanCert.Engine.WitnessSum (2.5s)
✔ [4015/4043] Built LeanCert.Engine.ReflectiveSum (3.0s)
✔ [4017/4046] Built LeanCert.Examples.BKLNW_a2_reflective (20s)
✔ [4020/4053] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (5.4s)
✔ [4022/4053] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.7s)
⚠ [4023/4053] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [4026/4055] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (2.4s)
✔ [4027/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4028/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4029/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (96s)
✔ [4030/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (82s)
✔ [4031/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (75s)
✔ [4032/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (72s)
✔ [4033/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (63s)
✔ [4034/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (58s)
✔ [4035/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (57s)
✔ [4036/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (57s)
✔ [4037/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (54s)
✔ [4038/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (52s)
✔ [4039/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (52s)
✔ [4040/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (50s)
✔ [4041/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.4s)
✔ [4042/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (35s)
✔ [4043/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (17s)
⚠ [4044/4055] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (11s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
⚠ [4046/4060] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (21s)
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4048/4060] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (116s)
⚠ [4051/4061] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (35s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [4054/4061] Built PrimeNumberTheoremAnd.IEANTN.Dusart (18s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [4056/4062] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (75s)
✔ [4059/4063] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (2.9s)
✔ [4061/4078] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
⚠ [4073/4089] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (10s)
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4078/4100] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.4s)
⚠ [4080/4100] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4082/4102] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4085/4102] 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`
⚠ [4086/4102] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (10s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:90:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:109:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:145:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:244:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:291:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:369:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:438:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:514:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:544:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1859:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1885:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2491:8: declaration uses `sorry`
⚠ [4093/4102] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.3s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4095/4102] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.5s)
✔ [4097/4102] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
⚠ [4099/4141] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.3s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
ℹ [4100/4141] 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.
✔ [4118/4141] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
✔ [4140/4141] Built PrimeNumberTheoremAnd (2.9s)
Build completed successfully (4141 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 6m 8s · created 6/12/2026, 7:11:19 PM

lake build :blueprint

✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (769ms)
✔ [23/35] Built Cli.Basic:c.o (3.2s)
✔ [30/35] Built Cli.Extensions:c.o (514ms)
✔ [33/62] Built Cli:c.o (90ms)
ℹ [3600/3635] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3614/3636] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.1s)
⚠ [3622/3660] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
⚠ [3762/3797] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3779/3797] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3838/3860] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3840/3860] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
⚠ [3949/3970] 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`
⚠ [3951/3970] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3958/3971] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (17s)
⚠ [4093/4109] 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`
✔ [4096/4109] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (2.7s)
⚠ [4097/4109] 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`
⚠ [4099/4109] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4102/4159] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
✔ [4103/4159] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.4s)
⚠ [4104/4159] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4106/4168] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (23s)
⚠ [4107/4168] Replayed LeanCert.Examples.BKLNW_a2_pow2
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:105:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:109:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:113:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:117:8: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_pow2.lean:121:8: declaration uses `sorry`
⚠ [4108/4168] Replayed LeanCert.Examples.BKLNW_a2_bounds
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
✔ [4118/4180] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.7s)
✔ [4121/4182] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (2.9s)
⚠ [4139/4182] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1740:8: declaration uses `sorry`
✔ [4143/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (2.8s)
✔ [4144/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (2.8s)
✔ [4146/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (2.8s)
✔ [4147/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (2.8s)
✔ [4148/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (2.8s)
✔ [4149/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (2.9s)
✔ [4150/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (2.8s)
✔ [4151/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.8s)
✔ [4152/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (2.8s)
✔ [4153/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (2.8s)
✔ [4154/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (2.8s)
✔ [4155/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (2.8s)
✔ [4156/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (2.8s)
✔ [4157/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (2.8s)
✔ [4158/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (2.9s)
✔ [4159/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.7s)
✔ [4160/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (2.8s)
⚠ [4162/4190] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3253:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3430:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3442:8: declaration uses `sorry`
✔ [4165/4190] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.3s)
⚠ [4166/4190] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
⚠ [4169/4191] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
✔ [4172/4191] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (18s)
✔ [4174/4191] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.1s)
⚠ [4175/4191] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [4177/4192] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (2.8s)
✔ [4179/4192] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4182/4193] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.8s)
✔ [4185/4193] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (18s)
✔ [4188/4195] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (2.9s)
✔ [4192/4224] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (10s)
⚠ [4201/4224] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4206/4252] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (2.6s)
✔ [4213/4255] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (2.9s)
⚠ [4214/4255] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4216/4255] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1000:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1004:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1014:8: declaration uses `sorry`
⚠ [4219/4255] 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`
✔ [4226/4255] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (44s)
⚠ [4227/4255] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
⚠ [4229/4255] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:90:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:109:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:145:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:244:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:291:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:369:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:438:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:514:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:544:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1859:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1885:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2491:8: declaration uses `sorry`
✔ [4242/4316] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (36s)
✔ [4243/4328] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.3s)
⚠ [4244/4328] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4246/4328] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.7s)
ℹ [4247/4328] 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.
✔ [4265/4328] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4267/4328] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.8s)
✔ [4293/4328] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4326/4329] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (2.9s)
ℹ [4327/4329] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (57ms)
info: Blueprint indexing
Build completed successfully (4329 jobs).

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

semantic_extract exit 0 duration 6m 0s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 4m 47s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 22s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 11m 38s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 25s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 23s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 49s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 10s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 25s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 20s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 56s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 11s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 19s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 39s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 34s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 46s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 41s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 37s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 43s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 1s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 10s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 5s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 10s · created 6/12/2026, 7:11:19 PM

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

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

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

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

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

semantic_extract exit 0 duration 7m 12s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 12s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 21s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 18s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 16s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 14s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 20s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 10s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 38s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 42s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 35s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 54s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 8m 14s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 7m 16s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 36s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 40s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 57s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 51s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 32s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 42s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 4m 37s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 4m 24s · created 6/12/2026, 7:11:19 PM

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

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

semantic_extract exit 0 duration 6m 55s · created 6/12/2026, 7:11:19 PM

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

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