Verification run
Run 3
succeeded commit
109b9f617702 toolchain lean-v4-29-0 prover lean took 33m 26s · 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
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-18-source
Cloning into '/var/lib/apodeixis/repos/job-18-source'...
git_checkout exit 0
git checkout 109b9f6177020e3cac5602eda08fb619a0fd2f1a
Note: switching to '109b9f6177020e3cac5602eda08fb619a0fd2f1a'. You are in 'detached HEAD' state. You can look around, make experimental changes and commit them, and you can discard any commits you make in this state without impacting any branches by switching back to a branch. If you want to create a new branch to retain commits you create, you may do so (now or later) by using -c with the switch command. Example: git switch -c <new-branch-name> Or undo this operation with: git switch - Turn off this advice by setting config variable advice.detachedHead to false HEAD is now at 109b9f6 fix: align Dusart1999.pi_inequality blueprint with Lean hypothesis (#1466)
lake_cache exit 0
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 (384ms)
✔ [3/22] Built Cache.Init (294ms)
✔ [4/22] Built Cache.Lean:c.o (310ms)
✔ [5/22] Built Cache.Init:c.o (372ms)
✔ [6/22] Built Cache.IO (1.1s)
✔ [7/22] Built Cache.Hashing (605ms)
✔ [8/22] Built Cache.Hashing:c.o (398ms)
✔ [9/22] Built Cache.IO:c.o (1.3s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (91ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (251ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (180ms)
✔ [18/22] Built Cache.Requests (1.7s)
✔ [19/22] Built Cache.Main (692ms)
✔ [20/22] Built Cache.Main:c.o (479ms)
✔ [21/22] Built Cache.Requests:c.o (1.0s)
✔ [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 7378k 0 --:--:-- --:--:-- --:--:-- 7378k
Downloaded: 1 file(s) [attempted 1/8232 = 0%, 13 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8232 = 0%, 4 KB/s], Decompressed: 9
Downloaded: 38 file(s) [attempted 38/8232 = 0%, 73 KB/s], Decompressed: 31
Downloaded: 67 file(s) [attempted 67/8232 = 0%, 29 KB/s], Decompressed: 61
Downloaded: 100 file(s) [attempted 100/8232 = 1%, 517 KB/s], Decompressed: 89
Downloaded: 137 file(s) [attempted 137/8232 = 1%, 938 KB/s], Decompressed: 117
Downloaded: 175 file(s) [attempted 175/8232 = 2%, 641 KB/s], Decompressed: 134
Downloaded: 210 file(s) [attempted 210/8232 = 2%, 342 KB/s], Decompressed: 155
Downloaded: 251 file(s) [attempted 251/8232 = 3%, 83 KB/s], Decompressed: 185
Downloaded: 292 file(s) [attempted 292/8232 = 3%, 735 KB/s], Decompressed: 227
Downloaded: 333 file(s) [attempted 333/8232 = 4%, 90 KB/s], Decompressed: 227
Downloaded: 371 file(s) [attempted 371/8232 = 4%, 90 KB/s], Decompressed: 278
Downloaded: 415 file(s) [attempted 415/8232 = 5%, 211 KB/s], Decompressed: 342
Downloaded: 463 file(s) [attempted 463/8232 = 5%, 435 KB/s], Decompressed: 342
Downloaded: 504 file(s) [attempted 504/8232 = 6%, 1149 KB/s], Decompressed: 401
Downloaded: 545 file(s) [attempted 545/8232 = 6%, 322 KB/s], Decompressed: 401
Downloaded: 586 file(s) [attempted 586/8232 = 7%, 206 KB/s], Decompressed: 470
Downloaded: 631 file(s) [attempted 631/8232 = 7%, 175 KB/s], Decompressed: 470
Downloaded: 665 file(s) [attempted 665/8232 = 8%, 589 KB/s], Decompressed: 552
Downloaded: 710 file(s) [attempted 710/8232 = 8%, 96 KB/s], Decompressed: 552
Downloaded: 754 file(s) [attempted 754/8232 = 9%, 365 KB/s], Decompressed: 552
Downloaded: 795 file(s) [attempted 795/8232 = 9%, 487 KB/s], Decompressed: 552
Downloaded: 836 file(s) [attempted 836/8232 = 10%, 103 KB/s], Decompressed: 665
Downloaded: 871 file(s) [attempted 871/8232 = 10%, 218 KB/s], Decompressed: 665
Downloaded: 915 file(s) [attempted 915/8232 = 11%, 1068 KB/s], Decompressed: 665
Downloaded: 960 file(s) [attempted 960/8232 = 11%, 629 KB/s], Decompressed: 665
Downloaded: 997 file(s) [attempted 997/8232 = 12%, 592 KB/s], Decompressed: 802
Downloaded: 1039 file(s) [attempted 1039/8232 = 12%, 338 KB/s], Decompressed: 802
Downloaded: 1080 file(s) [attempted 1080/8232 = 13%, 583 KB/s], Decompressed: 802
Downloaded: 1117 file(s) [attempted 1117/8232 = 13%, 179 KB/s], Decompressed: 802
Downloaded: 1162 file(s) [attempted 1162/8232 = 14%, 230 KB/s], Decompressed: 963
Downloaded: 1203 file(s) [attempted 1203/8232 = 14%, 278 KB/s], Decompressed: 963
Downloaded: 1251 file(s) [attempted 1251/8232 = 15%, 611 KB/s], Decompressed: 963
Downloaded: 1295 file(s) [attempted 1295/8232 = 15%, 100 KB/s], Decompressed: 963
Downloaded: 1336 file(s) [attempted 1336/8232 = 16%, 315 KB/s], Decompressed: 963
Downloaded: 1381 file(s) [attempted 1381/8232 = 16%, 85 KB/s], Decompressed: 963
Downloaded: 1418 file(s) [attempted 1418/8232 = 17%, 61 KB/s], Decompressed: 1148
Downloaded: 1459 file(s) [attempted 1459/8232 = 17%, 280 KB/s], Decompressed: 1148
Downloaded: 1501 file(s) [attempted 1501/8232 = 18%, 207 KB/s], Decompressed: 1148
Downloaded: 1545 file(s) [attempted 1545/8232 = 18%, 210 KB/s], Decompressed: 1148
Downloaded: 1586 file(s) [attempted 1586/8232 = 19%, 190 KB/s], Decompressed: 1148
Downloaded: 1627 file(s) [attempted 1627/8232 = 19%, 312 KB/s], Decompressed: 1148
Downloaded: 1672 file(s) [attempted 1672/8232 = 20%, 319 KB/s], Decompressed: 1148
Downloaded: 1716 file(s) [attempted 1716/8232 = 20%, 900 KB/s], Decompressed: 1398
Downloaded: 1757 file(s) [attempted 1757/8232 = 21%, 406 KB/s], Decompressed: 1398
Downloaded: 1798 file(s) [attempted 1798/8232 = 21%, 68 KB/s], Decompressed: 1398
Downloaded: 1839 file(s) [attempted 1839/8232 = 22%, 671 KB/s], Decompressed: 1398
Downloaded: 1880 file(s) [attempted 1880/8232 = 22%, 530 KB/s], Decompressed: 1398
Downloaded: 1921 file(s) [attempted 1921/8232 = 23%, 161 KB/s], Decompressed: 1398
Downloaded: 1963 file(s) [attempted 1963/8232 = 23%, 1365 KB/s], Decompressed: 1398
Downloaded: 2000 file(s) [attempted 2000/8232 = 24%, 66 KB/s], Decompressed: 1678
Downloaded: 2041 file(s) [attempted 2041/8232 = 24%, 29 KB/s], Decompressed: 1678
Downloaded: 2082 file(s) [attempted 2082/8232 = 25%, 203 KB/s], Decompressed: 1678
Downloaded: 2123 file(s) [attempted 2123/8232 = 25%, 309 KB/s], Decompressed: 1678
Downloaded: 2164 file(s) [attempted 2164/8232 = 26%, 885 KB/s], Decompressed: 1678
Downloaded: 2202 file(s) [attempted 2202/8232 = 26%, 909 KB/s], Decompressed: 1678
Downloaded: 2240 file(s) [attempted 2240/8232 = 27%, 311 KB/s], Decompressed: 1678
Downloaded: 2284 file(s) [attempted 2284/8232 = 27%, 87 KB/s], Decompressed: 1678
Downloaded: 2325 file(s) [attempted 2325/8232 = 28%, 128 KB/s], Decompressed: 1678
Downloaded: 2366 file(s) [attempted 2366/8232 = 28%, 256 KB/s], Decompressed: 1678
Downloaded: 2407 file(s) [attempted 2407/8232 = 29%, 83 KB/s], Decompressed: 1993
Downloaded: 2445 file(s) [attempted 2445/8232 = 29%, 373 KB/s], Decompressed: 1993
Downloaded: 2486 file(s) [attempted 2486/8232 = 30%, 56 KB/s], Decompressed: 1993
Downloaded: 2527 file(s) [attempted 2527/8232 = 30%, 448 KB/s], Decompressed: 1993
Downloaded: 2572 file(s) [attempted 2572/8232 = 31%, 131 KB/s], Decompressed: 1993
Downloaded: 2609 file(s) [attempted 2609/8232 = 31%, 862 KB/s], Decompressed: 1993
Downloaded: 2650 file(s) [attempted 2650/8232 = 32%, 110 KB/s], Decompressed: 1993
Downloaded: 2695 file(s) [attempted 2695/8232 = 32%, 882 KB/s], Decompressed: 1993
Downloaded: 2736 file(s) [attempted 2736/8232 = 33%, 134 KB/s], Decompressed: 1993
Downloaded: 2781 file(s) [attempted 2781/8232 = 33%, 205 KB/s], Decompressed: 1993
Downloaded: 2818 file(s) [attempted 2818/8232 = 34%, 310 KB/s], Decompressed: 1993
Downloaded: 2859 file(s) [attempted 2859/8232 = 34%, 582 KB/s], Decompressed: 2370
Downloaded: 2907 file(s) [attempted 2907/8232 = 35%, 605 KB/s], Decompressed: 2370
Downloaded: 2950 file(s) [attempted 2950/8232 = 35%, 24 KB/s], Decompressed: 2370
Downloaded: 2989 file(s) [attempted 2989/8232 = 36%, 177 KB/s], Decompressed: 2370
Downloaded: 3030 file(s) [attempted 3030/8232 = 36%, 137 KB/s], Decompressed: 2370
Downloaded: 3065 file(s) [attempted 3065/8232 = 37%, 47 KB/s], Decompressed: 2370
Downloaded: 3102 file(s) [attempted 3102/8232 = 37%, 211 KB/s], Decompressed: 2370
Downloaded: 3150 file(s) [attempted 3150/8232 = 38%, 352 KB/s], Decompressed: 2370
Downloaded: 3191 file(s) [attempted 3191/8232 = 38%, 334 KB/s], Decompressed: 2370
Downloaded: 3236 file(s) [attempted 3236/8232 = 39%, 213 KB/s], Decompressed: 2370
Downloaded: 3277 file(s) [attempted 3277/8232 = 39%, 917 KB/s], Decompressed: 2370
Downloaded: 3311 file(s) [attempted 3311/8232 = 40%, 411 KB/s], Decompressed: 2370
Downloaded: 3355 file(s) [attempted 3355/8232 = 40%, 176 KB/s], Decompressed: 2370
Downloaded: 3400 file(s) [attempted 3400/8232 = 41%, 192 KB/s], Decompressed: 2822
Downloaded: 3444 file(s) [attempted 3444/8232 = 41%, 66 KB/s], Decompressed: 2822
Downloaded: 3489 file(s) [attempted 3489/8232 = 42%, 175 KB/s], Decompressed: 2822
Downloaded: 3527 file(s) [attempted 3527/8232 = 42%, 577 KB/s], Decompressed: 2822
Downloaded: 3571 file(s) [attempted 3571/8232 = 43%, 1331 KB/s], Decompressed: 2822
Downloaded: 3605 file(s) [attempted 3605/8232 = 43%, 642 KB/s], Decompressed: 2822
Downloaded: 3646 file(s) [attempted 3646/8232 = 44%, 493 KB/s], Decompressed: 2822
Downloaded: 3687 file(s) [attempted 3687/8232 = 44%, 328 KB/s], Decompressed: 2822
Downloaded: 3729 file(s) [attempted 3729/8232 = 45%, 57 KB/s], Decompressed: 2822
Downloaded: 3773 file(s) [attempted 3773/8232 = 45%, 1296 KB/s], Decompressed: 2822
Downloaded: 3818 file(s) [attempted 3818/8232 = 46%, 116 KB/s], Decompressed: 2822
Downloaded: 3862 file(s) [attempted 3862/8232 = 46%, 332 KB/s], Decompressed: 2822
Downloaded: 3903 file(s) [attempted 3903/8232 = 47%, 725 KB/s], Decompressed: 2822
Downloaded: 3937 file(s) [attempted 3937/8232 = 47%, 99 KB/s], Decompressed: 2822
Downloaded: 3978 file(s) [attempted 3978/8232 = 48%, 465 KB/s], Decompressed: 2822
Downloaded: 4019 file(s) [attempted 4019/8232 = 48%, 33 KB/s], Decompressed: 2822
Downloaded: 4064 file(s) [attempted 4064/8232 = 49%, 42 KB/s], Decompressed: 3376
Downloaded: 4108 file(s) [attempted 4108/8232 = 49%, 34 KB/s], Decompressed: 3376
Downloaded: 4149 file(s) [attempted 4149/8232 = 50%, 198 KB/s], Decompressed: 3376
Downloaded: 4187 file(s) [attempted 4187/8232 = 50%, 142 KB/s], Decompressed: 3376
Downloaded: 4232 file(s) [attempted 4232/8232 = 51%, 183 KB/s], Decompressed: 3376
Downloaded: 4273 file(s) [attempted 4273/8232 = 51%, 71 KB/s], Decompressed: 3376
Downloaded: 4310 file(s) [attempted 4310/8232 = 52%, 81 KB/s], Decompressed: 3376
Downloaded: 4358 file(s) [attempted 4358/8232 = 52%, 71 KB/s], Decompressed: 3376
Downloaded: 4399 file(s) [attempted 4399/8232 = 53%, 308 KB/s], Decompressed: 3376
Downloaded: 4444 file(s) [attempted 4444/8232 = 53%, 1219 KB/s], Decompressed: 3376
Downloaded: 4495 file(s) [attempted 4495/8232 = 54%, 21 KB/s], Decompressed: 3376
Downloaded: 4543 file(s) [attempted 4543/8232 = 55%, 59 KB/s], Decompressed: 3376
Downloaded: 4588 file(s) [attempted 4588/8232 = 55%, 33 KB/s], Decompressed: 3376
Downloaded: 4622 file(s) [attempted 4622/8232 = 56%, 231 KB/s], Decompressed: 3376
Downloaded: 4659 file(s) [attempted 4659/8232 = 56%, 36 KB/s], Decompressed: 3376
Downloaded: 4704 file(s) [attempted 4704/8232 = 57%, 416 KB/s], Decompressed: 3376
Downloaded: 4748 file(s) [attempted 4748/8232 = 57%, 54 KB/s], Decompressed: 3376
Downloaded: 4793 file(s) [attempted 4793/8232 = 58%, 165 KB/s], Decompressed: 3376
Downloaded: 4837 file(s) [attempted 4837/8232 = 58%, 187 KB/s], Decompressed: 4023
Downloaded: 4878 file(s) [attempted 4878/8232 = 59%, 696 KB/s], Decompressed: 4023
Downloaded: 4916 file(s) [attempted 4916/8232 = 59%, 553 KB/s], Decompressed: 4023
Downloaded: 4961 file(s) [attempted 4961/8232 = 60%, 128 KB/s], Decompressed: 4023
Downloaded: 4998 file(s) [attempted 4998/8232 = 60%, 440 KB/s], Decompressed: 4023
Downloaded: 5046 file(s) [attempted 5046/8232 = 61%, 1392 KB/s], Decompressed: 4023
Downloaded: 5091 file(s) [attempted 5091/8232 = 61%, 120 KB/s], Decompressed: 4023
Downloaded: 5125 file(s) [attempted 5125/8232 = 62%, 36 KB/s], Decompressed: 4023
Downloaded: 5169 file(s) [attempted 5169/8232 = 62%, 34 KB/s], Decompressed: 4023
Downloaded: 5217 file(s) [attempted 5217/8232 = 63%, 728 KB/s], Decompressed: 4023
Downloaded: 5258 file(s) [attempted 5258/8232 = 63%, 70 KB/s], Decompressed: 4023
Downloaded: 5299 file(s) [attempted 5299/8232 = 64%, 149 KB/s], Decompressed: 4023
Downloaded: 5344 file(s) [attempted 5344/8232 = 64%, 63 KB/s], Decompressed: 4023
Downloaded: 5388 file(s) [attempted 5388/8232 = 65%, 83 KB/s], Decompressed: 4023
Downloaded: 5426 file(s) [attempted 5426/8232 = 65%, 137 KB/s], Decompressed: 4023
Downloaded: 5471 file(s) [attempted 5471/8232 = 66%, 1071 KB/s], Decompressed: 4023
Downloaded: 5512 file(s) [attempted 5512/8232 = 66%, 1466 KB/s], Decompressed: 4023
Downloaded: 5556 file(s) [attempted 5556/8232 = 67%, 416 KB/s], Decompressed: 4023
Downloaded: 5601 file(s) [attempted 5601/8232 = 68%, 32 KB/s], Decompressed: 4023
Downloaded: 5638 file(s) [attempted 5638/8232 = 68%, 115 KB/s], Decompressed: 4023
Downloaded: 5679 file(s) [attempted 5679/8232 = 68%, 94 KB/s], Decompressed: 4023
Downloaded: 5724 file(s) [attempted 5724/8232 = 69%, 187 KB/s], Decompressed: 4023
Downloaded: 5761 file(s) [attempted 5761/8232 = 69%, 1859 KB/s], Decompressed: 4796
Downloaded: 5809 file(s) [attempted 5809/8232 = 70%, 355 KB/s], Decompressed: 4796
Downloaded: 5854 file(s) [attempted 5854/8232 = 71%, 506 KB/s], Decompressed: 4796
Downloaded: 5892 file(s) [attempted 5892/8232 = 71%, 56 KB/s], Decompressed: 4796
Downloaded: 5936 file(s) [attempted 5936/8232 = 72%, 142 KB/s], Decompressed: 4796
Downloaded: 5977 file(s) [attempted 5977/8232 = 72%, 378 KB/s], Decompressed: 4796
Downloaded: 6011 file(s) [attempted 6011/8232 = 73%, 187 KB/s], Decompressed: 4796
Downloaded: 6052 file(s) [attempted 6052/8232 = 73%, 527 KB/s], Decompressed: 4796
Downloaded: 6093 file(s) [attempted 6093/8232 = 74%, 326 KB/s], Decompressed: 4796
Downloaded: 6135 file(s) [attempted 6135/8232 = 74%, 64 KB/s], Decompressed: 4796
Downloaded: 6179 file(s) [attempted 6179/8232 = 75%, 43 KB/s], Decompressed: 4796
Downloaded: 6217 file(s) [attempted 6217/8232 = 75%, 87 KB/s], Decompressed: 4796
Downloaded: 6261 file(s) [attempted 6261/8232 = 76%, 562 KB/s], Decompressed: 4796
Downloaded: 6299 file(s) [attempted 6299/8232 = 76%, 327 KB/s], Decompressed: 4796
Downloaded: 6343 file(s) [attempted 6343/8232 = 77%, 43 KB/s], Decompressed: 4796
Downloaded: 6384 file(s) [attempted 6384/8232 = 77%, 85 KB/s], Decompressed: 4796
Downloaded: 6429 file(s) [attempted 6429/8232 = 78%, 128 KB/s], Decompressed: 4796
Downloaded: 6470 file(s) [attempted 6470/8232 = 78%, 978 KB/s], Decompressed: 4796
Downloaded: 6511 file(s) [attempted 6511/8232 = 79%, 96 KB/s], Decompressed: 4796
Downloaded: 6549 file(s) [attempted 6549/8232 = 79%, 124 KB/s], Decompressed: 4796
Downloaded: 6590 file(s) [attempted 6590/8232 = 80%, 1109 KB/s], Decompressed: 4796
Downloaded: 6634 file(s) [attempted 6634/8232 = 80%, 42 KB/s], Decompressed: 4796
Downloaded: 6679 file(s) [attempted 6679/8232 = 81%, 57 KB/s], Decompressed: 4796
Downloaded: 6716 file(s) [attempted 6716/8232 = 81%, 174 KB/s], Decompressed: 4796
Downloaded: 6757 file(s) [attempted 6757/8232 = 82%, 245 KB/s], Decompressed: 4796
Downloaded: 6798 file(s) [attempted 6798/8232 = 82%, 489 KB/s], Decompressed: 4796
Downloaded: 6846 file(s) [attempted 6846/8232 = 83%, 104 KB/s], Decompressed: 5744
Downloaded: 6894 file(s) [attempted 6894/8232 = 83%, 623 KB/s], Decompressed: 5744
Downloaded: 6935 file(s) [attempted 6935/8232 = 84%, 252 KB/s], Decompressed: 5744
Downloaded: 6976 file(s) [attempted 6976/8232 = 84%, 482 KB/s], Decompressed: 5744
Downloaded: 7017 file(s) [attempted 7017/8232 = 85%, 252 KB/s], Decompressed: 5744
Downloaded: 7055 file(s) [attempted 7055/8232 = 85%, 413 KB/s], Decompressed: 5744
Downloaded: 7100 file(s) [attempted 7100/8232 = 86%, 628 KB/s], Decompressed: 5744
Downloaded: 7144 file(s) [attempted 7144/8232 = 86%, 22 KB/s], Decompressed: 5744
Downloaded: 7185 file(s) [attempted 7185/8232 = 87%, 183 KB/s], Decompressed: 5744
Downloaded: 7226 file(s) [attempted 7226/8232 = 87%, 199 KB/s], Decompressed: 5744
Downloaded: 7267 file(s) [attempted 7267/8232 = 88%, 308 KB/s], Decompressed: 5744
Downloaded: 7308 file(s) [attempted 7308/8232 = 88%, 242 KB/s], Decompressed: 5744
Downloaded: 7349 file(s) [attempted 7349/8232 = 89%, 207 KB/s], Decompressed: 5744
Downloaded: 7391 file(s) [attempted 7391/8232 = 89%, 139 KB/s], Decompressed: 5744
Downloaded: 7435 file(s) [attempted 7435/8232 = 90%, 150 KB/s], Decompressed: 5744
Downloaded: 7480 file(s) [attempted 7480/8232 = 90%, 655 KB/s], Decompressed: 5744
Downloaded: 7524 file(s) [attempted 7524/8232 = 91%, 150 KB/s], Decompressed: 5744
Downloaded: 7568 file(s) [attempted 7568/8232 = 91%, 125 KB/s], Decompressed: 5744
Downloaded: 7610 file(s) [attempted 7610/8232 = 92%, 88 KB/s], Decompressed: 5744
Downloaded: 7654 file(s) [attempted 7654/8232 = 92%, 444 KB/s], Decompressed: 5744
Downloaded: 7688 file(s) [attempted 7688/8232 = 93%, 3517 KB/s], Decompressed: 5744
Downloaded: 7733 file(s) [attempted 7733/8232 = 93%, 1661 KB/s], Decompressed: 5744
Downloaded: 7774 file(s) [attempted 7774/8232 = 94%, 592 KB/s], Decompressed: 5744
Downloaded: 7818 file(s) [attempted 7818/8232 = 94%, 550 KB/s], Decompressed: 5744
Downloaded: 7859 file(s) [attempted 7859/8232 = 95%, 638 KB/s], Decompressed: 5744
Downloaded: 7897 file(s) [attempted 7897/8232 = 95%, 406 KB/s], Decompressed: 5744
Downloaded: 7942 file(s) [attempted 7942/8232 = 96%, 101 KB/s], Decompressed: 5744
Downloaded: 7986 file(s) [attempted 7986/8232 = 97%, 1561 KB/s], Decompressed: 5744
Downloaded: 8027 file(s) [attempted 8027/8232 = 97%, 202 KB/s], Decompressed: 5744
Downloaded: 8065 file(s) [attempted 8065/8232 = 97%, 130 KB/s], Decompressed: 5744
Downloaded: 8106 file(s) [attempted 8106/8232 = 98%, 635 KB/s], Decompressed: 5744
Downloaded: 8150 file(s) [attempted 8150/8232 = 99%, 411 KB/s], Decompressed: 5744
Downloaded: 8191 file(s) [attempted 8191/8232 = 99%, 31 KB/s], Decompressed: 6843
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 271 KB/s], Decompressed: 6843
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 271 KB/s], Decompressed: 6843
lean_checker exit 0
lake build
✔ [2765/2780] Built Architect.Command (3.1s)
✔ [2809/2831] Built Architect.Basic (3.6s)
✔ [2812/2831] Built Architect.Tactic (1.6s)
✔ [2813/2831] Built Architect.CollectUsed (1.4s)
✔ [2817/2838] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (4.1s)
✔ [2821/2853] Built PrimeNumberTheoremAnd.Auxiliary (7.8s)
✔ [2885/2906] Built Architect.Content (1.5s)
✔ [2887/2909] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (3.5s)
✔ [2897/2954] Built Architect.Attribute (2.7s)
✔ [3163/3277] Built Architect.Output (3.3s)
✔ [3440/3464] Built Architect.Load (1.4s)
✔ [3443/3468] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.6s)
✔ [3447/3469] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (2.3s)
✔ [3472/3505] Built Architect (1.3s)
✔ [3485/3505] Built PrimeNumberTheoremAnd.Sobolev (14s)
✔ [3486/3505] Built PrimeNumberTheoremAnd.SmoothExistence (4.9s)
✔ [3487/3507] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (6.2s)
✔ [3490/3507] Built PrimeNumberTheoremAnd.ZetaConj (6.1s)
✔ [3491/3507] Built PrimeNumberTheoremAnd.Rectangle (6.5s)
✔ [3495/3508] Built PrimeNumberTheoremAnd.Fourier (5.6s)
✔ [3496/3511] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (7.1s)
✔ [3498/3521] Built PrimeNumberTheoremAnd.Defs (9.6s)
✔ [3583/3606] Built PrimeNumberTheoremAnd.HadamardFactorization (2.1s)
✔ [3584/3612] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (16s)
✔ [3587/3612] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (11s)
✔ [3588/3613] Built PrimeNumberTheoremAnd.MellinCalculus (21s)
✔ [3592/3613] Built PrimeNumberTheoremAnd.HoffsteinLockhart (3.3s)
✔ [3594/3613] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.8s)
✔ [3597/3614] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (5.6s)
✔ [3600/3617] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (7.3s)
⚠ [3602/3617] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (9.6s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3603/3617] Built PrimeNumberTheoremAnd.BrunTitchmarsh (13s)
✔ [3606/3635] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (21s)
✔ [3655/3682] Built PrimeNumberTheoremAnd.IEANTN.KLN (6.9s)
✔ [3665/3686] Built LeanCert.Core.Interval (6.2s)
✔ [3666/3687] Built LeanCert.Core.Expr (11s)
✔ [3667/3687] Built LeanCert.Core.Support (8.7s)
✔ [3668/3687] Built LeanCert.Core.IntervalRat.Basic (19s)
✔ [3669/3688] Built LeanCert.Meta.Numeral (8.6s)
✔ [3670/3688] Built LeanCert.Core.IntervalRat.Transcendental (10s)
✔ [3671/3688] Built LeanCert.Tactic.IntervalAuto.Types (7.2s)
✔ [3672/3688] Built LeanCert.Tactic.IntervalAuto.Extract (6.1s)
✔ [3673/3689] Built PrimeNumberTheoremAnd.ZetaBounds (69s)
✔ [3674/3693] Built LeanCert.Meta.ToExpr (8.6s)
✔ [3675/3693] Built LeanCert.Core.IntervalRat.LogReduction (9.6s)
✔ [3676/3694] Built LeanCert.Tactic.IntervalAuto.Norm (6.5s)
✔ [3678/3694] Built LeanCert.Tactic.IntervalAuto.Parse (11s)
⚠ [3679/3696] Built PrimeNumberTheoremAnd.Wiener (82s)
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
✔ [3680/3697] Built LeanCert.Core.DerivativeIntervals (17s)
✔ [3681/3699] Built LeanCert.Tactic.IntervalAuto.Diagnostic (11s)
✔ [3682/3699] Built LeanCert.Core.Taylor (20s)
✔ [3683/3700] Built LeanCert.Core.IntervalRat.Taylor (42s)
✔ [3684/3700] Built LeanCert.Core.IntervalRat.TrigReduced (28s)
ℹ [3685/3702] Built PrimeNumberTheoremAnd.MediumPNT (131s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3686/3703] Built LeanCert.Core.IntervalReal (6.5s)
✔ [3687/3703] Built PrimeNumberTheoremAnd.Consequences (115s)
✔ [3688/3710] Built LeanCert.Core.IntervalRealEndpoints (8.3s)
⚠ [3689/3710] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (155s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3690/3729] Built LeanCert.Contrib.Sinc (10s)
⚠ [3701/3732] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (8.6s)
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`
✔ [3702/3737] Built LeanCert.Engine.Eval.Core (14s)
✔ [3703/3737] Built LeanCert.Core.Dyadic (5.5s)
✔ [3704/3737] Built LeanCert.Engine.Eval.Extended (5.3s)
✔ [3705/3740] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (5.8s)
✔ [3706/3740] Built LeanCert.Engine.Affine.Basic (9.7s)
⚠ [3707/3741] Built PrimeNumberTheoremAnd.StrongPNT (39s)
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`
✔ [3708/3743] Built LeanCert.Tactic.Bound.Lemmas (5.0s)
✔ [3709/3746] Built LeanCert.Engine.IntervalEval (4.2s)
✔ [3710/3746] Built LeanCert.Core.IntervalDyadic (11s)
✔ [3711/3746] Built LeanCert.Engine.Affine.Nonlinear (6.4s)
✔ [3712/3746] Built PrimeNumberTheoremAnd.BorelCaratheodory (8.1s)
✔ [3713/3749] Built LeanCert.Engine.Optimization.Box (3.1s)
✔ [3714/3749] Built LeanCert.Engine.RootFinding.Basic (5.4s)
✔ [3715/3749] Built LeanCert.Engine.AD.Basic (2.5s)
✔ [3716/3749] Built LeanCert.Engine.IntervalEvalDyadic (4.5s)
⚠ [3717/3752] Built PrimeNumberTheoremAnd.DerivativeBound (3.3s)
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
✔ [3718/3752] Built LeanCert.Engine.Affine.Transcendental (4.2s)
✔ [3719/3752] Built LeanCert.Engine.TaylorModel.Core (8.4s)
✔ [3720/3754] Built LeanCert.Validity.DyadicBounds (3.0s)
✔ [3721/3754] Built LeanCert.Engine.AD.Transcendental (3.7s)
✔ [3722/3754] Built LeanCert.Engine.RootFinding.Bisection (3.0s)
✔ [3723/3754] Built LeanCert.Engine.Integrate (5.2s)
✔ [3724/3754] Built LeanCert.Engine.TaylorModel.Special (2.2s)
✔ [3725/3756] Built LeanCert.Engine.IntervalEvalAffine (2.9s)
✔ [3726/3762] Built LeanCert.Engine.AD.Eval (3.3s)
✔ [3727/3771] Built LeanCert.Engine.TaylorModel.ExpLog (9.7s)
✔ [3728/3771] Built LeanCert.Engine.AD.Correctness (4.7s)
✔ [3730/3772] Built LeanCert.Engine.TaylorModel.Hyperbolic (11s)
✔ [3731/3772] Built LeanCert.Engine.TaylorModel.Trig (11s)
✔ [3732/3773] Built LeanCert.Engine.AD.Computable (4.3s)
✔ [3733/3774] Built LeanCert.Engine.TaylorModel.Log1p (6.6s)
✔ [3735/3774] Built LeanCert.Engine.TaylorModel.Functions (2.5s)
✔ [3737/3774] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (9.0s)
✔ [3739/3774] Built LeanCert.Engine.AD.PartialCorrectness (7.7s)
⚠ [3740/3778] Built LeanCert.Examples.Li2Bounds (4.2s)
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3741/3780] Built LeanCert.Engine.AD (3.1s)
✔ [3743/3780] Built LeanCert.Engine.TaylorModel.Expr (5.3s)
✔ [3744/3782] Built LeanCert.Meta.ProveSupported (2.9s)
✔ [3748/3782] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (4.0s)
✔ [3749/3782] Built LeanCert.Engine.TaylorModel (2.3s)
✔ [3750/3785] Built LeanCert.Engine.Optimize (5.1s)
✔ [3754/3785] Built LeanCert.Meta.ProveContinuous (3.1s)
✔ [3755/3785] Built LeanCert.Engine.IntervalEvalRefined (2.0s)
✔ [3756/3786] Built LeanCert.Tactic.IntervalAuto.ProveCommon (4.3s)
✔ [3760/3786] Built LeanCert.Engine.RootFinding.Newton (3.8s)
✔ [3763/3800] Built LeanCert.Tactic.IntervalAuto.Basic (2.3s)
✔ [3866/3901] Built LeanCert.Engine.Optimization.Gradient (4.5s)
✔ [3867/3901] Built LeanCert.Tactic.VecUtil (3.1s)
✔ [3868/3901] Built LeanCert.Engine.RootFinding.MVTBounds (6.3s)
✔ [3869/3903] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (25s)
✔ [3871/3903] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (2.7s)
✔ [3872/3904] Built LeanCert.Tactic.FinSumExpand (2.0s)
✔ [3873/3904] Built LeanCert.Engine.RootFinding.Contraction (8.6s)
✔ [3876/3914] Built LeanCert.Engine.RootFinding.Main (4.1s)
✔ [3879/3914] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (15s)
✔ [3880/3914] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (22s)
✔ [3881/3916] Built LeanCert.Engine.Optimization.Global (21s)
✔ [3882/3921] Built LeanCert.Engine.Chebyshev.Psi (4.3s)
✔ [3883/3921] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (3.3s)
✔ [3885/3921] Built LeanCert.Engine.ChebyshevPsi (2.7s)
✔ [3887/3921] Built LeanCert.Engine.Optimization.BoundVerify (4.9s)
✔ [3890/3923] Built PrimeNumberTheoremAnd.Tactic.Simprocs (2.3s)
✔ [3891/3924] Built PrimeCert.Interval (5.9s)
✔ [3892/3925] Built LeanCert.Validity.Bounds (12s)
✔ [3893/3925] Built PrimeCert.Meta.PrimeCert (3.6s)
✔ [3894/3925] Built LeanCert.Tactic.IntervalAuto.Multivariate (6.6s)
✔ [3895/3925] Built LeanCert.Tactic.IntervalAuto.OptBound (3.6s)
✔ [3896/3926] Built LeanCert.Tactic.IntervalAuto.RootBound (4.0s)
✔ [3897/3927] Built PrimeCert.PredMod (400ms)
✔ [3898/3927] Built PrimeCert.Meta.SmallPrime (1.6s)
✔ [3899/3938] Built PrimeCert.PowMod (2.8s)
⚠ [3902/3938] Built PrimeCert.Pocklington (4.8s)
warning: PrimeCert/Pocklington.lean:60:22: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3903/3938] Built PrimeCert.Wieferich (3.9s)
✔ [3904/3938] Built LeanCert.Tactic.IntervalAuto.Bound (33s)
✔ [3905/3938] Built PrimeCert.SmallPrimes (3.9s)
⚠ [3906/3938] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (41s)
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`
⚠ [3907/3938] Built PrimeCert.Pocklington3 (8.8s)
warning: PrimeCert/Pocklington3.lean:39:8: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3908/3948] Built LeanCert.Tactic.IntervalAuto.Subdiv (12s)
✔ [3909/3948] Built PrimeCert (2.5s)
✔ [3911/3951] Built LeanCert.Tactic.IntervalAuto.Adaptive (9.5s)
✔ [3914/3960] Built LeanCert.Tactic.IntervalAuto.PointIneq (19s)
✔ [3917/3960] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (6.5s)
✔ [3918/3960] Built LeanCert.Tactic.IntervalAuto (3.2s)
✔ [3920/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (10s)
⚠ [3921/3960] Built PrimeNumberTheoremAnd.IEANTN.Mertens (21s)
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`
✔ [3922/3960] Built LeanCert.Engine.Chebyshev.Theta (14s)
⚠ [3923/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (96s)
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`
✔ [3924/3960] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (2.9s)
⚠ [3925/3960] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (7.6s)
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`
✔ [3927/3960] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (25s)
✔ [3928/3960] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (10s)
✔ [3929/3960] Built LeanCert.Engine.ChebyshevTheta (2.3s)
✔ [3930/3960] Built PrimeNumberTheoremAnd.IEANTN.LogTables (8.2s)
⚠ [3932/3960] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (5.3s)
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`
✔ [3933/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (5.6s)
✔ [3934/3960] Built PrimeNumberTheoremAnd.PerronFormula (11s)
⚠ [3935/3960] Built LeanCert.Examples.BKLNW_a2_pow2 (33s)
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.Buthe (21s)
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`
✔ [3937/3960] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (16s)
⚠ [3938/3960] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (26s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
ℹ [3939/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (40s)
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.
✔ [3940/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (4.0s)
✔ [3941/3960] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (34s)
⚠ [3942/3960] Built LeanCert.Examples.BKLNW_a2_bounds (6.0s)
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:136:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:138:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:142:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:144:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:148:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:150:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:154:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:156:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:160:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:162:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:166:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:168:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:172:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:174:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:178:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:180:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:184:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:186:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:190:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:192:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:196:6: declaration uses `sorry`
warning: LeanCert/Examples/BKLNW_a2_bounds.lean:198:6: declaration uses `sorry`
⚠ [3943/3960] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (10s)
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`
⚠ [3944/3960] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (7.8s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:152:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:164:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:176:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:217:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:353:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:367:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:382:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:401:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:417:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:463:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:472:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:487:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:528:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:633:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:658:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:702:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:712:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:725:8: declaration uses `sorry`
✔ [3945/3960] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (3.0s)
⚠ [3946/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (6.4s)
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`
✔ [3947/3960] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (86s)
✔ [3948/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (128s)
⚠ [3949/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1356:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1485:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2151:8: declaration uses `sorry`
✔ [3950/3960] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (8.0s)
⚠ [3951/3960] Built PrimeNumberTheoremAnd.IEANTN.Dusart (24s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:72:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:88:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:280:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:316:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:327:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:338:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:349:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:360:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:372:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:394:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:405:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:416:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:626:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:686:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:711:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:734:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:753:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:765:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:789:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:801:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:813:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:825:8: declaration uses `sorry`
✔ [3952/3960] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (12s)
⚠ [3953/3960] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (55s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3621:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4064:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4086:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4113:8: declaration uses `sorry`
⚠ [3954/3960] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (19s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [3955/3960] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (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 (10s)
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 (37s)
✔ [3958/3960] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (67s)
✔ [3959/3960] Built PrimeNumberTheoremAnd (2.5s)
Build completed successfully (3960 jobs).
blueprint_build exit 0
lake build :blueprint
✔ [9/35] Built Architect.Command:c.o (409ms)
✔ [10/35] Built Batteries.Lean.NameMapAttribute:c.o (650ms)
✔ [13/35] Built Architect.Basic:c.o (792ms)
✔ [14/35] Built Architect.CollectUsed:c.o (166ms)
✔ [15/35] Built Architect.Tactic:c.o (404ms)
✔ [18/35] Built Architect.Content:c.o (184ms)
✔ [20/42] Built Architect.Load:c.o (171ms)
✔ [21/42] Built Architect:c.o (67ms)
✔ [124/135] Built Architect.Attribute:c.o (832ms)
✔ [125/135] Built Cli:c.o (50ms)
✔ [128/187] Built Cli.Extensions:c.o (506ms)
✔ [174/231] Built Architect.Output:c.o (1.4s)
✔ [792/913] Built Main (1.1s)
✔ [1016/1161] Built Main:c.o (230ms)
ℹ [3457/3678] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3474/3678] 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`
⚠ [3610/3678] Replayed PrimeNumberTheoremAnd.DerivativeBound
warning: PrimeNumberTheoremAnd/DerivativeBound.lean:52:8: declaration uses `sorry`
⚠ [3622/3678] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3638/3901] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
⚠ [3686/3901] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3687/3901] 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/3901] 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/3901] 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.5s)
✔ [3980/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (1.9s)
✔ [3981/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (2.3s)
✔ [3982/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (2.2s)
✔ [3983/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (1.9s)
✔ [3984/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (2.0s)
✔ [3985/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.4s)
✔ [3986/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (12s)
✔ [3987/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (11s)
✔ [3988/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (1.1s)
✔ [3989/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (3.8s)
✔ [3990/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (48s)
✔ [3991/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.1s)
✔ [3992/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.6s)
✔ [3993/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (2.0s)
✔ [3994/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.1s)
✔ [3995/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.1s)
✔ [3996/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (2.0s)
✔ [3997/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (2.1s)
✔ [3998/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (8.0s)
✔ [3999/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (34s)
✔ [4000/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (13s)
✔ [4001/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.DerivativeBound:blueprint (3.8s)
✔ [4002/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.1s)
✔ [4003/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (2.6s)
✔ [4004/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (990ms)
✔ [4005/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (2.5s)
✔ [4006/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (10s)
✔ [4007/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (2.7s)
✔ [4008/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (2.4s)
✔ [4009/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (24s)
✔ [4010/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (2.8s)
✔ [4011/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.4s)
✔ [4012/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.1s)
✔ [4013/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.1s)
✔ [4014/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (15s)
✔ [4015/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (5.6s)
✔ [4016/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (2.4s)
✔ [4017/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.2s)
✔ [4018/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (1.9s)
✔ [4019/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.4s)
✔ [4020/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.3s)
✔ [4021/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (2.4s)
✔ [4022/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (19s)
✔ [4023/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (2.7s)
✔ [4024/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.1s)
✔ [4025/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (16s)
✔ [4026/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (4.5s)
✔ [4027/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4028/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.8s)
✔ [4029/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
✔ [4030/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (16s)
✔ [4031/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4032/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.4s)
✔ [4033/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (2.2s)
✔ [4034/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (3.2s)
✔ [4035/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4036/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (16s)
✔ [4037/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (31s)
✔ [4038/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (1.2s)
✔ [4039/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (1.9s)
✔ [4040/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (2.9s)
✔ [4041/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (44s)
✔ [4042/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.4s)
✔ [4043/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.7s)
✔ [4044/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (9.1s)
✔ [4045/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (2.1s)
✔ [4046/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4047/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (32s)
✔ [4048/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4049/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.6s)
✔ [4050/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (8.2s)
✔ [4051/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4052/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (37s)
✔ [4053/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (2.2s)
✔ [4054/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (21s)
✔ [4055/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (2.8s)
✔ [4056/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (57s)
✔ [4057/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (23s)
✔ [4058/4060] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (62s)
ℹ [4059/4061] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (54ms)
info: Blueprint indexing
Build completed successfully (4061 jobs).
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh