Verification run

Run 5

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via manual

succeeded commit manual toolchain lean-v4-29-0 prover lean took 36m 40s · 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 746 ms · created 6/2/2026, 1:50:33 PM

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

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

lake_cache exit 0 duration 1m 37s · created 6/2/2026, 1:50:33 PM

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 (475ms)
✔ [3/22] Built Cache.Init (397ms)
✔ [4/22] Built Cache.Init:c.o (381ms)
✔ [5/22] Built Cache.Lean:c.o (338ms)
✔ [6/22] Built Cache.IO (1.5s)
✔ [7/22] Built Cache.Hashing (741ms)
✔ [8/22] Built Cache.Hashing:c.o (407ms)
✔ [9/22] Built Cache.IO:c.o (1.4s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (94ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (228ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (207ms)
✔ [18/22] Built Cache.Requests (1.9s)
✔ [19/22] Built Cache.Main (882ms)
✔ [20/22] Built Cache.Main:c.o (495ms)
✔ [21/22] Built Cache.Requests:c.o (2.2s)
✔ [22/22] Built cache:exe (2.5s)
  % 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  3276k      0 --:--:-- --:--:-- --:--:-- 3276k


Downloaded: 1 file(s) [attempted 1/8232 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 14 file(s) [attempted 14/8232 = 0%, 8 KB/s], Decompressed: 13
Downloaded: 39 file(s) [attempted 39/8232 = 0%, 15 KB/s], Decompressed: 34
Downloaded: 69 file(s) [attempted 69/8232 = 0%, 255 KB/s], Decompressed: 61
Downloaded: 96 file(s) [attempted 96/8232 = 1%, 66 KB/s], Decompressed: 79
Downloaded: 131 file(s) [attempted 131/8232 = 1%, 15 KB/s], Decompressed: 103
Downloaded: 161 file(s) [attempted 161/8232 = 1%, 292 KB/s], Decompressed: 137
Downloaded: 203 file(s) [attempted 203/8232 = 2%, 438 KB/s], Decompressed: 155
Downloaded: 237 file(s) [attempted 237/8232 = 2%, 24 KB/s], Decompressed: 182
Downloaded: 278 file(s) [attempted 278/8232 = 3%, 908 KB/s], Decompressed: 206
Downloaded: 319 file(s) [attempted 319/8232 = 3%, 367 KB/s], Decompressed: 240
Downloaded: 353 file(s) [attempted 353/8232 = 4%, 82 KB/s], Decompressed: 282
Downloaded: 395 file(s) [attempted 395/8232 = 4%, 135 KB/s], Decompressed: 329
Downloaded: 439 file(s) [attempted 439/8232 = 5%, 277 KB/s], Decompressed: 388
Downloaded: 480 file(s) [attempted 480/8232 = 5%, 1396 KB/s], Decompressed: 388
Downloaded: 521 file(s) [attempted 521/8232 = 6%, 447 KB/s], Decompressed: 439
Downloaded: 557 file(s) [attempted 557/8232 = 6%, 66 KB/s], Decompressed: 439
Downloaded: 593 file(s) [attempted 593/8232 = 7%, 67 KB/s], Decompressed: 497
Downloaded: 634 file(s) [attempted 634/8232 = 7%, 130 KB/s], Decompressed: 497
Downloaded: 682 file(s) [attempted 682/8232 = 8%, 150 KB/s], Decompressed: 569
Downloaded: 727 file(s) [attempted 727/8232 = 8%, 50 KB/s], Decompressed: 569
Downloaded: 765 file(s) [attempted 765/8232 = 9%, 64 KB/s], Decompressed: 569
Downloaded: 795 file(s) [attempted 795/8232 = 9%, 84 KB/s], Decompressed: 675
Downloaded: 840 file(s) [attempted 840/8232 = 10%, 116 KB/s], Decompressed: 675
Downloaded: 884 file(s) [attempted 884/8232 = 10%, 27 KB/s], Decompressed: 771
Downloaded: 929 file(s) [attempted 929/8232 = 11%, 195 KB/s], Decompressed: 771
Downloaded: 970 file(s) [attempted 970/8232 = 11%, 240 KB/s], Decompressed: 771
Downloaded: 1001 file(s) [attempted 1001/8232 = 12%, 152 KB/s], Decompressed: 874
Downloaded: 1042 file(s) [attempted 1042/8232 = 12%, 672 KB/s], Decompressed: 874
Downloaded: 1086 file(s) [attempted 1086/8232 = 13%, 58 KB/s], Decompressed: 874
Downloaded: 1128 file(s) [attempted 1128/8232 = 13%, 128 KB/s], Decompressed: 984
Downloaded: 1169 file(s) [attempted 1169/8232 = 14%, 168 KB/s], Decompressed: 984
Downloaded: 1206 file(s) [attempted 1206/8232 = 14%, 294 KB/s], Decompressed: 1093
Downloaded: 1247 file(s) [attempted 1247/8232 = 15%, 86 KB/s], Decompressed: 1093
Downloaded: 1292 file(s) [attempted 1292/8232 = 15%, 101 KB/s], Decompressed: 1093
Downloaded: 1336 file(s) [attempted 1336/8232 = 16%, 142 KB/s], Decompressed: 1206
Downloaded: 1374 file(s) [attempted 1374/8232 = 16%, 370 KB/s], Decompressed: 1206
Downloaded: 1415 file(s) [attempted 1415/8232 = 17%, 53 KB/s], Decompressed: 1206
Downloaded: 1449 file(s) [attempted 1449/8232 = 17%, 101 KB/s], Decompressed: 1206
Downloaded: 1490 file(s) [attempted 1490/8232 = 18%, 47 KB/s], Decompressed: 1326
Downloaded: 1535 file(s) [attempted 1535/8232 = 18%, 57 KB/s], Decompressed: 1326
Downloaded: 1576 file(s) [attempted 1576/8232 = 19%, 93 KB/s], Decompressed: 1326
Downloaded: 1624 file(s) [attempted 1624/8232 = 19%, 3299 KB/s], Decompressed: 1466
Downloaded: 1672 file(s) [attempted 1672/8232 = 20%, 122 KB/s], Decompressed: 1466
Downloaded: 1709 file(s) [attempted 1709/8232 = 20%, 344 KB/s], Decompressed: 1466
Downloaded: 1747 file(s) [attempted 1747/8232 = 21%, 193 KB/s], Decompressed: 1593
Downloaded: 1785 file(s) [attempted 1785/8232 = 21%, 538 KB/s], Decompressed: 1593
Downloaded: 1829 file(s) [attempted 1829/8232 = 22%, 1741 KB/s], Decompressed: 1593
Downloaded: 1874 file(s) [attempted 1874/8232 = 22%, 492 KB/s], Decompressed: 1723
Downloaded: 1918 file(s) [attempted 1918/8232 = 23%, 607 KB/s], Decompressed: 1723
Downloaded: 1956 file(s) [attempted 1956/8232 = 23%, 123 KB/s], Decompressed: 1723
Downloaded: 1990 file(s) [attempted 1990/8232 = 24%, 137 KB/s], Decompressed: 1723
Downloaded: 2028 file(s) [attempted 2028/8232 = 24%, 860 KB/s], Decompressed: 1867
Downloaded: 2072 file(s) [attempted 2072/8232 = 25%, 1979 KB/s], Decompressed: 1867
Downloaded: 2117 file(s) [attempted 2117/8232 = 25%, 190 KB/s], Decompressed: 1867
Downloaded: 2134 file(s) [attempted 2134/8232 = 25%, 41 KB/s], Decompressed: 1867
Downloaded: 2195 file(s) [attempted 2195/8232 = 26%, 297 KB/s], Decompressed: 1867
Downloaded: 2230 file(s) [attempted 2230/8232 = 27%, 126 KB/s], Decompressed: 2021
Downloaded: 2274 file(s) [attempted 2274/8232 = 27%, 190 KB/s], Decompressed: 2021
Downloaded: 2319 file(s) [attempted 2319/8232 = 28%, 282 KB/s], Decompressed: 2021
Downloaded: 2363 file(s) [attempted 2363/8232 = 28%, 108 KB/s], Decompressed: 2021
Downloaded: 2404 file(s) [attempted 2404/8232 = 29%, 79 KB/s], Decompressed: 2021
Downloaded: 2431 file(s) [attempted 2431/8232 = 29%, 195 KB/s], Decompressed: 2216
Downloaded: 2476 file(s) [attempted 2476/8232 = 30%, 523 KB/s], Decompressed: 2216
Downloaded: 2520 file(s) [attempted 2520/8232 = 30%, 92 KB/s], Decompressed: 2216
Downloaded: 2558 file(s) [attempted 2558/8232 = 31%, 53 KB/s], Decompressed: 2216
Downloaded: 2603 file(s) [attempted 2603/8232 = 31%, 190 KB/s], Decompressed: 2216
Downloaded: 2633 file(s) [attempted 2633/8232 = 31%, 319 KB/s], Decompressed: 2216
Downloaded: 2678 file(s) [attempted 2678/8232 = 32%, 33 KB/s], Decompressed: 2216
Downloaded: 2719 file(s) [attempted 2719/8232 = 33%, 411 KB/s], Decompressed: 2431
Downloaded: 2757 file(s) [attempted 2757/8232 = 33%, 541 KB/s], Decompressed: 2431
Downloaded: 2805 file(s) [attempted 2805/8232 = 34%, 57 KB/s], Decompressed: 2431
Downloaded: 2842 file(s) [attempted 2842/8232 = 34%, 47 KB/s], Decompressed: 2431
Downloaded: 2877 file(s) [attempted 2877/8232 = 34%, 212 KB/s], Decompressed: 2431
Downloaded: 2914 file(s) [attempted 2914/8232 = 35%, 214 KB/s], Decompressed: 2431
Downloaded: 2959 file(s) [attempted 2959/8232 = 35%, 107 KB/s], Decompressed: 2431
Downloaded: 3006 file(s) [attempted 3006/8232 = 36%, 443 KB/s], Decompressed: 2431
Downloaded: 3054 file(s) [attempted 3054/8232 = 37%, 1231 KB/s], Decompressed: 2705
Downloaded: 3092 file(s) [attempted 3092/8232 = 37%, 168 KB/s], Decompressed: 2705
Downloaded: 3133 file(s) [attempted 3133/8232 = 38%, 429 KB/s], Decompressed: 2705
Downloaded: 3167 file(s) [attempted 3167/8232 = 38%, 200 KB/s], Decompressed: 2705
Downloaded: 3215 file(s) [attempted 3215/8232 = 39%, 136 KB/s], Decompressed: 2705
Downloaded: 3260 file(s) [attempted 3260/8232 = 39%, 425 KB/s], Decompressed: 2705
Downloaded: 3304 file(s) [attempted 3304/8232 = 40%, 1171 KB/s], Decompressed: 2705
Downloaded: 3345 file(s) [attempted 3345/8232 = 40%, 102 KB/s], Decompressed: 2705
Downloaded: 3376 file(s) [attempted 3376/8232 = 41%, 581 KB/s], Decompressed: 3013
Downloaded: 3417 file(s) [attempted 3417/8232 = 41%, 80 KB/s], Decompressed: 3013
Downloaded: 3462 file(s) [attempted 3462/8232 = 42%, 122 KB/s], Decompressed: 3013
Downloaded: 3506 file(s) [attempted 3506/8232 = 42%, 70 KB/s], Decompressed: 3013
Downloaded: 3551 file(s) [attempted 3551/8232 = 43%, 110 KB/s], Decompressed: 3013
Downloaded: 3595 file(s) [attempted 3595/8232 = 43%, 313 KB/s], Decompressed: 3013
Downloaded: 3629 file(s) [attempted 3629/8232 = 44%, 213 KB/s], Decompressed: 3013
Downloaded: 3667 file(s) [attempted 3667/8232 = 44%, 40 KB/s], Decompressed: 3013
Downloaded: 3711 file(s) [attempted 3711/8232 = 45%, 987 KB/s], Decompressed: 3013
Downloaded: 3759 file(s) [attempted 3759/8232 = 45%, 119 KB/s], Decompressed: 3356
Downloaded: 3800 file(s) [attempted 3800/8232 = 46%, 796 KB/s], Decompressed: 3356
Downloaded: 3842 file(s) [attempted 3842/8232 = 46%, 644 KB/s], Decompressed: 3356
Downloaded: 3879 file(s) [attempted 3879/8232 = 47%, 315 KB/s], Decompressed: 3356
Downloaded: 3920 file(s) [attempted 3920/8232 = 47%, 454 KB/s], Decompressed: 3356
Downloaded: 3961 file(s) [attempted 3961/8232 = 48%, 1079 KB/s], Decompressed: 3356
Downloaded: 3996 file(s) [attempted 3996/8232 = 48%, 999 KB/s], Decompressed: 3356
Downloaded: 4040 file(s) [attempted 4040/8232 = 49%, 166 KB/s], Decompressed: 3356
Downloaded: 4081 file(s) [attempted 4081/8232 = 49%, 52 KB/s], Decompressed: 3356
Downloaded: 4122 file(s) [attempted 4122/8232 = 50%, 437 KB/s], Decompressed: 3356
Downloaded: 4167 file(s) [attempted 4167/8232 = 50%, 191 KB/s], Decompressed: 3356
Downloaded: 4208 file(s) [attempted 4208/8232 = 51%, 70 KB/s], Decompressed: 3356
Downloaded: 4245 file(s) [attempted 4245/8232 = 51%, 383 KB/s], Decompressed: 3749
Downloaded: 4286 file(s) [attempted 4286/8232 = 52%, 328 KB/s], Decompressed: 3749
Downloaded: 4324 file(s) [attempted 4324/8232 = 52%, 332 KB/s], Decompressed: 3749
Downloaded: 4365 file(s) [attempted 4365/8232 = 53%, 788 KB/s], Decompressed: 3749
Downloaded: 4406 file(s) [attempted 4406/8232 = 53%, 260 KB/s], Decompressed: 3749
Downloaded: 4451 file(s) [attempted 4451/8232 = 54%, 36 KB/s], Decompressed: 3749
Downloaded: 4495 file(s) [attempted 4495/8232 = 54%, 493 KB/s], Decompressed: 3749
Downloaded: 4533 file(s) [attempted 4533/8232 = 55%, 60 KB/s], Decompressed: 3749
Downloaded: 4571 file(s) [attempted 4571/8232 = 55%, 281 KB/s], Decompressed: 3749
Downloaded: 4608 file(s) [attempted 4608/8232 = 55%, 291 KB/s], Decompressed: 3749
Downloaded: 4649 file(s) [attempted 4649/8232 = 56%, 1333 KB/s], Decompressed: 3749
Downloaded: 4697 file(s) [attempted 4697/8232 = 57%, 415 KB/s], Decompressed: 3749
Downloaded: 4738 file(s) [attempted 4738/8232 = 57%, 93 KB/s], Decompressed: 3749
Downloaded: 4779 file(s) [attempted 4779/8232 = 58%, 418 KB/s], Decompressed: 4211
Downloaded: 4810 file(s) [attempted 4810/8232 = 58%, 427 KB/s], Decompressed: 4211
Downloaded: 4851 file(s) [attempted 4851/8232 = 58%, 117 KB/s], Decompressed: 4211
Downloaded: 4896 file(s) [attempted 4896/8232 = 59%, 46 KB/s], Decompressed: 4211
Downloaded: 4933 file(s) [attempted 4933/8232 = 59%, 350 KB/s], Decompressed: 4211
Downloaded: 4978 file(s) [attempted 4978/8232 = 60%, 650 KB/s], Decompressed: 4211
Downloaded: 5019 file(s) [attempted 5019/8232 = 60%, 235 KB/s], Decompressed: 4211
Downloaded: 5060 file(s) [attempted 5060/8232 = 61%, 228 KB/s], Decompressed: 4211
Downloaded: 5098 file(s) [attempted 5098/8232 = 61%, 43 KB/s], Decompressed: 4211
Downloaded: 5135 file(s) [attempted 5135/8232 = 62%, 40 KB/s], Decompressed: 4211
Downloaded: 5176 file(s) [attempted 5176/8232 = 62%, 296 KB/s], Decompressed: 4211
Downloaded: 5217 file(s) [attempted 5217/8232 = 63%, 380 KB/s], Decompressed: 4211
Downloaded: 5258 file(s) [attempted 5258/8232 = 63%, 115 KB/s], Decompressed: 4211
Downloaded: 5300 file(s) [attempted 5300/8232 = 64%, 271 KB/s], Decompressed: 4211
Downloaded: 5341 file(s) [attempted 5341/8232 = 64%, 148 KB/s], Decompressed: 4211
Downloaded: 5375 file(s) [attempted 5375/8232 = 65%, 314 KB/s], Decompressed: 4745
Downloaded: 5419 file(s) [attempted 5419/8232 = 65%, 1079 KB/s], Decompressed: 4745
Downloaded: 5467 file(s) [attempted 5467/8232 = 66%, 232 KB/s], Decompressed: 4745
Downloaded: 5508 file(s) [attempted 5508/8232 = 66%, 216 KB/s], Decompressed: 4745
Downloaded: 5542 file(s) [attempted 5542/8232 = 67%, 224 KB/s], Decompressed: 4745
Downloaded: 5584 file(s) [attempted 5584/8232 = 67%, 678 KB/s], Decompressed: 4745
Downloaded: 5625 file(s) [attempted 5625/8232 = 68%, 296 KB/s], Decompressed: 4745
Downloaded: 5669 file(s) [attempted 5669/8232 = 68%, 496 KB/s], Decompressed: 4745
Downloaded: 5710 file(s) [attempted 5710/8232 = 69%, 218 KB/s], Decompressed: 4745
Downloaded: 5748 file(s) [attempted 5748/8232 = 69%, 148 KB/s], Decompressed: 4745
Downloaded: 5785 file(s) [attempted 5785/8232 = 70%, 1329 KB/s], Decompressed: 4745
Downloaded: 5827 file(s) [attempted 5827/8232 = 70%, 1766 KB/s], Decompressed: 4745
Downloaded: 5874 file(s) [attempted 5874/8232 = 71%, 838 KB/s], Decompressed: 4745
Downloaded: 5916 file(s) [attempted 5916/8232 = 71%, 857 KB/s], Decompressed: 4745
Downloaded: 5950 file(s) [attempted 5950/8232 = 72%, 54 KB/s], Decompressed: 4745
Downloaded: 5991 file(s) [attempted 5991/8232 = 72%, 958 KB/s], Decompressed: 4745
Downloaded: 6032 file(s) [attempted 6032/8232 = 73%, 143 KB/s], Decompressed: 5351
Downloaded: 6071 file(s) [attempted 6071/8232 = 73%, 90 KB/s], Decompressed: 5351
Downloaded: 6107 file(s) [attempted 6107/8232 = 74%, 48 KB/s], Decompressed: 5351
Downloaded: 6141 file(s) [attempted 6141/8232 = 74%, 705 KB/s], Decompressed: 5351
Downloaded: 6182 file(s) [attempted 6182/8232 = 75%, 50 KB/s], Decompressed: 5351
Downloaded: 6227 file(s) [attempted 6227/8232 = 75%, 347 KB/s], Decompressed: 5351
Downloaded: 6271 file(s) [attempted 6271/8232 = 76%, 301 KB/s], Decompressed: 5351
Downloaded: 6313 file(s) [attempted 6313/8232 = 76%, 50 KB/s], Decompressed: 5351
Downloaded: 6350 file(s) [attempted 6350/8232 = 77%, 1465 KB/s], Decompressed: 5351
Downloaded: 6391 file(s) [attempted 6391/8232 = 77%, 262 KB/s], Decompressed: 5351
Downloaded: 6432 file(s) [attempted 6432/8232 = 78%, 153 KB/s], Decompressed: 5351
Downloaded: 6473 file(s) [attempted 6473/8232 = 78%, 216 KB/s], Decompressed: 5351
Downloaded: 6511 file(s) [attempted 6511/8232 = 79%, 498 KB/s], Decompressed: 5351
Downloaded: 6552 file(s) [attempted 6552/8232 = 79%, 770 KB/s], Decompressed: 5351
Downloaded: 6597 file(s) [attempted 6597/8232 = 80%, 71 KB/s], Decompressed: 5351
Downloaded: 6634 file(s) [attempted 6634/8232 = 80%, 247 KB/s], Decompressed: 5351
Downloaded: 6679 file(s) [attempted 6679/8232 = 81%, 76 KB/s], Decompressed: 5351
Downloaded: 6713 file(s) [attempted 6713/8232 = 81%, 179 KB/s], Decompressed: 5351
Downloaded: 6751 file(s) [attempted 6751/8232 = 82%, 249 KB/s], Decompressed: 5351
Downloaded: 6795 file(s) [attempted 6795/8232 = 82%, 26 KB/s], Decompressed: 6018
Downloaded: 6840 file(s) [attempted 6840/8232 = 83%, 320 KB/s], Decompressed: 6018
Downloaded: 6877 file(s) [attempted 6877/8232 = 83%, 279 KB/s], Decompressed: 6018
Downloaded: 6918 file(s) [attempted 6918/8232 = 84%, 136 KB/s], Decompressed: 6018
Downloaded: 6960 file(s) [attempted 6960/8232 = 84%, 1636 KB/s], Decompressed: 6018
Downloaded: 7000 file(s) [attempted 7000/8232 = 85%, 716 KB/s], Decompressed: 6018
Downloaded: 7038 file(s) [attempted 7038/8232 = 85%, 312 KB/s], Decompressed: 6018
Downloaded: 7079 file(s) [attempted 7079/8232 = 85%, 264 KB/s], Decompressed: 6018
Downloaded: 7124 file(s) [attempted 7124/8232 = 86%, 130 KB/s], Decompressed: 6018
Downloaded: 7165 file(s) [attempted 7165/8232 = 87%, 215 KB/s], Decompressed: 6018
Downloaded: 7202 file(s) [attempted 7202/8232 = 87%, 949 KB/s], Decompressed: 6018
Downloaded: 7247 file(s) [attempted 7247/8232 = 88%, 73 KB/s], Decompressed: 6018
Downloaded: 7285 file(s) [attempted 7285/8232 = 88%, 534 KB/s], Decompressed: 6018
Downloaded: 7326 file(s) [attempted 7326/8232 = 88%, 543 KB/s], Decompressed: 6018
Downloaded: 7363 file(s) [attempted 7363/8232 = 89%, 272 KB/s], Decompressed: 6018
Downloaded: 7401 file(s) [attempted 7401/8232 = 89%, 1022 KB/s], Decompressed: 6018
Downloaded: 7445 file(s) [attempted 7445/8232 = 90%, 205 KB/s], Decompressed: 6018
Downloaded: 7486 file(s) [attempted 7486/8232 = 90%, 21 KB/s], Decompressed: 6018
Downloaded: 7527 file(s) [attempted 7527/8232 = 91%, 252 KB/s], Decompressed: 6018
Downloaded: 7565 file(s) [attempted 7565/8232 = 91%, 153 KB/s], Decompressed: 6018
Downloaded: 7603 file(s) [attempted 7603/8232 = 92%, 235 KB/s], Decompressed: 6018
Downloaded: 7644 file(s) [attempted 7644/8232 = 92%, 277 KB/s], Decompressed: 6764
Downloaded: 7682 file(s) [attempted 7682/8232 = 93%, 425 KB/s], Decompressed: 6764
Downloaded: 7726 file(s) [attempted 7726/8232 = 93%, 304 KB/s], Decompressed: 6764
Downloaded: 7767 file(s) [attempted 7767/8232 = 94%, 284 KB/s], Decompressed: 6764
Downloaded: 7805 file(s) [attempted 7805/8232 = 94%, 189 KB/s], Decompressed: 6764
Downloaded: 7846 file(s) [attempted 7846/8232 = 95%, 125 KB/s], Decompressed: 6764
Downloaded: 7890 file(s) [attempted 7890/8232 = 95%, 821 KB/s], Decompressed: 6764
Downloaded: 7931 file(s) [attempted 7931/8232 = 96%, 182 KB/s], Decompressed: 6764
Downloaded: 7969 file(s) [attempted 7969/8232 = 96%, 94 KB/s], Decompressed: 6764
Downloaded: 8007 file(s) [attempted 8007/8232 = 97%, 272 KB/s], Decompressed: 6764
Downloaded: 8044 file(s) [attempted 8044/8232 = 97%, 41 KB/s], Decompressed: 6764
Downloaded: 8085 file(s) [attempted 8085/8232 = 98%, 184 KB/s], Decompressed: 6764
Downloaded: 8126 file(s) [attempted 8126/8232 = 98%, 193 KB/s], Decompressed: 6764
Downloaded: 8164 file(s) [attempted 8164/8232 = 99%, 291 KB/s], Decompressed: 6764
Downloaded: 8202 file(s) [attempted 8202/8232 = 99%, 187 KB/s], Decompressed: 6764
Downloaded: 8229 file(s) [attempted 8229/8232 = 99%, 81 KB/s], Decompressed: 6764
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 81 KB/s], Decompressed: 6764

lean_checker exit 0 duration 15m 11s · created 6/2/2026, 1:50:33 PM

lake build

✔ [2765/2811] Built Architect.Command (4.5s)
✔ [2809/2835] Built Architect.Basic (5.0s)
✔ [2812/2835] Built Architect.Tactic (1.7s)
✔ [2813/2838] Built Architect.CollectUsed (1.8s)
✔ [2816/2838] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (3.9s)
✔ [2821/2844] Built PrimeNumberTheoremAnd.Auxiliary (9.0s)
✔ [3032/3066] Built Architect.Content (1.5s)
✔ [3054/3080] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (3.4s)
✔ [3225/3264] Built Architect.Output (2.8s)
✔ [3275/3359] Built Architect.Attribute (2.0s)
✔ [3440/3460] Built Architect.Load (1.1s)
✔ [3443/3464] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.4s)
✔ [3445/3468] Built Architect (1.4s)
✔ [3448/3468] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (2.5s)
✔ [3449/3468] Built PrimeNumberTheoremAnd.Sobolev (15s)
✔ [3450/3468] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (5.9s)
✔ [3451/3468] Built PrimeNumberTheoremAnd.SmoothExistence (5.3s)
✔ [3454/3468] Built PrimeNumberTheoremAnd.ZetaConj (5.3s)
✔ [3455/3472] Built PrimeNumberTheoremAnd.Rectangle (6.3s)
✔ [3456/3473] Built PrimeNumberTheoremAnd.Fourier (5.4s)
✔ [3459/3473] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (7.3s)
✔ [3462/3478] Built PrimeNumberTheoremAnd.Defs (11s)
✔ [3580/3606] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (15s)
✔ [3581/3611] Built PrimeNumberTheoremAnd.HadamardFactorization (1.5s)
✔ [3584/3612] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (12s)
✔ [3585/3613] Built PrimeNumberTheoremAnd.MellinCalculus (21s)
✔ [3589/3613] Built PrimeNumberTheoremAnd.HoffsteinLockhart (3.5s)
✔ [3591/3614] Built PrimeNumberTheoremAnd.GeneralMeromorphic (3.1s)
✔ [3594/3617] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (5.5s)
✔ [3597/3617] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (7.8s)
⚠ [3600/3617] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3601/3620] Built PrimeNumberTheoremAnd.BrunTitchmarsh (14s)
✔ [3614/3635] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (22s)
✔ [3655/3675] Built PrimeNumberTheoremAnd.IEANTN.KLN (6.6s)
✔ [3665/3686] Built LeanCert.Core.Interval (5.9s)
✔ [3666/3687] Built LeanCert.Core.Expr (13s)
✔ [3667/3687] Built LeanCert.Core.Support (8.1s)
✔ [3668/3687] Built LeanCert.Core.IntervalRat.Basic (20s)
✔ [3669/3688] Built LeanCert.Meta.Numeral (6.0s)
✔ [3670/3688] Built LeanCert.Core.IntervalRat.Transcendental (9.9s)
✔ [3671/3688] Built LeanCert.Tactic.IntervalAuto.Types (6.7s)
✔ [3672/3688] Built LeanCert.Tactic.IntervalAuto.Extract (5.9s)
✔ [3673/3689] Built PrimeNumberTheoremAnd.ZetaBounds (67s)
✔ [3674/3693] Built LeanCert.Meta.ToExpr (7.5s)
✔ [3675/3693] Built LeanCert.Core.IntervalRat.LogReduction (8.0s)
✔ [3676/3694] Built LeanCert.Tactic.IntervalAuto.Norm (6.9s)
✔ [3678/3694] Built LeanCert.Tactic.IntervalAuto.Parse (13s)
✔ [3679/3697] Built LeanCert.Core.DerivativeIntervals (11s)
✔ [3680/3697] Built LeanCert.Tactic.IntervalAuto.Diagnostic (7.9s)
⚠ [3681/3699] Built PrimeNumberTheoremAnd.Wiener (91s)
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
✔ [3682/3699] Built LeanCert.Core.Taylor (16s)
✔ [3683/3700] Built LeanCert.Core.IntervalRat.Taylor (40s)
✔ [3684/3700] Built LeanCert.Core.IntervalRat.TrigReduced (17s)
✔ [3685/3702] Built LeanCert.Core.IntervalReal (7.1s)
✔ [3686/3703] Built LeanCert.Core.IntervalRealEndpoints (12s)
✔ [3687/3705] Built LeanCert.Engine.Eval.Core (14s)
ℹ [3688/3710] Built PrimeNumberTheoremAnd.MediumPNT (142s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3689/3710] Built LeanCert.Engine.Eval.Extended (6.3s)
✔ [3690/3710] Built LeanCert.Contrib.Sinc (6.9s)
✔ [3691/3719] Built PrimeNumberTheoremAnd.Consequences (110s)
⚠ [3702/3732] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (154s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3703/3732] Built LeanCert.Tactic.Bound.Lemmas (3.0s)
✔ [3704/3737] Built LeanCert.Core.Dyadic (3.0s)
⚠ [3705/3740] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (4.0s)
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`
✔ [3706/3740] Built LeanCert.Engine.IntervalEval (3.2s)
✔ [3707/3740] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (7.8s)
✔ [3708/3741] Built LeanCert.Engine.Affine.Basic (10s)
✔ [3709/3741] Built LeanCert.Engine.Optimization.Box (5.7s)
✔ [3710/3742] Built LeanCert.Core.IntervalDyadic (14s)
✔ [3711/3742] Built LeanCert.Engine.AD.Basic (6.3s)
✔ [3712/3743] Built LeanCert.Engine.RootFinding.Basic (8.5s)
✔ [3713/3744] Built LeanCert.Engine.TaylorModel.Core (14s)
✔ [3714/3744] Built LeanCert.Engine.Affine.Nonlinear (7.2s)
✔ [3715/3746] Built LeanCert.Engine.IntervalEvalDyadic (6.0s)
✔ [3716/3746] Built LeanCert.Engine.AD.Transcendental (5.4s)
⚠ [3717/3746] Built PrimeNumberTheoremAnd.StrongPNT (35s)
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`
✔ [3718/3746] Built LeanCert.Engine.TaylorModel.Special (3.2s)
✔ [3719/3747] Built LeanCert.Engine.RootFinding.Bisection (4.9s)
✔ [3720/3747] Built LeanCert.Engine.TaylorModel.ExpLog (12s)
✔ [3721/3749] Built LeanCert.Engine.Affine.Transcendental (9.8s)
✔ [3722/3749] Built LeanCert.Engine.TaylorModel.Trig (13s)
✔ [3723/3752] Built LeanCert.Engine.AD.Eval (3.3s)
✔ [3724/3752] Built LeanCert.Engine.TaylorModel.Hyperbolic (15s)
✔ [3725/3752] Built LeanCert.Engine.TaylorModel.Functions (2.8s)
✔ [3726/3753] Built PrimeNumberTheoremAnd.BorelCaratheodory (7.0s)
✔ [3727/3754] Built LeanCert.Engine.IntervalEvalAffine (4.4s)
✔ [3728/3754] Built LeanCert.Validity.DyadicBounds (3.5s)
✔ [3729/3771] Built LeanCert.Engine.Integrate (7.3s)
✔ [3730/3771] Built LeanCert.Engine.AD.Correctness (4.2s)
⚠ [3732/3771] Built PrimeNumberTheoremAnd.DerivativeBound (4.2s)
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
✔ [3733/3772] Built LeanCert.Engine.TaylorModel.Expr (6.3s)
✔ [3734/3773] Built LeanCert.Engine.AD.Computable (6.3s)
✔ [3735/3773] Built LeanCert.Engine.TaylorModel.Log1p (10s)
✔ [3736/3774] Built LeanCert.Engine.AD.PartialCorrectness (8.0s)
✔ [3739/3774] Built LeanCert.Engine.TaylorModel (2.6s)
✔ [3740/3782] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (12s)
✔ [3856/3900] Built LeanCert.Engine.AD (3.4s)
⚠ [3857/3900] Built LeanCert.Examples.Li2Bounds (4.9s)
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3858/3901] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (4.1s)
✔ [3859/3901] Built LeanCert.Tactic.VecUtil (3.6s)
✔ [3860/3901] Built LeanCert.Engine.IntervalEvalRefined (6.4s)
✔ [3861/3901] Built LeanCert.Meta.ProveSupported (7.9s)
✔ [3862/3903] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (5.5s)
✔ [3864/3903] Built LeanCert.Engine.Optimize (8.0s)
✔ [3865/3904] Built LeanCert.Tactic.FinSumExpand (2.5s)
✔ [3866/3907] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (23s)
✔ [3868/3907] Built LeanCert.Meta.ProveContinuous (3.9s)
✔ [3869/3907] Built LeanCert.Tactic.IntervalAuto.ProveCommon (5.6s)
✔ [3873/3914] Built LeanCert.Engine.Optimization.Gradient (5.5s)
✔ [3874/3914] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (34s)
✔ [3875/3914] Built LeanCert.Engine.RootFinding.Newton (5.7s)
✔ [3876/3914] Built LeanCert.Tactic.IntervalAuto.Basic (2.8s)
✔ [3877/3916] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (3.7s)
✔ [3878/3916] Built LeanCert.Engine.Chebyshev.Psi (4.0s)
✔ [3879/3921] Built LeanCert.Engine.RootFinding.MVTBounds (15s)
✔ [3880/3921] Built LeanCert.Engine.Optimization.Global (33s)
✔ [3881/3921] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (29s)
✔ [3883/3921] Built LeanCert.Engine.ChebyshevPsi (4.8s)
✔ [3885/3922] Built PrimeNumberTheoremAnd.Tactic.Simprocs (3.4s)
✔ [3887/3923] Built LeanCert.Engine.RootFinding.Contraction (9.0s)
✔ [3889/3924] Built LeanCert.Engine.Optimization.BoundVerify (6.8s)
✔ [3890/3924] Built PrimeCert.Interval (6.3s)
✔ [3891/3924] Built PrimeCert.Meta.PrimeCert (3.7s)
✔ [3892/3925] Built LeanCert.Engine.RootFinding.Main (4.4s)
✔ [3893/3926] Built PrimeCert.Meta.SmallPrime (2.0s)
✔ [3894/3927] Built PrimeCert.PredMod (539ms)
✔ [3895/3931] Built PrimeCert.PowMod (4.1s)
✔ [3898/3938] Built LeanCert.Validity.Bounds (15s)
⚠ [3899/3938] Built PrimeCert.Pocklington (9.1s)
warning: PrimeCert/Pocklington.lean:60:22: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3900/3938] Built LeanCert.Tactic.IntervalAuto.Multivariate (8.4s)
✔ [3901/3938] Built LeanCert.Tactic.IntervalAuto.OptBound (5.3s)
⚠ [3902/3938] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (63s)
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`
✔ [3903/3938] Built LeanCert.Tactic.IntervalAuto.RootBound (4.9s)
✔ [3904/3938] Built PrimeCert.Wieferich (5.6s)
✔ [3905/3948] Built PrimeCert.SmallPrimes (4.8s)
✔ [3907/3948] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (10s)
⚠ [3912/3960] 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
✔ [3914/3960] Built LeanCert.Tactic.IntervalAuto.Bound (47s)
⚠ [3915/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (133s)
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`
⚠ [3916/3960] Built PrimeNumberTheoremAnd.IEANTN.Mertens (29s)
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.Engine.Chebyshev.Theta (16s)
✔ [3919/3960] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (3.6s)
✔ [3920/3960] Built PrimeCert (3.8s)
✔ [3921/3960] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (34s)
⚠ [3922/3960] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (7.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`
✔ [3923/3960] Built LeanCert.Tactic.IntervalAuto.Subdiv (10s)
⚠ [3924/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (8.4s)
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 LeanCert.Tactic.IntervalAuto.Adaptive (9.9s)
✔ [3927/3960] Built LeanCert.Engine.ChebyshevTheta (2.6s)
✔ [3928/3960] Built LeanCert.Tactic.IntervalAuto.PointIneq (20s)
✔ [3929/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (11s)
✔ [3930/3960] Built PrimeNumberTheoremAnd.PerronFormula (12s)
✔ [3931/3960] Built LeanCert.Tactic.IntervalAuto (4.2s)
⚠ [3932/3960] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (11s)
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`
✔ [3933/3960] Built PrimeNumberTheoremAnd.IEANTN.LogTables (13s)
✔ [3934/3960] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (15s)
ℹ [3935/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (44s)
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 (50s)
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 (6.3s)
✔ [3938/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (11s)
⚠ [3939/3960] Built PrimeNumberTheoremAnd.IEANTN.Buthe (31s)
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`
✔ [3940/3960] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (45s)
✔ [3941/3960] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (26s)
⚠ [3942/3960] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (33s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3943/3960] Built LeanCert.Examples.BKLNW_a2_bounds (6.8s)
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`
⚠ [3944/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (7.6s)
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.Erdos392 (122s)
✔ [3946/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.6s)
⚠ [3947/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (5.3s)
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 (173s)
⚠ [3949/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (30s)
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 (9.5s)
⚠ [3951/3960] Built PrimeNumberTheoremAnd.IEANTN.Dusart (29s)
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 (15s)
⚠ [3953/3960] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (24s)
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`
⚠ [3954/3960] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (71s)
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`
⚠ [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 (15s)
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 (43s)
✔ [3958/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (74s)
✔ [3959/3960] Built PrimeNumberTheoremAnd (2.8s)
Build completed successfully (3960 jobs).

blueprint_build exit 0 duration 5m 19s · created 6/2/2026, 1:50:33 PM

lake build :blueprint

✔ [11/35] Built Architect.Command:c.o (408ms)
✔ [12/35] Built Architect.Content:c.o (180ms)
✔ [13/35] Built Batteries.Lean.NameMapAttribute:c.o (648ms)
✔ [14/35] Built Architect.Basic:c.o (784ms)
✔ [15/35] Built Architect.CollectUsed:c.o (142ms)
✔ [17/35] Built Architect.Tactic:c.o (374ms)
✔ [23/35] Built Architect.Load:c.o (136ms)
✔ [25/35] Built Architect:c.o (96ms)
✔ [27/35] Built Architect.Attribute:c.o (950ms)
✔ [28/35] Built Cli:c.o (52ms)
✔ [29/43] Built Cli.Extensions:c.o (627ms)
✔ [276/381] Built Architect.Output:c.o (1.9s)
✔ [463/563] Built Main (1.1s)
✔ [762/908] Built Main:c.o (262ms)
ℹ [3456/3666] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3474/3666] 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`
⚠ [3604/3666] Replayed PrimeNumberTheoremAnd.DerivativeBound
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
⚠ [3627/3877] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
⚠ [3630/3877] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3686/3877] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3687/3877] 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`
⚠ [3780/3877] 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`
⚠ [3782/3877] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3908/4060] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3910/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`
⚠ [3911/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`
⚠ [3913/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`
⚠ [3916/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`
⚠ [3917/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`
⚠ [3924/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`
⚠ [3925/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`
⚠ [3931/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`
⚠ [3932/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`
⚠ [3937/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`
⚠ [3947/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
⚠ [3948/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
⚠ [3954/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`
⚠ [3955/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`
⚠ [3956/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`
⚠ [3962/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`
⚠ [3966/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`
ℹ [3972/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.
⚠ [3974/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`
✔ [3978/4060] Built Cli.Basic:c.o (4.2s)
✔ [3979/4060] Built extract_blueprint:exe (2.8s)
✔ [3980/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (2.4s)
✔ [3981/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (2.9s)
✔ [3982/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (2.9s)
✔ [3983/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (2.3s)
✔ [3984/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (2.5s)
✔ [3985/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.5s)
✔ [3986/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (17s)
✔ [3987/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (14s)
✔ [3988/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (1.8s)
✔ [3989/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (5.2s)
✔ [3990/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (75s)
✔ [3991/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (63s)
✔ [3992/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (8.1s)
✔ [3993/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.9s)
✔ [3994/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (2.9s)
✔ [3995/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.8s)
✔ [3996/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [3997/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (3.3s)
✔ [3998/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (3.0s)
✔ [3999/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (10s)
✔ [4000/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (45s)
✔ [4001/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (19s)
✔ [4002/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.DerivativeBound:blueprint (5.4s)
✔ [4003/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.5s)
✔ [4004/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (3.3s)
✔ [4005/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.3s)
✔ [4006/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (3.4s)
✔ [4007/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (13s)
✔ [4008/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (3.8s)
✔ [4009/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (3.9s)
✔ [4010/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (32s)
✔ [4011/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (4.5s)
✔ [4012/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.6s)
✔ [4013/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (3.2s)
✔ [4014/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (3.2s)
✔ [4015/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (7.3s)
✔ [4016/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (2.0s)
✔ [4017/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.7s)
✔ [4018/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (2.8s)
✔ [4019/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (12s)
✔ [4020/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (8.4s)
✔ [4021/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (3.8s)
✔ [4022/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (24s)
✔ [4023/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (4.7s)
✔ [4024/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (7.6s)
✔ [4025/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (21s)
✔ [4026/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (6.1s)
✔ [4027/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (33s)
✔ [4028/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (6.4s)
✔ [4029/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (68s)
✔ [4030/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
✔ [4031/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (24s)
✔ [4032/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (5.7s)
✔ [4033/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (3.1s)
✔ [4034/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (4.4s)
✔ [4035/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (24s)
✔ [4036/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (22s)
✔ [4037/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (42s)
✔ [4038/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (1.8s)
✔ [4039/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (2.8s)
✔ [4040/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.9s)
✔ [4041/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (58s)
✔ [4042/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (8.1s)
✔ [4043/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (7.8s)
✔ [4044/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (12s)
✔ [4045/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (3.2s)
✔ [4046/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (14s)
✔ [4047/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (41s)
✔ [4048/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (13s)
✔ [4049/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.8s)
✔ [4050/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (10s)
✔ [4051/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (28s)
✔ [4052/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (59s)
✔ [4053/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (12s)
✔ [4054/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (26s)
✔ [4055/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (12s)
✔ [4056/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (20s)
✔ [4057/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (74s)
✔ [4058/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (23s)
ℹ [4059/4061] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (92ms)
info: Blueprint indexing
Build completed successfully (4061 jobs).

semantic_extract exit 0 duration 13m 18s · created 6/2/2026, 1:50:33 PM

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