Verification run

Run 4

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via manual

succeeded commit manual toolchain lean-v4-29-0 prover lean took 47m 38s · finished 6w 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 1s · created 6/2/2026, 11:30:08 AM

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

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

lake_cache exit 0 duration 1m 45s · created 6/2/2026, 11:30:08 AM

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.Init (307ms)
✔ [3/22] Built Cache.Lean (399ms)
✔ [4/22] Built Cache.Lean:c.o (337ms)
✔ [5/22] Built Cache.Init:c.o (400ms)
✔ [6/22] Built Cache.IO (1.4s)
✔ [7/22] Built Cache.Hashing (862ms)
✔ [8/22] Built Cache.IO:c.o (1.5s)
✔ [9/22] Built Cache.Hashing:c.o (584ms)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (132ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (219ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (259ms)
✔ [18/22] Built Cache.Requests (1.7s)
✔ [19/22] Built Cache.Main (674ms)
✔ [20/22] Built Cache.Main:c.o (490ms)
✔ [21/22] Built Cache.Requests:c.o (1.0s)
✔ [22/22] Built cache:exe (2.6s)
  % 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  2442k      0 --:--:-- --:--:-- --:--:-- 2442k


Downloaded: 1 file(s) [attempted 1/8232 = 0%, 8 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8232 = 0%, 4 KB/s], Decompressed: 14
Downloaded: 38 file(s) [attempted 38/8232 = 0%, 14 KB/s], Decompressed: 28
Downloaded: 64 file(s) [attempted 64/8232 = 0%, 273 KB/s], Decompressed: 57
Downloaded: 96 file(s) [attempted 96/8232 = 1%, 68 KB/s], Decompressed: 75
Downloaded: 131 file(s) [attempted 131/8232 = 1%, 79 KB/s], Decompressed: 100
Downloaded: 164 file(s) [attempted 164/8232 = 1%, 72 KB/s], Decompressed: 120
Downloaded: 203 file(s) [attempted 203/8232 = 2%, 297 KB/s], Decompressed: 120
Downloaded: 237 file(s) [attempted 237/8232 = 2%, 120 KB/s], Decompressed: 155
Downloaded: 278 file(s) [attempted 278/8232 = 3%, 44 KB/s], Decompressed: 155
Downloaded: 316 file(s) [attempted 316/8232 = 3%, 106 KB/s], Decompressed: 216
Downloaded: 357 file(s) [attempted 357/8232 = 4%, 28 KB/s], Decompressed: 216
Downloaded: 401 file(s) [attempted 401/8232 = 4%, 76 KB/s], Decompressed: 216
Downloaded: 443 file(s) [attempted 443/8232 = 5%, 76 KB/s], Decompressed: 216
Downloaded: 480 file(s) [attempted 480/8232 = 5%, 428 KB/s], Decompressed: 216
Downloaded: 514 file(s) [attempted 514/8232 = 6%, 239 KB/s], Decompressed: 312
Downloaded: 552 file(s) [attempted 552/8232 = 6%, 353 KB/s], Decompressed: 312
Downloaded: 600 file(s) [attempted 600/8232 = 7%, 745 KB/s], Decompressed: 312
Downloaded: 648 file(s) [attempted 648/8232 = 7%, 79 KB/s], Decompressed: 312
Downloaded: 693 file(s) [attempted 693/8232 = 8%, 123 KB/s], Decompressed: 312
Downloaded: 737 file(s) [attempted 737/8232 = 8%, 101 KB/s], Decompressed: 312
Downloaded: 775 file(s) [attempted 775/8232 = 9%, 137 KB/s], Decompressed: 484
Downloaded: 806 file(s) [attempted 806/8232 = 9%, 176 KB/s], Decompressed: 484
Downloaded: 850 file(s) [attempted 850/8232 = 10%, 265 KB/s], Decompressed: 484
Downloaded: 898 file(s) [attempted 898/8232 = 10%, 895 KB/s], Decompressed: 484
Downloaded: 946 file(s) [attempted 946/8232 = 11%, 172 KB/s], Decompressed: 484
Downloaded: 984 file(s) [attempted 984/8232 = 11%, 179 KB/s], Decompressed: 484
Downloaded: 1025 file(s) [attempted 1025/8232 = 12%, 511 KB/s], Decompressed: 484
Downloaded: 1066 file(s) [attempted 1066/8232 = 12%, 39 KB/s], Decompressed: 484
Downloaded: 1110 file(s) [attempted 1110/8232 = 13%, 367 KB/s], Decompressed: 484
Downloaded: 1158 file(s) [attempted 1158/8232 = 14%, 834 KB/s], Decompressed: 484
Downloaded: 1196 file(s) [attempted 1196/8232 = 14%, 397 KB/s], Decompressed: 751
Downloaded: 1237 file(s) [attempted 1237/8232 = 15%, 66 KB/s], Decompressed: 751
Downloaded: 1276 file(s) [attempted 1276/8232 = 15%, 322 KB/s], Decompressed: 751
Downloaded: 1312 file(s) [attempted 1312/8232 = 15%, 51 KB/s], Decompressed: 751
Downloaded: 1360 file(s) [attempted 1360/8232 = 16%, 187 KB/s], Decompressed: 751
Downloaded: 1405 file(s) [attempted 1405/8232 = 17%, 290 KB/s], Decompressed: 751
Downloaded: 1446 file(s) [attempted 1446/8232 = 17%, 204 KB/s], Decompressed: 751
Downloaded: 1483 file(s) [attempted 1483/8232 = 18%, 156 KB/s], Decompressed: 751
Downloaded: 1524 file(s) [attempted 1524/8232 = 18%, 170 KB/s], Decompressed: 751
Downloaded: 1562 file(s) [attempted 1562/8232 = 18%, 152 KB/s], Decompressed: 751
Downloaded: 1607 file(s) [attempted 1607/8232 = 19%, 497 KB/s], Decompressed: 751
Downloaded: 1648 file(s) [attempted 1648/8232 = 20%, 319 KB/s], Decompressed: 751
Downloaded: 1682 file(s) [attempted 1682/8232 = 20%, 210 KB/s], Decompressed: 751
Downloaded: 1726 file(s) [attempted 1726/8232 = 20%, 961 KB/s], Decompressed: 751
Downloaded: 1774 file(s) [attempted 1774/8232 = 21%, 183 KB/s], Decompressed: 1162
Downloaded: 1812 file(s) [attempted 1812/8232 = 22%, 107 KB/s], Decompressed: 1162
Downloaded: 1846 file(s) [attempted 1846/8232 = 22%, 97 KB/s], Decompressed: 1162
Downloaded: 1884 file(s) [attempted 1884/8232 = 22%, 768 KB/s], Decompressed: 1162
Downloaded: 1928 file(s) [attempted 1928/8232 = 23%, 870 KB/s], Decompressed: 1162
Downloaded: 1973 file(s) [attempted 1973/8232 = 23%, 62 KB/s], Decompressed: 1162
Downloaded: 2014 file(s) [attempted 2014/8232 = 24%, 37 KB/s], Decompressed: 1162
Downloaded: 2052 file(s) [attempted 2052/8232 = 24%, 256 KB/s], Decompressed: 1162
Downloaded: 2086 file(s) [attempted 2086/8232 = 25%, 1404 KB/s], Decompressed: 1162
Downloaded: 2124 file(s) [attempted 2124/8232 = 25%, 222 KB/s], Decompressed: 1162
Downloaded: 2168 file(s) [attempted 2168/8232 = 26%, 780 KB/s], Decompressed: 1162
Downloaded: 2209 file(s) [attempted 2209/8232 = 26%, 288 KB/s], Decompressed: 1162
Downloaded: 2247 file(s) [attempted 2247/8232 = 27%, 601 KB/s], Decompressed: 1162
Downloaded: 2284 file(s) [attempted 2284/8232 = 27%, 82 KB/s], Decompressed: 1162
Downloaded: 2329 file(s) [attempted 2329/8232 = 28%, 93 KB/s], Decompressed: 1162
Downloaded: 2370 file(s) [attempted 2370/8232 = 28%, 271 KB/s], Decompressed: 1162
Downloaded: 2411 file(s) [attempted 2411/8232 = 29%, 866 KB/s], Decompressed: 1162
Downloaded: 2452 file(s) [attempted 2452/8232 = 29%, 348 KB/s], Decompressed: 1162
Downloaded: 2490 file(s) [attempted 2490/8232 = 30%, 116 KB/s], Decompressed: 1162
Downloaded: 2534 file(s) [attempted 2534/8232 = 30%, 36 KB/s], Decompressed: 1162
Downloaded: 2575 file(s) [attempted 2575/8232 = 31%, 94 KB/s], Decompressed: 1764
Downloaded: 2616 file(s) [attempted 2616/8232 = 31%, 200 KB/s], Decompressed: 1764
Downloaded: 2661 file(s) [attempted 2661/8232 = 32%, 185 KB/s], Decompressed: 1764
Downloaded: 2695 file(s) [attempted 2695/8232 = 32%, 449 KB/s], Decompressed: 1764
Downloaded: 2739 file(s) [attempted 2739/8232 = 33%, 130 KB/s], Decompressed: 1764
Downloaded: 2787 file(s) [attempted 2787/8232 = 33%, 299 KB/s], Decompressed: 1764
Downloaded: 2828 file(s) [attempted 2828/8232 = 34%, 627 KB/s], Decompressed: 1764
Downloaded: 2866 file(s) [attempted 2866/8232 = 34%, 934 KB/s], Decompressed: 1764
Downloaded: 2907 file(s) [attempted 2907/8232 = 35%, 576 KB/s], Decompressed: 1764
Downloaded: 2948 file(s) [attempted 2948/8232 = 35%, 120 KB/s], Decompressed: 1764
Downloaded: 2986 file(s) [attempted 2986/8232 = 36%, 217 KB/s], Decompressed: 1764
Downloaded: 3030 file(s) [attempted 3030/8232 = 36%, 215 KB/s], Decompressed: 1764
Downloaded: 3068 file(s) [attempted 3068/8232 = 37%, 562 KB/s], Decompressed: 1764
Downloaded: 3106 file(s) [attempted 3106/8232 = 37%, 235 KB/s], Decompressed: 1764
Downloaded: 3147 file(s) [attempted 3147/8232 = 38%, 370 KB/s], Decompressed: 1764
Downloaded: 3195 file(s) [attempted 3195/8232 = 38%, 392 KB/s], Decompressed: 1764
Downloaded: 3235 file(s) [attempted 3235/8232 = 39%, 81 KB/s], Decompressed: 1764
Downloaded: 3273 file(s) [attempted 3273/8232 = 39%, 480 KB/s], Decompressed: 1764
Downloaded: 3314 file(s) [attempted 3314/8232 = 40%, 636 KB/s], Decompressed: 1764
Downloaded: 3355 file(s) [attempted 3355/8232 = 40%, 53 KB/s], Decompressed: 1764
Downloaded: 3397 file(s) [attempted 3397/8232 = 41%, 139 KB/s], Decompressed: 1764
Downloaded: 3441 file(s) [attempted 3441/8232 = 41%, 57 KB/s], Decompressed: 1764
Downloaded: 3475 file(s) [attempted 3475/8232 = 42%, 425 KB/s], Decompressed: 1764
Downloaded: 3520 file(s) [attempted 3520/8232 = 42%, 37 KB/s], Decompressed: 1764
Downloaded: 3561 file(s) [attempted 3561/8232 = 43%, 471 KB/s], Decompressed: 1764
Downloaded: 3598 file(s) [attempted 3598/8232 = 43%, 201 KB/s], Decompressed: 1764
Downloaded: 3640 file(s) [attempted 3640/8232 = 44%, 25 KB/s], Decompressed: 1764
Downloaded: 3677 file(s) [attempted 3677/8232 = 44%, 59 KB/s], Decompressed: 1764
Downloaded: 3718 file(s) [attempted 3718/8232 = 45%, 308 KB/s], Decompressed: 1764
Downloaded: 3759 file(s) [attempted 3759/8232 = 45%, 755 KB/s], Decompressed: 1764
Downloaded: 3807 file(s) [attempted 3807/8232 = 46%, 807 KB/s], Decompressed: 1764
Downloaded: 3855 file(s) [attempted 3855/8232 = 46%, 263 KB/s], Decompressed: 1764
Downloaded: 3889 file(s) [attempted 3889/8232 = 47%, 1636 KB/s], Decompressed: 2568
Downloaded: 3920 file(s) [attempted 3920/8232 = 47%, 471 KB/s], Decompressed: 2568
Downloaded: 3965 file(s) [attempted 3965/8232 = 48%, 245 KB/s], Decompressed: 2568
Downloaded: 4006 file(s) [attempted 4006/8232 = 48%, 97 KB/s], Decompressed: 2568
Downloaded: 4050 file(s) [attempted 4050/8232 = 49%, 107 KB/s], Decompressed: 2568
Downloaded: 4095 file(s) [attempted 4095/8232 = 49%, 398 KB/s], Decompressed: 2568
Downloaded: 4126 file(s) [attempted 4126/8232 = 50%, 222 KB/s], Decompressed: 2568
Downloaded: 4173 file(s) [attempted 4173/8232 = 50%, 97 KB/s], Decompressed: 2568
Downloaded: 4221 file(s) [attempted 4221/8232 = 51%, 828 KB/s], Decompressed: 2568
Downloaded: 4262 file(s) [attempted 4262/8232 = 51%, 94 KB/s], Decompressed: 2568
Downloaded: 4307 file(s) [attempted 4307/8232 = 52%, 110 KB/s], Decompressed: 2568
Downloaded: 4351 file(s) [attempted 4351/8232 = 52%, 918 KB/s], Decompressed: 2568
Downloaded: 4382 file(s) [attempted 4382/8232 = 53%, 360 KB/s], Decompressed: 2568
Downloaded: 4430 file(s) [attempted 4430/8232 = 53%, 198 KB/s], Decompressed: 2568
Downloaded: 4478 file(s) [attempted 4478/8232 = 54%, 481 KB/s], Decompressed: 2568
Downloaded: 4519 file(s) [attempted 4519/8232 = 54%, 136 KB/s], Decompressed: 2568
Downloaded: 4557 file(s) [attempted 4557/8232 = 55%, 53 KB/s], Decompressed: 2568
Downloaded: 4594 file(s) [attempted 4594/8232 = 55%, 295 KB/s], Decompressed: 2568
Downloaded: 4635 file(s) [attempted 4635/8232 = 56%, 245 KB/s], Decompressed: 2568
Downloaded: 4677 file(s) [attempted 4677/8232 = 56%, 217 KB/s], Decompressed: 2568
Downloaded: 4718 file(s) [attempted 4718/8232 = 57%, 39 KB/s], Decompressed: 2568
Downloaded: 4762 file(s) [attempted 4762/8232 = 57%, 186 KB/s], Decompressed: 2568
Downloaded: 4800 file(s) [attempted 4800/8232 = 58%, 48 KB/s], Decompressed: 2568
Downloaded: 4837 file(s) [attempted 4837/8232 = 58%, 133 KB/s], Decompressed: 2568
Downloaded: 4878 file(s) [attempted 4878/8232 = 59%, 455 KB/s], Decompressed: 2568
Downloaded: 4920 file(s) [attempted 4920/8232 = 59%, 385 KB/s], Decompressed: 2568
Downloaded: 4967 file(s) [attempted 4967/8232 = 60%, 815 KB/s], Decompressed: 2568
Downloaded: 5014 file(s) [attempted 5014/8232 = 60%, 258 KB/s], Decompressed: 2568
Downloaded: 5046 file(s) [attempted 5046/8232 = 61%, 154 KB/s], Decompressed: 2568
Downloaded: 5091 file(s) [attempted 5091/8232 = 61%, 57 KB/s], Decompressed: 2568
Downloaded: 5128 file(s) [attempted 5128/8232 = 62%, 34 KB/s], Decompressed: 2568
Downloaded: 5169 file(s) [attempted 5169/8232 = 62%, 502 KB/s], Decompressed: 2568
Downloaded: 5214 file(s) [attempted 5214/8232 = 63%, 571 KB/s], Decompressed: 2568
Downloaded: 5258 file(s) [attempted 5258/8232 = 63%, 180 KB/s], Decompressed: 2568
Downloaded: 5297 file(s) [attempted 5297/8232 = 64%, 154 KB/s], Decompressed: 2568
Downloaded: 5337 file(s) [attempted 5337/8232 = 64%, 265 KB/s], Decompressed: 2568
Downloaded: 5382 file(s) [attempted 5382/8232 = 65%, 191 KB/s], Decompressed: 2568
Downloaded: 5419 file(s) [attempted 5419/8232 = 65%, 468 KB/s], Decompressed: 2568
Downloaded: 5457 file(s) [attempted 5457/8232 = 66%, 229 KB/s], Decompressed: 2568
Downloaded: 5498 file(s) [attempted 5498/8232 = 66%, 44 KB/s], Decompressed: 2568
Downloaded: 5539 file(s) [attempted 5539/8232 = 67%, 226 KB/s], Decompressed: 2568
Downloaded: 5583 file(s) [attempted 5583/8232 = 67%, 144 KB/s], Decompressed: 2568
Downloaded: 5628 file(s) [attempted 5628/8232 = 68%, 115 KB/s], Decompressed: 2568
Downloaded: 5669 file(s) [attempted 5669/8232 = 68%, 516 KB/s], Decompressed: 2568
Downloaded: 5707 file(s) [attempted 5707/8232 = 69%, 87 KB/s], Decompressed: 2568
Downloaded: 5744 file(s) [attempted 5744/8232 = 69%, 292 KB/s], Decompressed: 2568
Downloaded: 5789 file(s) [attempted 5789/8232 = 70%, 527 KB/s], Decompressed: 3859
Downloaded: 5830 file(s) [attempted 5830/8232 = 70%, 411 KB/s], Decompressed: 3859
Downloaded: 5874 file(s) [attempted 5874/8232 = 71%, 851 KB/s], Decompressed: 3859
Downloaded: 5898 file(s) [attempted 5898/8232 = 71%, 333 KB/s], Decompressed: 3859
Downloaded: 5943 file(s) [attempted 5943/8232 = 72%, 313 KB/s], Decompressed: 3859
Downloaded: 5987 file(s) [attempted 5987/8232 = 72%, 222 KB/s], Decompressed: 3859
Downloaded: 6035 file(s) [attempted 6035/8232 = 73%, 43 KB/s], Decompressed: 3859
Downloaded: 6083 file(s) [attempted 6083/8232 = 73%, 237 KB/s], Decompressed: 3859
Downloaded: 6128 file(s) [attempted 6128/8232 = 74%, 123 KB/s], Decompressed: 3859
Downloaded: 6158 file(s) [attempted 6158/8232 = 74%, 395 KB/s], Decompressed: 3859
Downloaded: 6205 file(s) [attempted 6205/8232 = 75%, 683 KB/s], Decompressed: 3859
Downloaded: 6241 file(s) [attempted 6241/8232 = 75%, 153 KB/s], Decompressed: 3859
Downloaded: 6285 file(s) [attempted 6285/8232 = 76%, 241 KB/s], Decompressed: 3859
Downloaded: 6326 file(s) [attempted 6326/8232 = 76%, 65 KB/s], Decompressed: 3859
Downloaded: 6364 file(s) [attempted 6364/8232 = 77%, 444 KB/s], Decompressed: 3859
Downloaded: 6405 file(s) [attempted 6405/8232 = 77%, 75 KB/s], Decompressed: 3859
Downloaded: 6449 file(s) [attempted 6449/8232 = 78%, 865 KB/s], Decompressed: 3859
Downloaded: 6494 file(s) [attempted 6494/8232 = 78%, 331 KB/s], Decompressed: 3859
Downloaded: 6535 file(s) [attempted 6535/8232 = 79%, 431 KB/s], Decompressed: 3859
Downloaded: 6566 file(s) [attempted 6566/8232 = 79%, 171 KB/s], Decompressed: 3859
Downloaded: 6610 file(s) [attempted 6610/8232 = 80%, 32 KB/s], Decompressed: 3859
Downloaded: 6655 file(s) [attempted 6655/8232 = 80%, 254 KB/s], Decompressed: 3859
Downloaded: 6696 file(s) [attempted 6696/8232 = 81%, 102 KB/s], Decompressed: 3859
Downloaded: 6737 file(s) [attempted 6737/8232 = 81%, 299 KB/s], Decompressed: 3859
Downloaded: 6771 file(s) [attempted 6771/8232 = 82%, 109 KB/s], Decompressed: 3859
Downloaded: 6812 file(s) [attempted 6812/8232 = 82%, 35 KB/s], Decompressed: 3859
Downloaded: 6860 file(s) [attempted 6860/8232 = 83%, 148 KB/s], Decompressed: 3859
Downloaded: 6908 file(s) [attempted 6908/8232 = 83%, 97 KB/s], Decompressed: 3859
Downloaded: 6949 file(s) [attempted 6949/8232 = 84%, 76 KB/s], Decompressed: 3859
Downloaded: 6989 file(s) [attempted 6989/8232 = 84%, 30 KB/s], Decompressed: 3859
Downloaded: 7024 file(s) [attempted 7024/8232 = 85%, 165 KB/s], Decompressed: 3859
Downloaded: 7065 file(s) [attempted 7065/8232 = 85%, 36 KB/s], Decompressed: 3859
Downloaded: 7110 file(s) [attempted 7110/8232 = 86%, 269 KB/s], Decompressed: 3859
Downloaded: 7151 file(s) [attempted 7151/8232 = 86%, 546 KB/s], Decompressed: 3859
Downloaded: 7185 file(s) [attempted 7185/8232 = 87%, 301 KB/s], Decompressed: 3859
Downloaded: 7230 file(s) [attempted 7230/8232 = 87%, 373 KB/s], Decompressed: 3859
Downloaded: 7267 file(s) [attempted 7267/8232 = 88%, 961 KB/s], Decompressed: 3859
Downloaded: 7308 file(s) [attempted 7308/8232 = 88%, 235 KB/s], Decompressed: 3859
Downloaded: 7356 file(s) [attempted 7356/8232 = 89%, 108 KB/s], Decompressed: 3859
Downloaded: 7397 file(s) [attempted 7397/8232 = 89%, 163 KB/s], Decompressed: 3859
Downloaded: 7438 file(s) [attempted 7438/8232 = 90%, 147 KB/s], Decompressed: 3859
Downloaded: 7480 file(s) [attempted 7480/8232 = 90%, 224 KB/s], Decompressed: 3859
Downloaded: 7517 file(s) [attempted 7517/8232 = 91%, 2571 KB/s], Decompressed: 3859
Downloaded: 7565 file(s) [attempted 7565/8232 = 91%, 81 KB/s], Decompressed: 3859
Downloaded: 7604 file(s) [attempted 7604/8232 = 92%, 284 KB/s], Decompressed: 3859
Downloaded: 7647 file(s) [attempted 7647/8232 = 92%, 433 KB/s], Decompressed: 3859
Downloaded: 7685 file(s) [attempted 7685/8232 = 93%, 384 KB/s], Decompressed: 3859
Downloaded: 7729 file(s) [attempted 7729/8232 = 93%, 37 KB/s], Decompressed: 3859
Downloaded: 7764 file(s) [attempted 7764/8232 = 94%, 140 KB/s], Decompressed: 3859
Downloaded: 7805 file(s) [attempted 7805/8232 = 94%, 183 KB/s], Decompressed: 3859
Downloaded: 7846 file(s) [attempted 7846/8232 = 95%, 241 KB/s], Decompressed: 3859
Downloaded: 7890 file(s) [attempted 7890/8232 = 95%, 2450 KB/s], Decompressed: 3859
Downloaded: 7931 file(s) [attempted 7931/8232 = 96%, 395 KB/s], Decompressed: 3859
Downloaded: 7976 file(s) [attempted 7976/8232 = 96%, 327 KB/s], Decompressed: 3859
Downloaded: 8007 file(s) [attempted 8007/8232 = 97%, 522 KB/s], Decompressed: 3859
Downloaded: 8051 file(s) [attempted 8051/8232 = 97%, 83 KB/s], Decompressed: 3859
Downloaded: 8094 file(s) [attempted 8094/8232 = 98%, 390 KB/s], Decompressed: 3859
Downloaded: 8137 file(s) [attempted 8137/8232 = 98%, 365 KB/s], Decompressed: 3859
Downloaded: 8178 file(s) [attempted 8178/8232 = 99%, 310 KB/s], Decompressed: 3859
Downloaded: 8208 file(s) [attempted 8208/8232 = 99%, 712 KB/s], Decompressed: 3859
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 85 KB/s], Decompressed: 3859
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 85 KB/s], Decompressed: 3859

lean_checker exit 0 duration 21m 58s · created 6/2/2026, 11:30:08 AM

lake build

✔ [2765/2799] Built Architect.Command (5.2s)
✔ [2809/2831] Built Architect.Basic (5.7s)
✔ [2812/2835] Built Architect.Tactic (2.8s)
✔ [2813/2835] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (5.2s)
✔ [2814/2838] Built PrimeNumberTheoremAnd.Auxiliary (11s)
✔ [2820/2844] Built Architect.CollectUsed (2.8s)
✔ [3039/3070] Built Architect.Content (2.4s)
✔ [3057/3075] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (5.1s)
✔ [3123/3164] Built Architect.Attribute (3.9s)
✔ [3124/3164] Built Architect.Output (3.8s)
✔ [3440/3464] Built Architect.Load (1.7s)
✔ [3443/3468] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (2.4s)
✔ [3445/3468] Built Architect (1.6s)
✔ [3448/3468] Built PrimeNumberTheoremAnd.Sobolev (18s)
✔ [3449/3468] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (4.3s)
✔ [3450/3468] Built PrimeNumberTheoremAnd.ZetaConj (8.1s)
✔ [3451/3472] Built PrimeNumberTheoremAnd.SmoothExistence (8.6s)
✔ [3454/3473] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (9.8s)
✔ [3457/3474] Built PrimeNumberTheoremAnd.Rectangle (8.9s)
✔ [3460/3474] Built PrimeNumberTheoremAnd.Fourier (7.7s)
✔ [3463/3474] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (9.8s)
✔ [3464/3493] Built PrimeNumberTheoremAnd.Defs (17s)
✔ [3582/3606] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (25s)
✔ [3583/3612] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (17s)
✔ [3586/3612] Built PrimeNumberTheoremAnd.MellinCalculus (29s)
✔ [3587/3612] Built PrimeNumberTheoremAnd.HadamardFactorization (4.6s)
✔ [3589/3613] Built PrimeNumberTheoremAnd.HoffsteinLockhart (5.2s)
✔ [3594/3614] Built PrimeNumberTheoremAnd.GeneralMeromorphic (4.2s)
✔ [3597/3617] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (7.7s)
✔ [3601/3617] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (9.2s)
⚠ [3603/3617] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (13s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3604/3619] Built PrimeNumberTheoremAnd.BrunTitchmarsh (23s)
✔ [3608/3630] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (37s)
✔ [3656/3685] Built PrimeNumberTheoremAnd.IEANTN.KLN (15s)
✔ [3665/3686] Built LeanCert.Core.Interval (9.5s)
✔ [3666/3686] Built LeanCert.Core.Expr (14s)
✔ [3667/3687] Built LeanCert.Core.Support (12s)
✔ [3668/3687] Built LeanCert.Core.IntervalRat.Basic (29s)
✔ [3669/3687] Built LeanCert.Meta.Numeral (11s)
✔ [3670/3688] Built LeanCert.Tactic.IntervalAuto.Types (10s)
✔ [3671/3688] Built LeanCert.Core.IntervalRat.Transcendental (14s)
✔ [3672/3688] Built PrimeNumberTheoremAnd.ZetaBounds (97s)
✔ [3673/3688] Built LeanCert.Tactic.IntervalAuto.Extract (11s)
✔ [3674/3693] Built LeanCert.Meta.ToExpr (11s)
✔ [3675/3693] Built LeanCert.Tactic.IntervalAuto.Norm (10s)
✔ [3676/3693] Built LeanCert.Core.IntervalRat.LogReduction (12s)
✔ [3677/3693] Built LeanCert.Tactic.IntervalAuto.Parse (18s)
⚠ [3679/3694] Built PrimeNumberTheoremAnd.Wiener (126s)
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
✔ [3680/3697] Built LeanCert.Core.DerivativeIntervals (38s)
✔ [3681/3697] Built LeanCert.Tactic.IntervalAuto.Diagnostic (16s)
✔ [3682/3699] Built LeanCert.Core.Taylor (27s)
✔ [3683/3700] Built LeanCert.Core.IntervalRat.Taylor (101s)
ℹ [3684/3700] Built PrimeNumberTheoremAnd.MediumPNT (205s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3685/3701] Built PrimeNumberTheoremAnd.Consequences (155s)
⚠ [3686/3703] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (221s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3687/3703] Built LeanCert.Core.IntervalReal (18s)
✔ [3688/3710] Built LeanCert.Core.IntervalRat.TrigReduced (29s)
⚠ [3689/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (6.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/3710] Built LeanCert.Core.IntervalRealEndpoints (9.2s)
✔ [3691/3710] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (8.7s)
✔ [3702/3737] Built LeanCert.Contrib.Sinc (11s)
✔ [3703/3737] Built LeanCert.Core.Dyadic (10s)
✔ [3704/3740] Built LeanCert.Engine.Eval.Core (21s)
✔ [3705/3740] Built LeanCert.Engine.Affine.Basic (19s)
✔ [3706/3741] Built LeanCert.Engine.Eval.Extended (11s)
✔ [3707/3771] Built LeanCert.Core.IntervalDyadic (21s)
✔ [3709/3772] Built LeanCert.Engine.Affine.Nonlinear (10s)
✔ [3710/3773] Built LeanCert.Tactic.Bound.Lemmas (5.0s)
⚠ [3712/3774] Built PrimeNumberTheoremAnd.StrongPNT (55s)
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`
✔ [3714/3774] Built LeanCert.Engine.IntervalEval (7.0s)
✔ [3716/3774] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (15s)
✔ [3717/3774] Built LeanCert.Engine.Affine.Transcendental (7.6s)
✔ [3718/3774] Built PrimeNumberTheoremAnd.BorelCaratheodory (15s)
✔ [3719/3774] Built LeanCert.Engine.Integrate (10s)
✔ [3720/3774] Built LeanCert.Engine.IntervalEvalDyadic (5.0s)
✔ [3721/3774] Built LeanCert.Engine.RootFinding.Basic (7.8s)
✔ [3722/3776] Built LeanCert.Engine.Optimization.Box (5.6s)
✔ [3723/3776] Built LeanCert.Engine.AD.Basic (6.0s)
✔ [3724/3776] Built LeanCert.Engine.IntervalEvalAffine (8.4s)
✔ [3725/3776] Built LeanCert.Engine.TaylorModel.Core (13s)
✔ [3726/3776] Built LeanCert.Validity.DyadicBounds (5.6s)
⚠ [3728/3778] Built PrimeNumberTheoremAnd.DerivativeBound (9.6s)
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
✔ [3729/3778] Built LeanCert.Engine.RootFinding.Bisection (7.0s)
✔ [3730/3778] Built LeanCert.Engine.TaylorModel.Special (6.1s)
✔ [3731/3778] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (52s)
✔ [3732/3778] Built LeanCert.Engine.AD.Transcendental (8.8s)
✔ [3733/3782] Built LeanCert.Engine.TaylorModel.Log1p (11s)
✔ [3736/3782] Built LeanCert.Engine.TaylorModel.ExpLog (20s)
✔ [3737/3782] Built LeanCert.Engine.TaylorModel.Trig (21s)
✔ [3738/3784] Built LeanCert.Engine.TaylorModel.Hyperbolic (25s)
✔ [3741/3785] Built LeanCert.Engine.AD.Eval (5.8s)
⚠ [3745/3786] Built LeanCert.Examples.Li2Bounds (6.1s)
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3749/3786] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (25s)
✔ [3787/3842] Built LeanCert.Engine.TaylorModel.Functions (4.7s)
✔ [3854/3898] Built LeanCert.Engine.AD.Correctness (6.2s)
✔ [3855/3900] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (6.7s)
✔ [3856/3901] Built LeanCert.Engine.TaylorModel.Expr (9.5s)
✔ [3857/3901] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (7.6s)
✔ [3858/3901] Built LeanCert.Tactic.VecUtil (4.8s)
✔ [3859/3901] Built LeanCert.Engine.TaylorModel (8.7s)
✔ [3861/3914] Built LeanCert.Engine.AD.Computable (10s)
✔ [3866/3914] Built LeanCert.Tactic.FinSumExpand (5.7s)
✔ [3867/3914] Built LeanCert.Engine.AD.PartialCorrectness (15s)
✔ [3868/3916] Built LeanCert.Engine.Chebyshev.Psi (7.0s)
✔ [3869/3916] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (6.6s)
✔ [3870/3916] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (37s)
✔ [3871/3921] Built LeanCert.Engine.AD (6.3s)
✔ [3873/3921] Built LeanCert.Engine.ChebyshevPsi (6.6s)
✔ [3874/3921] Built LeanCert.Meta.ProveSupported (8.8s)
✔ [3875/3921] Built LeanCert.Engine.IntervalEvalRefined (12s)
✔ [3878/3923] Built PrimeNumberTheoremAnd.Tactic.Simprocs (8.3s)
✔ [3880/3923] Built LeanCert.Engine.Optimize (19s)
✔ [3881/3923] Built LeanCert.Meta.ProveContinuous (10s)
✔ [3882/3924] Built PrimeCert.Interval (7.9s)
✔ [3883/3924] Built LeanCert.Tactic.IntervalAuto.ProveCommon (13s)
✔ [3884/3924] Built PrimeCert.Meta.PrimeCert (5.6s)
✔ [3885/3925] Built LeanCert.Engine.Optimization.Gradient (15s)
✔ [3886/3925] Built LeanCert.Engine.RootFinding.Newton (13s)
✔ [3887/3925] Built PrimeCert.Meta.SmallPrime (4.7s)
✔ [3888/3926] Built LeanCert.Tactic.IntervalAuto.Basic (6.9s)
✔ [3889/3927] Built PrimeCert.PredMod (1.2s)
✔ [3890/3927] Built LeanCert.Engine.RootFinding.MVTBounds (26s)
✔ [3891/3929] Built PrimeCert.PowMod (13s)
⚠ [3893/3938] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (108s)
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`
✔ [3895/3938] Built LeanCert.Engine.Optimization.Global (48s)
✔ [3896/3938] Built PrimeCert.Wieferich (8.0s)
⚠ [3897/3938] Built PrimeCert.Pocklington (13s)
warning: PrimeCert/Pocklington.lean:60:22: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3898/3938] Built LeanCert.Engine.RootFinding.Contraction (23s)
✔ [3899/3943] Built PrimeCert.SmallPrimes (7.0s)
✔ [3900/3948] Built LeanCert.Engine.Optimization.BoundVerify (11s)
✔ [3902/3951] Built LeanCert.Engine.RootFinding.Main (5.1s)
✔ [3905/3951] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (16s)
⚠ [3908/3960] Built PrimeCert.Pocklington3 (19s)
warning: PrimeCert/Pocklington3.lean:39:8: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3910/3960] Built LeanCert.Validity.Bounds (18s)
⚠ [3911/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (173s)
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`
⚠ [3912/3960] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (15s)
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`
✔ [3913/3960] Built LeanCert.Engine.Chebyshev.Theta (27s)
✔ [3915/3960] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (13s)
✔ [3916/3960] Built PrimeCert (7.8s)
⚠ [3917/3960] Built PrimeNumberTheoremAnd.IEANTN.Mertens (45s)
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`
✔ [3918/3960] Built LeanCert.Tactic.IntervalAuto.OptBound (4.0s)
✔ [3919/3960] Built LeanCert.Tactic.IntervalAuto.Multivariate (10s)
✔ [3920/3960] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (50s)
✔ [3921/3960] Built LeanCert.Engine.ChebyshevTheta (3.9s)
✔ [3922/3960] Built LeanCert.Tactic.IntervalAuto.RootBound (5.1s)
⚠ [3924/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (15s)
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`
✔ [3925/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (17s)
✔ [3926/3960] Built PrimeNumberTheoremAnd.PerronFormula (17s)
✔ [3927/3960] Built LeanCert.Tactic.IntervalAuto.Bound (43s)
⚠ [3928/3960] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (15s)
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`
✔ [3929/3960] Built LeanCert.Tactic.IntervalAuto.Adaptive (10s)
✔ [3930/3960] Built LeanCert.Tactic.IntervalAuto.Subdiv (11s)
✔ [3931/3960] Built LeanCert.Tactic.IntervalAuto.PointIneq (16s)
✔ [3932/3960] Built LeanCert.Tactic.IntervalAuto (2.7s)
✔ [3933/3960] Built PrimeNumberTheoremAnd.IEANTN.LogTables (17s)
✔ [3934/3960] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (27s)
⚠ [3935/3960] Built LeanCert.Examples.BKLNW_a2_pow2 (67s)
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`
ℹ [3936/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (69s)
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.
✔ [3937/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (36s)
✔ [3938/3960] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (79s)
✔ [3939/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (60s)
✔ [3940/3960] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (153s)
✔ [3941/3960] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (36s)
⚠ [3942/3960] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (48s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3943/3960] Built PrimeNumberTheoremAnd.IEANTN.Buthe (64s)
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`
⚠ [3944/3960] Built LeanCert.Examples.BKLNW_a2_bounds (23s)
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`
⚠ [3945/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (18s)
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`
✔ [3946/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (5.7s)
⚠ [3947/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (8.9s)
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 (228s)
⚠ [3949/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (38s)
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 (16s)
⚠ [3951/3960] Built PrimeNumberTheoremAnd.IEANTN.Dusart (46s)
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 (34s)
⚠ [3953/3960] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (93s)
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 (26s)
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 (10s)
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 (22s)
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 (58s)
✔ [3958/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (91s)
✔ [3959/3960] Built PrimeNumberTheoremAnd (7.9s)
Build completed successfully (3960 jobs).

blueprint_build exit 0 duration 7m 34s · created 6/2/2026, 11:30:08 AM

lake build :blueprint

✔ [10/35] Built Architect.Command:c.o (522ms)
✔ [11/35] Built Batteries.Lean.NameMapAttribute:c.o (692ms)
✔ [12/35] Built Architect.Basic:c.o (849ms)
✔ [15/35] Built Architect.CollectUsed:c.o (221ms)
✔ [16/35] Built Architect.Tactic:c.o (455ms)
✔ [18/35] Built Architect.Content:c.o (265ms)
✔ [23/35] Built Architect.Load:c.o (290ms)
✔ [25/35] Built Architect:c.o (161ms)
✔ [27/35] Built Cli.Extensions:c.o (1.2s)
✔ [28/42] Built Architect.Attribute:c.o (1.0s)
✔ [29/42] Built Cli:c.o (68ms)
✔ [34/83] Built Architect.Output:c.o (2.1s)
✔ [1209/1269] Built Main (2.2s)
✔ [1441/1515] Built Main:c.o (483ms)
✔ [2687/2817] Built Cli.Basic:c.o (5.2s)
ℹ [3457/3586] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3475/3586] Replayed PrimeNumberTheoremAnd.StrongPNT
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`
⚠ [3616/3743] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
⚠ [3618/3743] Replayed PrimeNumberTheoremAnd.DerivativeBound
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
⚠ [3630/3743] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3696/3867] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3697/3867] 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`
⚠ [3781/3867] 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: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`
⚠ [3783/3867] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3909/4060] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3911/4060] 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`
⚠ [3912/4060] 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: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`
⚠ [3914/4060] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
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`
⚠ [3917/4060] 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`
⚠ [3918/4060] 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`
⚠ [3925/4060] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
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`
⚠ [3926/4060] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
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`
⚠ [3932/4060] 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`
⚠ [3933/4060] 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`
⚠ [3938/4060] 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`
⚠ [3948/4060] Replayed PrimeCert.Pocklington
warning: PrimeCert/Pocklington.lean:60:22: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
⚠ [3949/4060] Replayed PrimeCert.Pocklington3
warning: PrimeCert/Pocklington3.lean:39:8: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
⚠ [3955/4060] 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`
⚠ [3956/4060] 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`
⚠ [3957/4060] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [3964/4060] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
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`
ℹ [3970/4060] 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.
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.
⚠ [3971/4060] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
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`
⚠ [3975/4060] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
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`
✔ [3979/4060] Built extract_blueprint:exe (2.9s)
✔ [3980/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (4.4s)
✔ [3981/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (3.9s)
✔ [3982/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (4.9s)
✔ [3983/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (3.4s)
✔ [3984/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (4.6s)
✔ [3985/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (2.7s)
✔ [3986/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (22s)
✔ [3987/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (21s)
✔ [3988/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (2.2s)
✔ [3989/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (10s)
✔ [3990/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (92s)
✔ [3991/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (13s)
✔ [3992/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (3.1s)
✔ [3993/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (3.0s)
✔ [3994/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (4.1s)
✔ [3995/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (4.0s)
✔ [3996/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (3.6s)
✔ [3997/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (4.9s)
✔ [3998/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (14s)
✔ [3999/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (65s)
✔ [4000/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (28s)
✔ [4001/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.DerivativeBound:blueprint (7.2s)
✔ [4002/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (4.4s)
✔ [4003/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (5.0s)
✔ [4004/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (2.0s)
✔ [4005/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (4.5s)
✔ [4006/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (18s)
✔ [4007/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (5.2s)
✔ [4008/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (5.1s)
✔ [4009/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (48s)
✔ [4010/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (5.6s)
✔ [4011/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (4.7s)
✔ [4012/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (4.1s)
✔ [4013/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (4.7s)
✔ [4014/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (32s)
✔ [4015/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (10s)
✔ [4016/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (4.1s)
✔ [4017/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (3.7s)
✔ [4018/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (4.2s)
✔ [4019/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (18s)
✔ [4020/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (13s)
✔ [4021/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (4.7s)
✔ [4022/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (35s)
✔ [4023/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (6.6s)
✔ [4024/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (10s)
✔ [4025/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (31s)
✔ [4026/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (8.0s)
✔ [4027/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (47s)
✔ [4028/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (11s)
✔ [4029/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (99s)
✔ [4030/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (30s)
✔ [4031/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (34s)
✔ [4032/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (12s)
✔ [4033/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (4.6s)
✔ [4034/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (9.7s)
✔ [4035/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (33s)
✔ [4036/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (30s)
✔ [4037/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (58s)
✔ [4038/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (2.8s)
✔ [4039/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (3.9s)
✔ [4040/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (4.8s)
✔ [4041/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (80s)
✔ [4042/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (12s)
✔ [4043/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (14s)
✔ [4044/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (18s)
✔ [4045/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (6.0s)
✔ [4046/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (20s)
✔ [4047/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (57s)
✔ [4048/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (19s)
✔ [4049/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (7.1s)
✔ [4050/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (17s)
✔ [4051/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (34s)
✔ [4052/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (81s)
✔ [4053/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (18s)
✔ [4054/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (51s)
✔ [4055/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (18s)
✔ [4056/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (102s)
✔ [4057/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (29s)
✔ [4058/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (93s)
ℹ [4059/4061] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (79ms)
info: Blueprint indexing
Build completed successfully (4061 jobs).

semantic_extract exit 0 duration 15m 5s · created 6/2/2026, 11:30:08 AM

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