Run 1

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

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

lake exe cache get

installing leantar 0.1.17
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
Attempting to download 8232 file(s) from leanprover-community/mathlib4 cache
Decompressed 8232 file(s)
Already decompressed 8232 file(s)

info: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision '2030255c7e3efb07074171879ec920b500ee0e58'
info: leancert: cloning https://github.com/alerad/leancert
info: leancert: checking out revision '6237c769e79d4cefec17f5f3c40d288a9baa01e5'
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '8a178386ffc0f5fef0b77738bb5449d50efeea95'
info: LeanArchitect: cloning https://github.com/hanwenzhu/LeanArchitect.git
info: LeanArchitect: checking out revision '719ea595bb100be70d0b53b01eca828862d9f860'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '83e90935a17ca19ebe4b7893c7f7066e266f50d3'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '48d5698bc464786347c1b0d859b18f938420f060'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '7152850e7b216a0d409701617721b6e469d34bf6'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '707efb56d0696634e9e965523a1bbe9ac6ce141d'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '756e3321fd3b02a85ffda19fef789916223e578c'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '7802da01beb530bf051ab657443f9cd9bc3e1a29'
✔ [2/22] Built Cache.Lean (472ms)
✔ [3/22] Built Cache.Init (372ms)
✔ [4/22] Built Cache.Init:c.o (168ms)
✔ [5/22] Built Cache.Lean:c.o (138ms)
✔ [6/22] Built Cache.IO (1.4s)
✔ [7/22] Built Cache.Hashing (728ms)
✔ [8/22] Built Cache.Hashing:c.o (414ms)
✔ [9/22] Built Cache.IO:c.o (1.3s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (93ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (234ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (172ms)
✔ [18/22] Built Cache.Requests (1.0s)
✔ [19/22] Built Cache.Main (836ms)
✔ [20/22] Built Cache.Main:c.o (516ms)
✔ [21/22] Built Cache.Requests:c.o (2.1s)
✔ [22/22] Built cache:exe (1.0s)
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0

100 1119k  100 1119k    0     0  2112k      0 --:--:-- --:--:-- --:--:-- 2112k


Downloaded: 1 file(s) [attempted 1/8232 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8232 = 0%, 1 KB/s], Decompressed: 8
Downloaded: 38 file(s) [attempted 38/8232 = 0%, 15 KB/s], Decompressed: 28
Downloaded: 68 file(s) [attempted 68/8232 = 0%, 265 KB/s], Decompressed: 62
Downloaded: 100 file(s) [attempted 100/8232 = 1%, 424 KB/s], Decompressed: 86
Downloaded: 136 file(s) [attempted 136/8232 = 1%, 35 KB/s], Decompressed: 117
Downloaded: 168 file(s) [attempted 168/8232 = 2%, 438 KB/s], Decompressed: 148
Downloaded: 206 file(s) [attempted 206/8232 = 2%, 351 KB/s], Decompressed: 168
Downloaded: 247 file(s) [attempted 247/8232 = 3%, 119 KB/s], Decompressed: 213
Downloaded: 282 file(s) [attempted 282/8232 = 3%, 40 KB/s], Decompressed: 237
Downloaded: 323 file(s) [attempted 323/8232 = 3%, 280 KB/s], Decompressed: 285
Downloaded: 367 file(s) [attempted 367/8232 = 4%, 109 KB/s], Decompressed: 329
Downloaded: 408 file(s) [attempted 408/8232 = 4%, 158 KB/s], Decompressed: 374
Downloaded: 449 file(s) [attempted 449/8232 = 5%, 205 KB/s], Decompressed: 419
Downloaded: 490 file(s) [attempted 490/8232 = 5%, 794 KB/s], Decompressed: 463
Downloaded: 528 file(s) [attempted 528/8232 = 6%, 34 KB/s], Decompressed: 490
Downloaded: 566 file(s) [attempted 566/8232 = 6%, 569 KB/s], Decompressed: 518
Downloaded: 607 file(s) [attempted 607/8232 = 7%, 278 KB/s], Decompressed: 562
Downloaded: 645 file(s) [attempted 645/8232 = 7%, 779 KB/s], Decompressed: 604
Downloaded: 686 file(s) [attempted 686/8232 = 8%, 278 KB/s], Decompressed: 641
Downloaded: 730 file(s) [attempted 730/8232 = 8%, 81 KB/s], Decompressed: 707
Downloaded: 775 file(s) [attempted 775/8232 = 9%, 59 KB/s], Decompressed: 730
Downloaded: 816 file(s) [attempted 816/8232 = 9%, 334 KB/s], Decompressed: 778
Downloaded: 857 file(s) [attempted 857/8232 = 10%, 153 KB/s], Decompressed: 806
Downloaded: 897 file(s) [attempted 897/8232 = 10%, 191 KB/s], Decompressed: 867
Downloaded: 939 file(s) [attempted 939/8232 = 11%, 138 KB/s], Decompressed: 895
Downloaded: 980 file(s) [attempted 980/8232 = 11%, 213 KB/s], Decompressed: 953
Downloaded: 1015 file(s) [attempted 1015/8232 = 12%, 619 KB/s], Decompressed: 980
Downloaded: 1062 file(s) [attempted 1062/8232 = 12%, 74 KB/s], Decompressed: 1011
Downloaded: 1110 file(s) [attempted 1110/8232 = 13%, 361 KB/s], Decompressed: 1042
Downloaded: 1151 file(s) [attempted 1151/8232 = 13%, 217 KB/s], Decompressed: 1083
Downloaded: 1193 file(s) [attempted 1193/8232 = 14%, 520 KB/s], Decompressed: 1121
Downloaded: 1234 file(s) [attempted 1234/8232 = 14%, 106 KB/s], Decompressed: 1162
Downloaded: 1275 file(s) [attempted 1275/8232 = 15%, 778 KB/s], Decompressed: 1210
Downloaded: 1312 file(s) [attempted 1312/8232 = 15%, 64 KB/s], Decompressed: 1210
Downloaded: 1357 file(s) [attempted 1357/8232 = 16%, 27 KB/s], Decompressed: 1261
Downloaded: 1398 file(s) [attempted 1398/8232 = 16%, 588 KB/s], Decompressed: 1319
Downloaded: 1436 file(s) [attempted 1436/8232 = 17%, 43 KB/s], Decompressed: 1377
Downloaded: 1477 file(s) [attempted 1477/8232 = 17%, 145 KB/s], Decompressed: 1418
Downloaded: 1518 file(s) [attempted 1518/8232 = 18%, 237 KB/s], Decompressed: 1463
Downloaded: 1562 file(s) [attempted 1562/8232 = 18%, 157 KB/s], Decompressed: 1501
Downloaded: 1603 file(s) [attempted 1603/8232 = 19%, 416 KB/s], Decompressed: 1569
Downloaded: 1641 file(s) [attempted 1641/8232 = 19%, 1596 KB/s], Decompressed: 1593
Downloaded: 1685 file(s) [attempted 1685/8232 = 20%, 210 KB/s], Decompressed: 1648
Downloaded: 1733 file(s) [attempted 1733/8232 = 21%, 230 KB/s], Decompressed: 1679
Downloaded: 1771 file(s) [attempted 1771/8232 = 21%, 197 KB/s], Decompressed: 1737
Downloaded: 1809 file(s) [attempted 1809/8232 = 21%, 22 KB/s], Decompressed: 1771
Downloaded: 1846 file(s) [attempted 1846/8232 = 22%, 1378 KB/s], Decompressed: 1802
Downloaded: 1887 file(s) [attempted 1887/8232 = 22%, 119 KB/s], Decompressed: 1833
Downloaded: 1928 file(s) [attempted 1928/8232 = 23%, 2554 KB/s], Decompressed: 1863
Downloaded: 1969 file(s) [attempted 1969/8232 = 23%, 369 KB/s], Decompressed: 1894
Downloaded: 2007 file(s) [attempted 2007/8232 = 24%, 811 KB/s], Decompressed: 1894
Downloaded: 2045 file(s) [attempted 2045/8232 = 24%, 708 KB/s], Decompressed: 1966
Downloaded: 2086 file(s) [attempted 2086/8232 = 25%, 86 KB/s], Decompressed: 1966
Downloaded: 2127 file(s) [attempted 2127/8232 = 25%, 1235 KB/s], Decompressed: 2038
Downloaded: 2168 file(s) [attempted 2168/8232 = 26%, 182 KB/s], Decompressed: 2038
Downloaded: 2212 file(s) [attempted 2212/8232 = 26%, 286 KB/s], Decompressed: 2123
Downloaded: 2253 file(s) [attempted 2253/8232 = 27%, 188 KB/s], Decompressed: 2123
Downloaded: 2288 file(s) [attempted 2288/8232 = 27%, 181 KB/s], Decompressed: 2212
Downloaded: 2329 file(s) [attempted 2329/8232 = 28%, 703 KB/s], Decompressed: 2212
Downloaded: 2370 file(s) [attempted 2370/8232 = 28%, 33 KB/s], Decompressed: 2288
Downloaded: 2407 file(s) [attempted 2407/8232 = 29%, 348 KB/s], Decompressed: 2288
Downloaded: 2452 file(s) [attempted 2452/8232 = 29%, 46 KB/s], Decompressed: 2363
Downloaded: 2486 file(s) [attempted 2486/8232 = 30%, 128 KB/s], Decompressed: 2363
Downloaded: 2531 file(s) [attempted 2531/8232 = 30%, 355 KB/s], Decompressed: 2431
Downloaded: 2572 file(s) [attempted 2572/8232 = 31%, 116 KB/s], Decompressed: 2431
Downloaded: 2613 file(s) [attempted 2613/8232 = 31%, 215 KB/s], Decompressed: 2514
Downloaded: 2650 file(s) [attempted 2650/8232 = 32%, 258 KB/s], Decompressed: 2514
Downloaded: 2692 file(s) [attempted 2692/8232 = 32%, 864 KB/s], Decompressed: 2582
Downloaded: 2733 file(s) [attempted 2733/8232 = 33%, 131 KB/s], Decompressed: 2582
Downloaded: 2777 file(s) [attempted 2777/8232 = 33%, 114 KB/s], Decompressed: 2661
Downloaded: 2822 file(s) [attempted 2822/8232 = 34%, 129 KB/s], Decompressed: 2739
Downloaded: 2859 file(s) [attempted 2859/8232 = 34%, 597 KB/s], Decompressed: 2739
Downloaded: 2900 file(s) [attempted 2900/8232 = 35%, 99 KB/s], Decompressed: 2739
Downloaded: 2941 file(s) [attempted 2941/8232 = 35%, 206 KB/s], Decompressed: 2822
Downloaded: 2982 file(s) [attempted 2982/8232 = 36%, 149 KB/s], Decompressed: 2822
Downloaded: 3027 file(s) [attempted 3027/8232 = 36%, 27 KB/s], Decompressed: 2913
Downloaded: 3068 file(s) [attempted 3068/8232 = 37%, 335 KB/s], Decompressed: 2913
Downloaded: 3109 file(s) [attempted 3109/8232 = 37%, 218 KB/s], Decompressed: 2996
Downloaded: 3150 file(s) [attempted 3150/8232 = 38%, 151 KB/s], Decompressed: 2996
Downloaded: 3191 file(s) [attempted 3191/8232 = 38%, 938 KB/s], Decompressed: 2996
Downloaded: 3232 file(s) [attempted 3232/8232 = 39%, 82 KB/s], Decompressed: 3095
Downloaded: 3273 file(s) [attempted 3273/8232 = 39%, 77 KB/s], Decompressed: 3095
Downloaded: 3318 file(s) [attempted 3318/8232 = 40%, 630 KB/s], Decompressed: 3201
Downloaded: 3362 file(s) [attempted 3362/8232 = 40%, 80 KB/s], Decompressed: 3201
Downloaded: 3403 file(s) [attempted 3403/8232 = 41%, 463 KB/s], Decompressed: 3201
Downloaded: 3441 file(s) [attempted 3441/8232 = 41%, 155 KB/s], Decompressed: 3314
Downloaded: 3479 file(s) [attempted 3479/8232 = 42%, 442 KB/s], Decompressed: 3314
Downloaded: 3523 file(s) [attempted 3523/8232 = 42%, 172 KB/s], Decompressed: 3314
Downloaded: 3568 file(s) [attempted 3568/8232 = 43%, 611 KB/s], Decompressed: 3427
Downloaded: 3616 file(s) [attempted 3616/8232 = 43%, 58 KB/s], Decompressed: 3427
Downloaded: 3664 file(s) [attempted 3664/8232 = 44%, 74 KB/s], Decompressed: 3540
Downloaded: 3699 file(s) [attempted 3699/8232 = 44%, 124 KB/s], Decompressed: 3540
Downloaded: 3742 file(s) [attempted 3742/8232 = 45%, 82 KB/s], Decompressed: 3540
Downloaded: 3780 file(s) [attempted 3780/8232 = 45%, 84 KB/s], Decompressed: 3657
Downloaded: 3821 file(s) [attempted 3821/8232 = 46%, 58 KB/s], Decompressed: 3657
Downloaded: 3865 file(s) [attempted 3865/8232 = 46%, 105 KB/s], Decompressed: 3759
Downloaded: 3907 file(s) [attempted 3907/8232 = 47%, 246 KB/s], Decompressed: 3759
Downloaded: 3942 file(s) [attempted 3942/8232 = 47%, 131 KB/s], Decompressed: 3852
Downloaded: 3978 file(s) [attempted 3978/8232 = 48%, 128 KB/s], Decompressed: 3852
Downloaded: 4019 file(s) [attempted 4019/8232 = 48%, 318 KB/s], Decompressed: 3852
Downloaded: 4067 file(s) [attempted 4067/8232 = 49%, 199 KB/s], Decompressed: 3941
Downloaded: 4115 file(s) [attempted 4115/8232 = 49%, 88 KB/s], Decompressed: 3941
Downloaded: 4163 file(s) [attempted 4163/8232 = 50%, 443 KB/s], Decompressed: 4037
Downloaded: 4208 file(s) [attempted 4208/8232 = 51%, 228 KB/s], Decompressed: 4037
Downloaded: 4249 file(s) [attempted 4249/8232 = 51%, 169 KB/s], Decompressed: 4126
Downloaded: 4286 file(s) [attempted 4286/8232 = 52%, 348 KB/s], Decompressed: 4126
Downloaded: 4327 file(s) [attempted 4327/8232 = 52%, 519 KB/s], Decompressed: 4126
Downloaded: 4369 file(s) [attempted 4369/8232 = 53%, 125 KB/s], Decompressed: 4235
Downloaded: 4413 file(s) [attempted 4413/8232 = 53%, 329 KB/s], Decompressed: 4235
Downloaded: 4447 file(s) [attempted 4447/8232 = 54%, 171 KB/s], Decompressed: 4235
Downloaded: 4495 file(s) [attempted 4495/8232 = 54%, 20 KB/s], Decompressed: 4351
Downloaded: 4543 file(s) [attempted 4543/8232 = 55%, 357 KB/s], Decompressed: 4351
Downloaded: 4581 file(s) [attempted 4581/8232 = 55%, 386 KB/s], Decompressed: 4464
Downloaded: 4622 file(s) [attempted 4622/8232 = 56%, 94 KB/s], Decompressed: 4464
Downloaded: 4663 file(s) [attempted 4663/8232 = 56%, 116 KB/s], Decompressed: 4464
Downloaded: 4701 file(s) [attempted 4701/8232 = 57%, 414 KB/s], Decompressed: 4567
Downloaded: 4745 file(s) [attempted 4745/8232 = 57%, 83 KB/s], Decompressed: 4567
Downloaded: 4789 file(s) [attempted 4789/8232 = 58%, 2732 KB/s], Decompressed: 4677
Downloaded: 4831 file(s) [attempted 4831/8232 = 58%, 51 KB/s], Decompressed: 4677
Downloaded: 4872 file(s) [attempted 4872/8232 = 59%, 823 KB/s], Decompressed: 4677
Downloaded: 4913 file(s) [attempted 4913/8232 = 59%, 328 KB/s], Decompressed: 4783
Downloaded: 4950 file(s) [attempted 4950/8232 = 60%, 230 KB/s], Decompressed: 4783
Downloaded: 4995 file(s) [attempted 4995/8232 = 60%, 68 KB/s], Decompressed: 4875
Downloaded: 5039 file(s) [attempted 5039/8232 = 61%, 73 KB/s], Decompressed: 4875
Downloaded: 5080 file(s) [attempted 5080/8232 = 61%, 23 KB/s], Decompressed: 4967
Downloaded: 5122 file(s) [attempted 5122/8232 = 62%, 89 KB/s], Decompressed: 5043
Downloaded: 5163 file(s) [attempted 5163/8232 = 62%, 57 KB/s], Decompressed: 5043
Downloaded: 5200 file(s) [attempted 5200/8232 = 63%, 423 KB/s], Decompressed: 5122
Downloaded: 5241 file(s) [attempted 5241/8232 = 63%, 309 KB/s], Decompressed: 5122
Downloaded: 5282 file(s) [attempted 5282/8232 = 64%, 166 KB/s], Decompressed: 5187
Downloaded: 5327 file(s) [attempted 5327/8232 = 64%, 47 KB/s], Decompressed: 5187
Downloaded: 5364 file(s) [attempted 5364/8232 = 65%, 983 KB/s], Decompressed: 5255
Downloaded: 5406 file(s) [attempted 5406/8232 = 65%, 422 KB/s], Decompressed: 5334
Downloaded: 5450 file(s) [attempted 5450/8232 = 66%, 1594 KB/s], Decompressed: 5334
Downloaded: 5488 file(s) [attempted 5488/8232 = 66%, 25 KB/s], Decompressed: 5406
Downloaded: 5532 file(s) [attempted 5532/8232 = 67%, 48 KB/s], Decompressed: 5406
Downloaded: 5577 file(s) [attempted 5577/8232 = 67%, 285 KB/s], Decompressed: 5474
Downloaded: 5614 file(s) [attempted 5614/8232 = 68%, 208 KB/s], Decompressed: 5539
Downloaded: 5655 file(s) [attempted 5655/8232 = 68%, 134 KB/s], Decompressed: 5539
Downloaded: 5700 file(s) [attempted 5700/8232 = 69%, 921 KB/s], Decompressed: 5607
Downloaded: 5741 file(s) [attempted 5741/8232 = 69%, 88 KB/s], Decompressed: 5676
Downloaded: 5782 file(s) [attempted 5782/8232 = 70%, 1443 KB/s], Decompressed: 5676
Downloaded: 5820 file(s) [attempted 5820/8232 = 70%, 224 KB/s], Decompressed: 5734
Downloaded: 5857 file(s) [attempted 5857/8232 = 71%, 82 KB/s], Decompressed: 5799
Downloaded: 5895 file(s) [attempted 5895/8232 = 71%, 224 KB/s], Decompressed: 5799
Downloaded: 5939 file(s) [attempted 5939/8232 = 72%, 106 KB/s], Decompressed: 5857
Downloaded: 5984 file(s) [attempted 5984/8232 = 72%, 795 KB/s], Decompressed: 5909
Downloaded: 6025 file(s) [attempted 6025/8232 = 73%, 492 KB/s], Decompressed: 5960
Downloaded: 6056 file(s) [attempted 6056/8232 = 73%, 38 KB/s], Decompressed: 5960
Downloaded: 6097 file(s) [attempted 6097/8232 = 74%, 147 KB/s], Decompressed: 6022
Downloaded: 6141 file(s) [attempted 6141/8232 = 74%, 242 KB/s], Decompressed: 6080
Downloaded: 6186 file(s) [attempted 6186/8232 = 75%, 56 KB/s], Decompressed: 6080
Downloaded: 6227 file(s) [attempted 6227/8232 = 75%, 350 KB/s], Decompressed: 6141
Downloaded: 6261 file(s) [attempted 6261/8232 = 76%, 1630 KB/s], Decompressed: 6141
Downloaded: 6302 file(s) [attempted 6302/8232 = 76%, 130 KB/s], Decompressed: 6206
Downloaded: 6347 file(s) [attempted 6347/8232 = 77%, 760 KB/s], Decompressed: 6206
Downloaded: 6391 file(s) [attempted 6391/8232 = 77%, 577 KB/s], Decompressed: 6285
Downloaded: 6429 file(s) [attempted 6429/8232 = 78%, 53 KB/s], Decompressed: 6350
Downloaded: 6463 file(s) [attempted 6463/8232 = 78%, 249 KB/s], Decompressed: 6350
Downloaded: 6504 file(s) [attempted 6504/8232 = 79%, 394 KB/s], Decompressed: 6412
Downloaded: 6545 file(s) [attempted 6545/8232 = 79%, 145 KB/s], Decompressed: 6471
Downloaded: 6590 file(s) [attempted 6590/8232 = 80%, 354 KB/s], Decompressed: 6525
Downloaded: 6631 file(s) [attempted 6631/8232 = 80%, 22 KB/s], Decompressed: 6525
Downloaded: 6665 file(s) [attempted 6665/8232 = 80%, 282 KB/s], Decompressed: 6573
Downloaded: 6706 file(s) [attempted 6706/8232 = 81%, 65 KB/s], Decompressed: 6638
Downloaded: 6747 file(s) [attempted 6747/8232 = 81%, 74 KB/s], Decompressed: 6692
Downloaded: 6792 file(s) [attempted 6792/8232 = 82%, 130 KB/s], Decompressed: 6692
Downloaded: 6836 file(s) [attempted 6836/8232 = 83%, 93 KB/s], Decompressed: 6744
Downloaded: 6877 file(s) [attempted 6877/8232 = 83%, 216 KB/s], Decompressed: 6798
Downloaded: 6915 file(s) [attempted 6915/8232 = 84%, 141 KB/s], Decompressed: 6857
Downloaded: 6956 file(s) [attempted 6956/8232 = 84%, 74 KB/s], Decompressed: 6857
Downloaded: 6997 file(s) [attempted 6997/8232 = 84%, 118 KB/s], Decompressed: 6915
Downloaded: 7041 file(s) [attempted 7041/8232 = 85%, 120 KB/s], Decompressed: 6915
Downloaded: 7086 file(s) [attempted 7086/8232 = 86%, 206 KB/s], Decompressed: 6987
Downloaded: 7127 file(s) [attempted 7127/8232 = 86%, 307 KB/s], Decompressed: 6987
Downloaded: 7168 file(s) [attempted 7168/8232 = 87%, 121 KB/s], Decompressed: 7055
Downloaded: 7209 file(s) [attempted 7209/8232 = 87%, 105 KB/s], Decompressed: 7055
Downloaded: 7250 file(s) [attempted 7250/8232 = 88%, 218 KB/s], Decompressed: 7137
Downloaded: 7295 file(s) [attempted 7295/8232 = 88%, 1221 KB/s], Decompressed: 7137
Downloaded: 7339 file(s) [attempted 7339/8232 = 89%, 47 KB/s], Decompressed: 7219
Downloaded: 7377 file(s) [attempted 7377/8232 = 89%, 855 KB/s], Decompressed: 7219
Downloaded: 7418 file(s) [attempted 7418/8232 = 90%, 496 KB/s], Decompressed: 7312
Downloaded: 7459 file(s) [attempted 7459/8232 = 90%, 360 KB/s], Decompressed: 7312
Downloaded: 7500 file(s) [attempted 7500/8232 = 91%, 1121 KB/s], Decompressed: 7401
Downloaded: 7541 file(s) [attempted 7541/8232 = 91%, 336 KB/s], Decompressed: 7401
Downloaded: 7586 file(s) [attempted 7586/8232 = 92%, 144 KB/s], Decompressed: 7401
Downloaded: 7620 file(s) [attempted 7620/8232 = 92%, 344 KB/s], Decompressed: 7500
Downloaded: 7654 file(s) [attempted 7654/8232 = 92%, 667 KB/s], Decompressed: 7500
Downloaded: 7702 file(s) [attempted 7702/8232 = 93%, 408 KB/s], Decompressed: 7500
Downloaded: 7746 file(s) [attempted 7746/8232 = 94%, 135 KB/s], Decompressed: 7606
Downloaded: 7790 file(s) [attempted 7790/8232 = 94%, 291 KB/s], Decompressed: 7606
Downloaded: 7822 file(s) [attempted 7822/8232 = 95%, 1877 KB/s], Decompressed: 7606
Downloaded: 7856 file(s) [attempted 7856/8232 = 95%, 487 KB/s], Decompressed: 7705
Downloaded: 7904 file(s) [attempted 7904/8232 = 96%, 35 KB/s], Decompressed: 7705
Downloaded: 7952 file(s) [attempted 7952/8232 = 96%, 117 KB/s], Decompressed: 7705
Downloaded: 7996 file(s) [attempted 7996/8232 = 97%, 788 KB/s], Decompressed: 7829
Downloaded: 8037 file(s) [attempted 8037/8232 = 97%, 73 KB/s], Decompressed: 7829
Downloaded: 8078 file(s) [attempted 8078/8232 = 98%, 619 KB/s], Decompressed: 7829
Downloaded: 8113 file(s) [attempted 8113/8232 = 98%, 96 KB/s], Decompressed: 7962
Downloaded: 8157 file(s) [attempted 8157/8232 = 99%, 1438 KB/s], Decompressed: 7962
Downloaded: 8202 file(s) [attempted 8202/8232 = 99%, 146 KB/s], Decompressed: 7962
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 269 KB/s], Decompressed: 8099
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 269 KB/s], Decompressed: 8099

lake build

✔ [2765/2805] Built Architect.Command (4.7s)
✔ [2810/2831] Built Architect.Basic (5.1s)
✔ [2813/2831] Built Architect.Tactic (1.6s)
✔ [2814/2831] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (2.4s)
✔ [2815/2838] Built PrimeNumberTheoremAnd.Auxiliary (7.4s)
✔ [2822/2842] Built Architect.CollectUsed (1.4s)
✔ [2946/2984] Built Architect.Content (1.4s)
✔ [2972/3005] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (2.7s)
✔ [3113/3196] Built Architect.Attribute (1.0s)
✔ [3114/3196] Built Architect.Output (2.0s)
✔ [3440/3464] Built Architect.Load (1.1s)
✔ [3443/3468] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.3s)
✔ [3445/3468] Built Architect (1.1s)
✔ [3446/3468] Built PrimeNumberTheoremAnd.Sobolev (11s)
✔ [3449/3468] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (1.0s)
✔ [3450/3468] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (4.9s)
✔ [3451/3469] Built PrimeNumberTheoremAnd.SmoothExistence (4.4s)
✔ [3454/3472] Built PrimeNumberTheoremAnd.ZetaConj (4.8s)
✔ [3455/3473] Built PrimeNumberTheoremAnd.Rectangle (5.0s)
✔ [3458/3474] Built PrimeNumberTheoremAnd.Fourier (4.3s)
✔ [3461/3474] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (5.5s)
✔ [3464/3481] Built PrimeNumberTheoremAnd.Defs (8.6s)
✔ [3584/3606] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (13s)
✔ [3587/3612] Built PrimeNumberTheoremAnd.HadamardFactorization (1.9s)
✔ [3588/3612] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (10s)
✔ [3589/3613] Built PrimeNumberTheoremAnd.MellinCalculus (17s)
✔ [3593/3613] Built PrimeNumberTheoremAnd.HoffsteinLockhart (3.4s)
✔ [3596/3613] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.7s)
✔ [3599/3617] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (6.5s)
✔ [3602/3617] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (8.3s)
✔ [3604/3617] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (17s)
✔ [3605/3617] Built PrimeNumberTheoremAnd.BrunTitchmarsh (10s)
⚠ [3606/3632] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (9.7s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3631/3675] Built PrimeNumberTheoremAnd.IEANTN.KLN (9.8s)
✔ [3665/3686] Built LeanCert.Core.Interval (8.6s)
✔ [3666/3687] Built LeanCert.Core.Expr (12s)
✔ [3667/3687] Built LeanCert.Core.Support (5.9s)
✔ [3668/3688] Built LeanCert.Core.IntervalRat.Basic (15s)
✔ [3669/3688] Built LeanCert.Meta.Numeral (6.7s)
✔ [3670/3688] Built PrimeNumberTheoremAnd.ZetaBounds (57s)
✔ [3671/3688] Built LeanCert.Tactic.IntervalAuto.Types (5.1s)
✔ [3672/3693] Built LeanCert.Core.IntervalRat.Transcendental (7.8s)
✔ [3673/3693] Built LeanCert.Tactic.IntervalAuto.Extract (4.8s)
✔ [3674/3693] Built LeanCert.Core.IntervalRat.LogReduction (8.1s)
✔ [3675/3693] Built LeanCert.Meta.ToExpr (5.6s)
✔ [3676/3694] Built LeanCert.Tactic.IntervalAuto.Norm (3.6s)
⚠ [3678/3696] Built PrimeNumberTheoremAnd.Wiener (68s)
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
✔ [3679/3697] Built LeanCert.Core.DerivativeIntervals (9.2s)
✔ [3680/3699] Built LeanCert.Tactic.IntervalAuto.Parse (14s)
✔ [3681/3699] Built LeanCert.Core.Taylor (16s)
✔ [3682/3699] Built LeanCert.Tactic.IntervalAuto.Diagnostic (8.7s)
✔ [3683/3701] Built LeanCert.Core.IntervalRat.Taylor (28s)
✔ [3684/3701] Built PrimeNumberTheoremAnd.Consequences (91s)
ℹ [3685/3702] Built PrimeNumberTheoremAnd.MediumPNT (106s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3686/3710] Built LeanCert.Core.IntervalRat.TrigReduced (31s)
⚠ [3687/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (114s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3688/3710] Built LeanCert.Core.IntervalReal (9.7s)
⚠ [3689/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (3.8s)
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`
✔ [3690/3726] Built LeanCert.Contrib.Sinc (5.1s)
✔ [3701/3732] Built LeanCert.Core.IntervalRealEndpoints (5.5s)
✔ [3702/3737] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (3.8s)
✔ [3703/3740] Built LeanCert.Core.Dyadic (4.0s)
✔ [3704/3740] Built LeanCert.Engine.Affine.Basic (9.5s)
✔ [3705/3742] Built LeanCert.Engine.Eval.Core (11s)
✔ [3706/3771] Built LeanCert.Core.IntervalDyadic (12s)
✔ [3708/3773] Built LeanCert.Engine.Eval.Extended (4.8s)
✔ [3709/3773] Built LeanCert.Engine.Affine.Nonlinear (6.2s)
⚠ [3710/3774] Built PrimeNumberTheoremAnd.StrongPNT (33s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1477:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1526:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1643:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2183:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2273:6: declaration uses `sorry`
✔ [3713/3774] Built LeanCert.Tactic.Bound.Lemmas (4.1s)
✔ [3715/3776] Built LeanCert.Engine.IntervalEval (2.9s)
✔ [3716/3776] Built PrimeNumberTheoremAnd.BorelCaratheodory (6.0s)
✔ [3717/3776] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (10s)
✔ [3718/3776] Built LeanCert.Engine.Affine.Transcendental (3.7s)
✔ [3719/3776] Built LeanCert.Engine.IntervalEvalDyadic (4.4s)
✔ [3720/3776] Built LeanCert.Engine.Integrate (5.3s)
✔ [3721/3776] Built LeanCert.Engine.RootFinding.Basic (4.6s)
✔ [3722/3778] Built LeanCert.Engine.Optimization.Box (2.7s)
✔ [3724/3778] Built LeanCert.Engine.AD.Basic (2.6s)
⚠ [3725/3778] Built PrimeNumberTheoremAnd.DerivativeBound (3.4s)
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
✔ [3726/3778] Built LeanCert.Engine.IntervalEvalAffine (3.8s)
✔ [3727/3780] Built LeanCert.Engine.TaylorModel.Core (8.1s)
✔ [3730/3782] Built LeanCert.Validity.DyadicBounds (3.3s)
✔ [3731/3782] Built LeanCert.Engine.RootFinding.Bisection (3.8s)
✔ [3732/3782] Built LeanCert.Engine.AD.Transcendental (3.9s)
✔ [3733/3782] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (27s)
✔ [3734/3782] Built LeanCert.Engine.TaylorModel.Special (2.0s)
✔ [3735/3784] Built LeanCert.Engine.TaylorModel.Log1p (6.4s)
✔ [3738/3784] Built LeanCert.Engine.AD.Eval (4.6s)
✔ [3739/3784] Built LeanCert.Engine.TaylorModel.ExpLog (9.3s)
✔ [3740/3784] Built LeanCert.Engine.TaylorModel.Hyperbolic (13s)
✔ [3744/3786] Built LeanCert.Engine.TaylorModel.Trig (11s)
⚠ [3749/3786] Built LeanCert.Examples.Li2Bounds (4.6s)
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3750/3790] Built LeanCert.Engine.TaylorModel.Functions (2.3s)
✔ [3751/3792] Built LeanCert.Engine.AD.Correctness (3.7s)
✔ [3753/3794] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (4.6s)
✔ [3754/3794] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (11s)
✔ [3856/3900] Built LeanCert.Engine.AD.Computable (3.8s)
✔ [3857/3901] Built LeanCert.Engine.TaylorModel.Expr (5.2s)
✔ [3858/3901] Built LeanCert.Tactic.VecUtil (2.7s)
✔ [3859/3903] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (2.0s)
✔ [3861/3907] Built LeanCert.Engine.AD.PartialCorrectness (5.6s)
✔ [3863/3914] Built LeanCert.Engine.TaylorModel (2.4s)
✔ [3867/3914] Built LeanCert.Tactic.FinSumExpand (2.4s)
✔ [3868/3914] Built LeanCert.Engine.AD (2.4s)
✔ [3869/3916] Built LeanCert.Engine.Chebyshev.Psi (5.6s)
✔ [3870/3916] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (5.3s)
✔ [3871/3916] Built LeanCert.Meta.ProveSupported (4.8s)
✔ [3872/3916] Built LeanCert.Engine.IntervalEvalRefined (5.5s)
✔ [3873/3916] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (19s)
✔ [3875/3921] Built LeanCert.Engine.ChebyshevPsi (3.5s)
✔ [3876/3921] Built LeanCert.Engine.Optimize (8.4s)
✔ [3877/3921] Built LeanCert.Meta.ProveContinuous (5.0s)
✔ [3880/3922] Built PrimeNumberTheoremAnd.Tactic.Simprocs (4.6s)
✔ [3882/3923] Built LeanCert.Tactic.IntervalAuto.ProveCommon (8.3s)
✔ [3883/3923] Built LeanCert.Engine.Optimization.Gradient (6.8s)
✔ [3884/3924] Built LeanCert.Engine.RootFinding.Newton (6.3s)
✔ [3885/3924] Built PrimeCert.Interval (4.2s)
✔ [3886/3924] Built LeanCert.Tactic.IntervalAuto.Basic (3.2s)
✔ [3887/3924] Built PrimeCert.Meta.PrimeCert (2.6s)
✔ [3888/3925] Built LeanCert.Engine.RootFinding.MVTBounds (12s)
✔ [3889/3925] Built PrimeCert.Meta.SmallPrime (3.6s)
✔ [3890/3926] Built LeanCert.Engine.Optimization.Global (25s)
⚠ [3891/3926] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (49s)
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`
✔ [3892/3926] Built PrimeCert.PredMod (822ms)
✔ [3893/3938] Built PrimeCert.PowMod (3.7s)
✔ [3896/3938] Built LeanCert.Engine.RootFinding.Contraction (13s)
✔ [3897/3938] Built LeanCert.Engine.Optimization.BoundVerify (6.1s)
⚠ [3898/3938] Built PrimeCert.Pocklington (6.8s)
warning: PrimeCert/Pocklington.lean:60:22: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3899/3938] Built LeanCert.Engine.RootFinding.Main (5.2s)
✔ [3900/3938] Built PrimeCert.Wieferich (5.7s)
✔ [3901/3947] Built PrimeCert.SmallPrimes (5.4s)
⚠ [3903/3951] Built PrimeCert.Pocklington3 (14s)
warning: PrimeCert/Pocklington3.lean:39:8: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3907/3960] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (10s)
✔ [3909/3960] Built LeanCert.Validity.Bounds (15s)
✔ [3911/3960] Built PrimeCert (3.4s)
✔ [3912/3960] Built LeanCert.Engine.Chebyshev.Theta (12s)
⚠ [3913/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (108s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:357: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:1737:8: declaration uses `sorry`
✔ [3914/3960] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (6.0s)
⚠ [3915/3960] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (9.5s)
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:73:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:90:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:297:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:679:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:717:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:739:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:763:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:814:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:984:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:999:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1011:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1029:6: declaration uses `sorry`
⚠ [3916/3960] Built PrimeNumberTheoremAnd.IEANTN.Mertens (25s)
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:263:0: ArithmeticFunction.vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, Λ i = log ↑n
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:853:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:857:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:867:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1237:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1270:8: declaration uses `sorry`
✔ [3917/3960] Built LeanCert.Tactic.IntervalAuto.OptBound (3.0s)
✔ [3918/3960] Built LeanCert.Tactic.IntervalAuto.Multivariate (5.1s)
✔ [3920/3960] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (29s)
✔ [3921/3960] Built LeanCert.Tactic.IntervalAuto.RootBound (2.6s)
✔ [3922/3960] Built LeanCert.Engine.ChebyshevTheta (2.3s)
✔ [3923/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (7.4s)
⚠ [3925/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (5.0s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:513:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:542:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:603:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:662:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:834:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:899:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1023:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1037:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1051:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1063:8: declaration uses `sorry`
✔ [3926/3960] Built PrimeNumberTheoremAnd.PerronFormula (10s)
⚠ [3927/3960] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (7.6s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:85:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:103:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:219:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:252:8: declaration uses `sorry`
✔ [3928/3960] Built LeanCert.Tactic.IntervalAuto.Bound (23s)
✔ [3929/3960] Built LeanCert.Tactic.IntervalAuto.Adaptive (6.5s)
✔ [3930/3960] Built LeanCert.Tactic.IntervalAuto.Subdiv (6.5s)
✔ [3931/3960] Built LeanCert.Tactic.IntervalAuto.PointIneq (11s)
✔ [3932/3960] Built LeanCert.Tactic.IntervalAuto (2.5s)
✔ [3933/3960] Built PrimeNumberTheoremAnd.IEANTN.LogTables (9.9s)
✔ [3934/3960] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (12s)
ℹ [3935/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (34s)
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.
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:88: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.
⚠ [3936/3960] Built LeanCert.Examples.BKLNW_a2_pow2 (36s)
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`
✔ [3937/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (4.5s)
✔ [3938/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (8.9s)
✔ [3939/3960] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (32s)
⚠ [3940/3960] Built PrimeNumberTheoremAnd.IEANTN.Buthe (20s)
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`
✔ [3941/3960] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (21s)
⚠ [3942/3960] Built LeanCert.Examples.BKLNW_a2_bounds (5.5s)
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`
⚠ [3943/3960] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (27s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3944/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.9s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [3945/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.7s)
✔ [3946/3960] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (97s)
⚠ [3947/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (5.1s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:398:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:668:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:721:8: declaration uses `sorry`
✔ [3948/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (139s)
⚠ [3949/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
✔ [3950/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (8.7s)
⚠ [3951/3960] Built PrimeNumberTheoremAnd.IEANTN.Dusart (24s)
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`
✔ [3952/3960] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (12s)
⚠ [3953/3960] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (55s)
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`
⚠ [3954/3960] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (19s)
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`
⚠ [3955/3960] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.9s)
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`
⚠ [3956/3960] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [3957/3960] Built PrimeNumberTheoremAnd.IEANTN.Lcm (38s)
✔ [3958/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (67s)
✔ [3959/3960] Built PrimeNumberTheoremAnd (2.6s)
Build completed successfully (3960 jobs).

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