Verification run

Run 8

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via github_backfill

failed commit 91ce7f4bee94 toolchain lean-v4-29-0 prover lean took 4h 23m · finished 6w ago

./.apodeixis/tools/lean-semantic-extract.sh failed with exit code none (process did not exit cleanly) (toolchain lean-v4-29-0, command: elan run leanprover/lean4:v4.29.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase ./.apodeixis/tools/lean-semantic-extract.sh)

Open project

Package inputs

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

Trust verification

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

(verification not run)

Manifest

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

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 1s · created 6/4/2026, 10:15:45 AM

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

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

git_checkout exit 128 duration 3 ms · created 6/4/2026, 10:15:45 AM

git checkout 91ce7f4bee948130b16b3f7c97fcb15f9a3b7b7e

fatal: reference is not a tree: 91ce7f4bee948130b16b3f7c97fcb15f9a3b7b7e

git_checkout exit 0 duration 828 ms · created 6/4/2026, 10:15:45 AM

git fetch --depth 1 origin 91ce7f4bee948130b16b3f7c97fcb15f9a3b7b7e

From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd
 * branch            91ce7f4bee948130b16b3f7c97fcb15f9a3b7b7e -> FETCH_HEAD

git_checkout exit 0 duration 46 ms · created 6/4/2026, 10:15:45 AM

git checkout 91ce7f4bee948130b16b3f7c97fcb15f9a3b7b7e (after fetch)

Note: switching to '91ce7f4bee948130b16b3f7c97fcb15f9a3b7b7e'.

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 91ce7f4 [StrongPNT] delete DerivativeBound.lean (#1471)

lake_cache exit 0 duration 1m 36s · created 6/4/2026, 10:15:45 AM

lake exe cache get

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

info: PrimeCert: cloning https://github.com/b-mehta/PrimeCert
info: PrimeCert: checking out revision '2030255c7e3efb07074171879ec920b500ee0e58'
info: leancert: cloning https://github.com/alerad/leancert
info: leancert: checking out revision '6237c769e79d4cefec17f5f3c40d288a9baa01e5'
info: 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: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '48d5698bc464786347c1b0d859b18f938420f060'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '7152850e7b216a0d409701617721b6e469d34bf6'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '707efb56d0696634e9e965523a1bbe9ac6ce141d'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '756e3321fd3b02a85ffda19fef789916223e578c'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '7802da01beb530bf051ab657443f9cd9bc3e1a29'
✔ [2/22] Built Cache.Init (448ms)
✔ [3/22] Built Cache.Lean (500ms)
✔ [4/22] Built Cache.Lean:c.o (361ms)
✔ [5/22] Built Cache.Init:c.o (369ms)
✔ [6/22] Built Cache.IO (1.4s)
✔ [7/22] Built Cache.Hashing (757ms)
✔ [8/22] Built Cache.Hashing:c.o (427ms)
✔ [9/22] Built Cache.IO:c.o (1.3s)
✔ [15/22] Built Batteries.Data.String.Basic:c.o (138ms)
✔ [16/22] Built Batteries.Data.Array.Match:c.o (214ms)
✔ [17/22] Built Batteries.Data.String.Matcher:c.o (181ms)
✔ [18/22] Built Cache.Requests (1.9s)
✔ [19/22] Built Cache.Main (782ms)
✔ [20/22] Built Cache.Main:c.o (504ms)
✔ [21/22] Built Cache.Requests:c.o (2.0s)
✔ [22/22] Built cache:exe (2.6s)
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

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

100 1119k  100 1119k    0     0  2700k      0 --:--:-- --:--:-- --:--:-- 2700k


Downloaded: 1 file(s) [attempted 1/8232 = 0%, 8 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8232 = 0%, 1 KB/s], Decompressed: 9
Downloaded: 41 file(s) [attempted 41/8232 = 0%, 29 KB/s], Decompressed: 29
Downloaded: 70 file(s) [attempted 70/8232 = 0%, 260 KB/s], Decompressed: 54
Downloaded: 96 file(s) [attempted 96/8232 = 1%, 69 KB/s], Decompressed: 86
Downloaded: 127 file(s) [attempted 127/8232 = 1%, 194 KB/s], Decompressed: 106
Downloaded: 168 file(s) [attempted 168/8232 = 2%, 350 KB/s], Decompressed: 141
Downloaded: 210 file(s) [attempted 210/8232 = 2%, 338 KB/s], Decompressed: 161
Downloaded: 247 file(s) [attempted 247/8232 = 3%, 312 KB/s], Decompressed: 182
Downloaded: 288 file(s) [attempted 288/8232 = 3%, 91 KB/s], Decompressed: 216
Downloaded: 333 file(s) [attempted 333/8232 = 4%, 47 KB/s], Decompressed: 258
Downloaded: 369 file(s) [attempted 369/8232 = 4%, 428 KB/s], Decompressed: 258
Downloaded: 415 file(s) [attempted 415/8232 = 5%, 59 KB/s], Decompressed: 316
Downloaded: 463 file(s) [attempted 463/8232 = 5%, 76 KB/s], Decompressed: 384
Downloaded: 504 file(s) [attempted 504/8232 = 6%, 1583 KB/s], Decompressed: 384
Downloaded: 542 file(s) [attempted 542/8232 = 6%, 259 KB/s], Decompressed: 384
Downloaded: 586 file(s) [attempted 586/8232 = 7%, 335 KB/s], Decompressed: 463
Downloaded: 624 file(s) [attempted 624/8232 = 7%, 287 KB/s], Decompressed: 463
Downloaded: 665 file(s) [attempted 665/8232 = 8%, 100 KB/s], Decompressed: 463
Downloaded: 710 file(s) [attempted 710/8232 = 8%, 43 KB/s], Decompressed: 559
Downloaded: 751 file(s) [attempted 751/8232 = 9%, 193 KB/s], Decompressed: 559
Downloaded: 792 file(s) [attempted 792/8232 = 9%, 609 KB/s], Decompressed: 559
Downloaded: 840 file(s) [attempted 840/8232 = 10%, 164 KB/s], Decompressed: 559
Downloaded: 884 file(s) [attempted 884/8232 = 10%, 371 KB/s], Decompressed: 703
Downloaded: 922 file(s) [attempted 922/8232 = 11%, 172 KB/s], Decompressed: 703
Downloaded: 963 file(s) [attempted 963/8232 = 11%, 598 KB/s], Decompressed: 703
Downloaded: 1004 file(s) [attempted 1004/8232 = 12%, 801 KB/s], Decompressed: 703
Downloaded: 1045 file(s) [attempted 1045/8232 = 12%, 58 KB/s], Decompressed: 860
Downloaded: 1090 file(s) [attempted 1090/8232 = 13%, 634 KB/s], Decompressed: 860
Downloaded: 1131 file(s) [attempted 1131/8232 = 13%, 160 KB/s], Decompressed: 860
Downloaded: 1172 file(s) [attempted 1172/8232 = 14%, 76 KB/s], Decompressed: 860
Downloaded: 1217 file(s) [attempted 1217/8232 = 14%, 467 KB/s], Decompressed: 860
Downloaded: 1258 file(s) [attempted 1258/8232 = 15%, 216 KB/s], Decompressed: 1039
Downloaded: 1295 file(s) [attempted 1295/8232 = 15%, 172 KB/s], Decompressed: 1039
Downloaded: 1340 file(s) [attempted 1340/8232 = 16%, 605 KB/s], Decompressed: 1039
Downloaded: 1381 file(s) [attempted 1381/8232 = 16%, 418 KB/s], Decompressed: 1039
Downloaded: 1425 file(s) [attempted 1425/8232 = 17%, 48 KB/s], Decompressed: 1039
Downloaded: 1463 file(s) [attempted 1463/8232 = 17%, 410 KB/s], Decompressed: 1039
Downloaded: 1501 file(s) [attempted 1501/8232 = 18%, 53 KB/s], Decompressed: 1039
Downloaded: 1545 file(s) [attempted 1545/8232 = 18%, 119 KB/s], Decompressed: 1254
Downloaded: 1590 file(s) [attempted 1590/8232 = 19%, 188 KB/s], Decompressed: 1254
Downloaded: 1634 file(s) [attempted 1634/8232 = 19%, 59 KB/s], Decompressed: 1254
Downloaded: 1675 file(s) [attempted 1675/8232 = 20%, 684 KB/s], Decompressed: 1254
Downloaded: 1713 file(s) [attempted 1713/8232 = 20%, 24 KB/s], Decompressed: 1254
Downloaded: 1750 file(s) [attempted 1750/8232 = 21%, 193 KB/s], Decompressed: 1254
Downloaded: 1795 file(s) [attempted 1795/8232 = 21%, 292 KB/s], Decompressed: 1254
Downloaded: 1836 file(s) [attempted 1836/8232 = 22%, 283 KB/s], Decompressed: 1254
Downloaded: 1880 file(s) [attempted 1880/8232 = 22%, 485 KB/s], Decompressed: 1528
Downloaded: 1918 file(s) [attempted 1918/8232 = 23%, 238 KB/s], Decompressed: 1528
Downloaded: 1956 file(s) [attempted 1956/8232 = 23%, 123 KB/s], Decompressed: 1528
Downloaded: 1990 file(s) [attempted 1990/8232 = 24%, 92 KB/s], Decompressed: 1528
Downloaded: 2028 file(s) [attempted 2028/8232 = 24%, 59 KB/s], Decompressed: 1528
Downloaded: 2072 file(s) [attempted 2072/8232 = 25%, 350 KB/s], Decompressed: 1528
Downloaded: 2117 file(s) [attempted 2117/8232 = 25%, 159 KB/s], Decompressed: 1528
Downloaded: 2164 file(s) [attempted 2164/8232 = 26%, 145 KB/s], Decompressed: 1528
Downloaded: 2209 file(s) [attempted 2209/8232 = 26%, 47 KB/s], Decompressed: 1843
Downloaded: 2250 file(s) [attempted 2250/8232 = 27%, 104 KB/s], Decompressed: 1843
Downloaded: 2288 file(s) [attempted 2288/8232 = 27%, 194 KB/s], Decompressed: 1843
Downloaded: 2329 file(s) [attempted 2329/8232 = 28%, 98 KB/s], Decompressed: 1843
Downloaded: 2366 file(s) [attempted 2366/8232 = 28%, 106 KB/s], Decompressed: 1843
Downloaded: 2411 file(s) [attempted 2411/8232 = 29%, 2747 KB/s], Decompressed: 1843
Downloaded: 2449 file(s) [attempted 2449/8232 = 29%, 86 KB/s], Decompressed: 1843
Downloaded: 2486 file(s) [attempted 2486/8232 = 30%, 25 KB/s], Decompressed: 1843
Downloaded: 2531 file(s) [attempted 2531/8232 = 30%, 377 KB/s], Decompressed: 1843
Downloaded: 2575 file(s) [attempted 2575/8232 = 31%, 309 KB/s], Decompressed: 1843
Downloaded: 2616 file(s) [attempted 2616/8232 = 31%, 62 KB/s], Decompressed: 1843
Downloaded: 2657 file(s) [attempted 2657/8232 = 32%, 179 KB/s], Decompressed: 1843
Downloaded: 2698 file(s) [attempted 2698/8232 = 32%, 229 KB/s], Decompressed: 2206
Downloaded: 2739 file(s) [attempted 2739/8232 = 33%, 132 KB/s], Decompressed: 2206
Downloaded: 2784 file(s) [attempted 2784/8232 = 33%, 62 KB/s], Decompressed: 2206
Downloaded: 2828 file(s) [attempted 2828/8232 = 34%, 470 KB/s], Decompressed: 2206
Downloaded: 2873 file(s) [attempted 2873/8232 = 34%, 122 KB/s], Decompressed: 2206
Downloaded: 2914 file(s) [attempted 2914/8232 = 35%, 231 KB/s], Decompressed: 2206
Downloaded: 2952 file(s) [attempted 2952/8232 = 35%, 370 KB/s], Decompressed: 2206
Downloaded: 2993 file(s) [attempted 2993/8232 = 36%, 196 KB/s], Decompressed: 2206
Downloaded: 3030 file(s) [attempted 3030/8232 = 36%, 88 KB/s], Decompressed: 2206
Downloaded: 3075 file(s) [attempted 3075/8232 = 37%, 171 KB/s], Decompressed: 2206
Downloaded: 3112 file(s) [attempted 3112/8232 = 37%, 428 KB/s], Decompressed: 2206
Downloaded: 3154 file(s) [attempted 3154/8232 = 38%, 257 KB/s], Decompressed: 2206
Downloaded: 3195 file(s) [attempted 3195/8232 = 38%, 158 KB/s], Decompressed: 2206
Downloaded: 3239 file(s) [attempted 3239/8232 = 39%, 227 KB/s], Decompressed: 2674
Downloaded: 3277 file(s) [attempted 3277/8232 = 39%, 480 KB/s], Decompressed: 2674
Downloaded: 3318 file(s) [attempted 3318/8232 = 40%, 202 KB/s], Decompressed: 2674
Downloaded: 3355 file(s) [attempted 3355/8232 = 40%, 176 KB/s], Decompressed: 2674
Downloaded: 3393 file(s) [attempted 3393/8232 = 41%, 86 KB/s], Decompressed: 2674
Downloaded: 3441 file(s) [attempted 3441/8232 = 41%, 154 KB/s], Decompressed: 2674
Downloaded: 3482 file(s) [attempted 3482/8232 = 42%, 345 KB/s], Decompressed: 2674
Downloaded: 3523 file(s) [attempted 3523/8232 = 42%, 600 KB/s], Decompressed: 2674
Downloaded: 3561 file(s) [attempted 3561/8232 = 43%, 244 KB/s], Decompressed: 2674
Downloaded: 3602 file(s) [attempted 3602/8232 = 43%, 183 KB/s], Decompressed: 2674
Downloaded: 3646 file(s) [attempted 3646/8232 = 44%, 387 KB/s], Decompressed: 2674
Downloaded: 3694 file(s) [attempted 3694/8232 = 44%, 193 KB/s], Decompressed: 2674
Downloaded: 3732 file(s) [attempted 3732/8232 = 45%, 256 KB/s], Decompressed: 2674
Downloaded: 3770 file(s) [attempted 3770/8232 = 45%, 915 KB/s], Decompressed: 2674
Downloaded: 3814 file(s) [attempted 3814/8232 = 46%, 655 KB/s], Decompressed: 2674
Downloaded: 3855 file(s) [attempted 3855/8232 = 46%, 206 KB/s], Decompressed: 2674
Downloaded: 3900 file(s) [attempted 3900/8232 = 47%, 127 KB/s], Decompressed: 2674
Downloaded: 3941 file(s) [attempted 3941/8232 = 47%, 123 KB/s], Decompressed: 3225
Downloaded: 3982 file(s) [attempted 3982/8232 = 48%, 254 KB/s], Decompressed: 3225
Downloaded: 4019 file(s) [attempted 4019/8232 = 48%, 106 KB/s], Decompressed: 3225
Downloaded: 4061 file(s) [attempted 4061/8232 = 49%, 243 KB/s], Decompressed: 3225
Downloaded: 4108 file(s) [attempted 4108/8232 = 49%, 35 KB/s], Decompressed: 3225
Downloaded: 4150 file(s) [attempted 4150/8232 = 50%, 211 KB/s], Decompressed: 3225
Downloaded: 4197 file(s) [attempted 4197/8232 = 50%, 1075 KB/s], Decompressed: 3225
Downloaded: 4245 file(s) [attempted 4245/8232 = 51%, 449 KB/s], Decompressed: 3225
Downloaded: 4290 file(s) [attempted 4290/8232 = 52%, 344 KB/s], Decompressed: 3225
Downloaded: 4327 file(s) [attempted 4327/8232 = 52%, 517 KB/s], Decompressed: 3225
Downloaded: 4369 file(s) [attempted 4369/8232 = 53%, 184 KB/s], Decompressed: 3225
Downloaded: 4410 file(s) [attempted 4410/8232 = 53%, 109 KB/s], Decompressed: 3225
Downloaded: 4454 file(s) [attempted 4454/8232 = 54%, 173 KB/s], Decompressed: 3225
Downloaded: 4495 file(s) [attempted 4495/8232 = 54%, 491 KB/s], Decompressed: 3225
Downloaded: 4540 file(s) [attempted 4540/8232 = 55%, 597 KB/s], Decompressed: 3225
Downloaded: 4577 file(s) [attempted 4577/8232 = 55%, 93 KB/s], Decompressed: 3225
Downloaded: 4622 file(s) [attempted 4622/8232 = 56%, 603 KB/s], Decompressed: 3225
Downloaded: 4656 file(s) [attempted 4656/8232 = 56%, 595 KB/s], Decompressed: 3225
Downloaded: 4697 file(s) [attempted 4697/8232 = 57%, 92 KB/s], Decompressed: 3225
Downloaded: 4738 file(s) [attempted 4738/8232 = 57%, 265 KB/s], Decompressed: 3225
Downloaded: 4776 file(s) [attempted 4776/8232 = 58%, 473 KB/s], Decompressed: 3913
Downloaded: 4817 file(s) [attempted 4817/8232 = 58%, 419 KB/s], Decompressed: 3913
Downloaded: 4865 file(s) [attempted 4865/8232 = 59%, 53 KB/s], Decompressed: 3913
Downloaded: 4902 file(s) [attempted 4902/8232 = 59%, 34 KB/s], Decompressed: 3913
Downloaded: 4940 file(s) [attempted 4940/8232 = 60%, 514 KB/s], Decompressed: 3913
Downloaded: 4978 file(s) [attempted 4978/8232 = 60%, 75 KB/s], Decompressed: 3913
Downloaded: 5022 file(s) [attempted 5022/8232 = 61%, 123 KB/s], Decompressed: 3913
Downloaded: 5067 file(s) [attempted 5067/8232 = 61%, 172 KB/s], Decompressed: 3913
Downloaded: 5111 file(s) [attempted 5111/8232 = 62%, 76 KB/s], Decompressed: 3913
Downloaded: 5153 file(s) [attempted 5153/8232 = 62%, 263 KB/s], Decompressed: 3913
Downloaded: 5193 file(s) [attempted 5193/8232 = 63%, 1033 KB/s], Decompressed: 3913
Downloaded: 5228 file(s) [attempted 5228/8232 = 63%, 88 KB/s], Decompressed: 3913
Downloaded: 5265 file(s) [attempted 5265/8232 = 63%, 267 KB/s], Decompressed: 3913
Downloaded: 5313 file(s) [attempted 5313/8232 = 64%, 153 KB/s], Decompressed: 3913
Downloaded: 5364 file(s) [attempted 5364/8232 = 65%, 314 KB/s], Decompressed: 3913
Downloaded: 5412 file(s) [attempted 5412/8232 = 65%, 1053 KB/s], Decompressed: 3913
Downloaded: 5460 file(s) [attempted 5460/8232 = 66%, 20 KB/s], Decompressed: 3913
Downloaded: 5501 file(s) [attempted 5501/8232 = 66%, 44 KB/s], Decompressed: 3913
Downloaded: 5549 file(s) [attempted 5549/8232 = 67%, 219 KB/s], Decompressed: 3913
Downloaded: 5587 file(s) [attempted 5587/8232 = 67%, 72 KB/s], Decompressed: 3913
Downloaded: 5628 file(s) [attempted 5628/8232 = 68%, 493 KB/s], Decompressed: 3913
Downloaded: 5672 file(s) [attempted 5672/8232 = 68%, 223 KB/s], Decompressed: 3913
Downloaded: 5717 file(s) [attempted 5717/8232 = 69%, 354 KB/s], Decompressed: 3913
Downloaded: 5751 file(s) [attempted 5751/8232 = 69%, 684 KB/s], Decompressed: 3913
Downloaded: 5792 file(s) [attempted 5792/8232 = 70%, 323 KB/s], Decompressed: 4745
Downloaded: 5830 file(s) [attempted 5830/8232 = 70%, 427 KB/s], Decompressed: 4745
Downloaded: 5878 file(s) [attempted 5878/8232 = 71%, 280 KB/s], Decompressed: 4745
Downloaded: 5926 file(s) [attempted 5926/8232 = 71%, 116 KB/s], Decompressed: 4745
Downloaded: 5963 file(s) [attempted 5963/8232 = 72%, 336 KB/s], Decompressed: 4745
Downloaded: 6001 file(s) [attempted 6001/8232 = 72%, 568 KB/s], Decompressed: 4745
Downloaded: 6039 file(s) [attempted 6039/8232 = 73%, 162 KB/s], Decompressed: 4745
Downloaded: 6083 file(s) [attempted 6083/8232 = 73%, 378 KB/s], Decompressed: 4745
Downloaded: 6124 file(s) [attempted 6124/8232 = 74%, 549 KB/s], Decompressed: 4745
Downloaded: 6165 file(s) [attempted 6165/8232 = 74%, 938 KB/s], Decompressed: 4745
Downloaded: 6210 file(s) [attempted 6210/8232 = 75%, 111 KB/s], Decompressed: 4745
Downloaded: 6251 file(s) [attempted 6251/8232 = 75%, 123 KB/s], Decompressed: 4745
Downloaded: 6292 file(s) [attempted 6292/8232 = 76%, 1822 KB/s], Decompressed: 4745
Downloaded: 6333 file(s) [attempted 6333/8232 = 76%, 69 KB/s], Decompressed: 4745
Downloaded: 6377 file(s) [attempted 6377/8232 = 77%, 574 KB/s], Decompressed: 4745
Downloaded: 6412 file(s) [attempted 6412/8232 = 77%, 377 KB/s], Decompressed: 4745
Downloaded: 6453 file(s) [attempted 6453/8232 = 78%, 294 KB/s], Decompressed: 4745
Downloaded: 6497 file(s) [attempted 6497/8232 = 78%, 187 KB/s], Decompressed: 4745
Downloaded: 6538 file(s) [attempted 6538/8232 = 79%, 76 KB/s], Decompressed: 4745
Downloaded: 6576 file(s) [attempted 6576/8232 = 79%, 1001 KB/s], Decompressed: 4745
Downloaded: 6617 file(s) [attempted 6617/8232 = 80%, 238 KB/s], Decompressed: 4745
Downloaded: 6655 file(s) [attempted 6655/8232 = 80%, 126 KB/s], Decompressed: 4745
Downloaded: 6699 file(s) [attempted 6699/8232 = 81%, 97 KB/s], Decompressed: 4745
Downloaded: 6747 file(s) [attempted 6747/8232 = 81%, 113 KB/s], Decompressed: 4745
Downloaded: 6795 file(s) [attempted 6795/8232 = 82%, 177 KB/s], Decompressed: 4745
Downloaded: 6840 file(s) [attempted 6840/8232 = 83%, 372 KB/s], Decompressed: 4745
Downloaded: 6874 file(s) [attempted 6874/8232 = 83%, 228 KB/s], Decompressed: 4745
Downloaded: 6911 file(s) [attempted 6911/8232 = 83%, 697 KB/s], Decompressed: 4745
Downloaded: 6956 file(s) [attempted 6956/8232 = 84%, 99 KB/s], Decompressed: 4745
Downloaded: 7000 file(s) [attempted 7000/8232 = 85%, 1170 KB/s], Decompressed: 4745
Downloaded: 7048 file(s) [attempted 7048/8232 = 85%, 1049 KB/s], Decompressed: 5792
Downloaded: 7096 file(s) [attempted 7096/8232 = 86%, 360 KB/s], Decompressed: 5792
Downloaded: 7134 file(s) [attempted 7134/8232 = 86%, 72 KB/s], Decompressed: 5792
Downloaded: 7172 file(s) [attempted 7172/8232 = 87%, 53 KB/s], Decompressed: 5792
Downloaded: 7213 file(s) [attempted 7213/8232 = 87%, 83 KB/s], Decompressed: 5792
Downloaded: 7257 file(s) [attempted 7257/8232 = 88%, 422 KB/s], Decompressed: 5792
Downloaded: 7295 file(s) [attempted 7295/8232 = 88%, 1164 KB/s], Decompressed: 5792
Downloaded: 7336 file(s) [attempted 7336/8232 = 89%, 212 KB/s], Decompressed: 5792
Downloaded: 7373 file(s) [attempted 7373/8232 = 89%, 470 KB/s], Decompressed: 5792
Downloaded: 7421 file(s) [attempted 7421/8232 = 90%, 106 KB/s], Decompressed: 5792
Downloaded: 7466 file(s) [attempted 7466/8232 = 90%, 395 KB/s], Decompressed: 5792
Downloaded: 7507 file(s) [attempted 7507/8232 = 91%, 251 KB/s], Decompressed: 5792
Downloaded: 7548 file(s) [attempted 7548/8232 = 91%, 724 KB/s], Decompressed: 5792
Downloaded: 7582 file(s) [attempted 7582/8232 = 92%, 22 KB/s], Decompressed: 5792
Downloaded: 7623 file(s) [attempted 7623/8232 = 92%, 286 KB/s], Decompressed: 5792
Downloaded: 7671 file(s) [attempted 7671/8232 = 93%, 948 KB/s], Decompressed: 5792
Downloaded: 7719 file(s) [attempted 7719/8232 = 93%, 131 KB/s], Decompressed: 5792
Downloaded: 7764 file(s) [attempted 7764/8232 = 94%, 1903 KB/s], Decompressed: 5792
Downloaded: 7805 file(s) [attempted 7805/8232 = 94%, 170 KB/s], Decompressed: 5792
Downloaded: 7846 file(s) [attempted 7846/8232 = 95%, 237 KB/s], Decompressed: 5792
Downloaded: 7880 file(s) [attempted 7880/8232 = 95%, 133 KB/s], Decompressed: 5792
Downloaded: 7924 file(s) [attempted 7924/8232 = 96%, 163 KB/s], Decompressed: 5792
Downloaded: 7965 file(s) [attempted 7965/8232 = 96%, 89 KB/s], Decompressed: 5792
Downloaded: 8007 file(s) [attempted 8007/8232 = 97%, 514 KB/s], Decompressed: 5792
Downloaded: 8044 file(s) [attempted 8044/8232 = 97%, 43 KB/s], Decompressed: 5792
Downloaded: 8085 file(s) [attempted 8085/8232 = 98%, 60 KB/s], Decompressed: 5792
Downloaded: 8126 file(s) [attempted 8126/8232 = 98%, 261 KB/s], Decompressed: 5792
Downloaded: 8167 file(s) [attempted 8167/8232 = 99%, 881 KB/s], Decompressed: 5792
Downloaded: 8212 file(s) [attempted 8212/8232 = 99%, 111 KB/s], Decompressed: 5792
Downloaded: 8232 file(s) [attempted 8232/8232 = 100%, 111 KB/s], Decompressed: 5792

lean_checker exit 0 duration 15m 26s · created 6/4/2026, 10:15:45 AM

lake build

✔ [2765/2805] Built Architect.Command (4.4s)
✔ [2810/2835] Built Architect.Basic (4.9s)
✔ [2813/2835] Built Architect.Tactic (1.6s)
✔ [2814/2835] Built Architect.CollectUsed (1.6s)
✔ [2817/2838] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic (3.7s)
✔ [2821/2858] Built PrimeNumberTheoremAnd.Auxiliary (8.8s)
✔ [3028/3057] Built Architect.Content (1.6s)
✔ [3043/3063] Built PrimeNumberTheoremAnd.Tactic.AdditiveCombination (3.3s)
✔ [3293/3387] Built Architect.Attribute (2.9s)
✔ [3423/3460] Built Architect.Output (3.1s)
✔ [3440/3468] Built PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support (1.6s)
✔ [3444/3468] Built Architect.Load (1.6s)
✔ [3448/3478] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics (2.5s)
✔ [3518/3554] Built Architect (1.2s)
✔ [3535/3555] Built PrimeNumberTheoremAnd.Sobolev (15s)
✔ [3536/3555] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults (6.5s)
✔ [3537/3557] Built PrimeNumberTheoremAnd.SmoothExistence (5.9s)
✔ [3539/3564] Built PrimeNumberTheoremAnd.ZetaConj (6.3s)
✔ [3541/3570] Built PrimeNumberTheoremAnd.Rectangle (6.5s)
✔ [3544/3570] Built PrimeNumberTheoremAnd.Fourier (5.3s)
✔ [3547/3572] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic (7.1s)
✔ [3549/3586] Built PrimeNumberTheoremAnd.Defs (11s)
✔ [3583/3605] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (16s)
✔ [3586/3611] Built PrimeNumberTheoremAnd.HadamardFactorization (1.8s)
✔ [3587/3611] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg (13s)
✔ [3589/3611] Built PrimeNumberTheoremAnd.HoffsteinLockhart (3.2s)
✔ [3591/3612] Built PrimeNumberTheoremAnd.MellinCalculus (21s)
✔ [3594/3612] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.9s)
✔ [3597/3615] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds (6.5s)
✔ [3600/3616] Built PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions (7.7s)
⚠ [3603/3616] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta (9.3s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3604/3618] Built PrimeNumberTheoremAnd.BrunTitchmarsh (14s)
✔ [3608/3631] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (22s)
✔ [3656/3674] Built PrimeNumberTheoremAnd.IEANTN.KLN (6.8s)
✔ [3665/3685] Built LeanCert.Core.Interval (5.2s)
✔ [3666/3686] Built LeanCert.Core.Expr (9.0s)
✔ [3667/3686] Built LeanCert.Core.Support (8.1s)
✔ [3668/3686] Built LeanCert.Core.IntervalRat.Basic (20s)
✔ [3669/3687] Built LeanCert.Meta.Numeral (8.4s)
✔ [3670/3687] Built LeanCert.Tactic.IntervalAuto.Types (8.3s)
✔ [3671/3687] Built LeanCert.Core.IntervalRat.Transcendental (11s)
✔ [3672/3687] Built LeanCert.Tactic.IntervalAuto.Extract (6.3s)
✔ [3673/3687] Built LeanCert.Meta.ToExpr (7.2s)
✔ [3674/3688] Built PrimeNumberTheoremAnd.ZetaBounds (69s)
✔ [3675/3692] Built LeanCert.Core.IntervalRat.LogReduction (9.7s)
✔ [3676/3692] Built LeanCert.Tactic.IntervalAuto.Norm (7.9s)
✔ [3677/3693] Built LeanCert.Tactic.IntervalAuto.Parse (10s)
✔ [3679/3695] Built LeanCert.Core.DerivativeIntervals (8.2s)
✔ [3680/3696] Built LeanCert.Tactic.IntervalAuto.Diagnostic (9.4s)
✔ [3681/3698] Built LeanCert.Core.Taylor (17s)
⚠ [3682/3699] Built PrimeNumberTheoremAnd.Wiener (94s)
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
✔ [3683/3701] Built LeanCert.Core.IntervalRat.Taylor (41s)
✔ [3684/3701] Built LeanCert.Core.IntervalRat.TrigReduced (11s)
✔ [3685/3702] Built LeanCert.Core.IntervalReal (7.8s)
✔ [3686/3702] Built LeanCert.Core.IntervalRealEndpoints (10s)
✔ [3687/3704] Built LeanCert.Engine.Eval.Core (19s)
✔ [3688/3709] Built LeanCert.Engine.Eval.Extended (11s)
ℹ [3689/3709] Built PrimeNumberTheoremAnd.MediumPNT (141s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3690/3709] Built LeanCert.Tactic.Bound.Lemmas (6.8s)
✔ [3691/3709] Built LeanCert.Contrib.Sinc (8.5s)
✔ [3692/3713] Built PrimeNumberTheoremAnd.Consequences (112s)
✔ [3703/3731] Built LeanCert.Engine.IntervalEval (3.5s)
✔ [3704/3731] Built LeanCert.Core.Dyadic (4.8s)
⚠ [3705/3735] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (161s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
✔ [3706/3735] Built LeanCert.Engine.AD.Basic (5.6s)
✔ [3707/3736] Built LeanCert.Engine.TaylorModel.Core (13s)
⚠ [3708/3736] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (8.9s)
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`
✔ [3709/3736] Built LeanCert.Core.IntervalDyadic (15s)
✔ [3710/3736] Built LeanCert.Engine.Affine.Basic (12s)
✔ [3711/3736] Built LeanCert.Engine.AD.Transcendental (8.5s)
✔ [3712/3736] Built LeanCert.Engine.TaylorModel.Special (4.5s)
⚠ [3713/3736] Built PrimeNumberTheoremAnd.StrongPNT (38s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1477:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1526:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1643:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2183:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2273:6: declaration uses `sorry`
✔ [3714/3736] Built LeanCert.Engine.TaylorModel.ExpLog (12s)
✔ [3715/3739] Built LeanCert.Engine.Optimization.Box (5.3s)
✔ [3716/3739] Built LeanCert.Engine.TaylorModel.Hyperbolic (15s)
✔ [3717/3739] Built LeanCert.Engine.TaylorModel.Trig (14s)
✔ [3718/3739] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (3.2s)
✔ [3719/3739] Built LeanCert.Engine.IntervalEvalDyadic (4.7s)
✔ [3720/3739] Built LeanCert.Engine.AD.Eval (3.5s)
✔ [3721/3741] Built LeanCert.Engine.TaylorModel.Functions (3.0s)
✔ [3722/3742] Built LeanCert.Engine.Affine.Nonlinear (6.3s)
✔ [3723/3743] Built PrimeNumberTheoremAnd.BorelCaratheodory (6.0s)
✔ [3724/3746] Built LeanCert.Engine.AD.Correctness (4.1s)
✔ [3725/3746] Built LeanCert.Engine.RootFinding.Basic (5.7s)
✔ [3726/3748] Built LeanCert.Engine.TaylorModel.Expr (6.2s)
✔ [3727/3749] Built LeanCert.Engine.Affine.Transcendental (5.2s)
✔ [3728/3749] Built LeanCert.Engine.AD.Computable (5.2s)
✔ [3729/3751] Built LeanCert.Engine.TaylorModel (3.0s)
✔ [3730/3751] Built LeanCert.Engine.RootFinding.Bisection (5.2s)
✔ [3731/3764] Built LeanCert.Engine.Integrate (6.9s)
✔ [3732/3770] Built LeanCert.Engine.AD.PartialCorrectness (7.9s)
✔ [3734/3770] Built LeanCert.Validity.DyadicBounds (3.1s)
✔ [3735/3771] Built LeanCert.Engine.IntervalEvalAffine (4.2s)
✔ [3736/3773] Built LeanCert.Engine.AD (5.3s)
✔ [3738/3773] Built LeanCert.Engine.TaylorModel.Log1p (9.4s)
✔ [3739/3773] Built LeanCert.Engine.IntervalEvalRefined (5.6s)
✔ [3740/3773] Built PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries (13s)
✔ [3743/3773] Built LeanCert.Engine.Optimize (7.5s)
✔ [3744/3773] Built LeanCert.Meta.ProveSupported (4.4s)
⚠ [3745/3777] Built LeanCert.Examples.Li2Bounds (5.2s)
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
✔ [3746/3777] Built LeanCert.Engine.Optimization.Gradient (6.2s)
✔ [3747/3777] Built LeanCert.Engine.RootFinding.Newton (6.1s)
✔ [3748/3779] Built LeanCert.Meta.ProveContinuous (4.9s)
✔ [3750/3779] Built PrimeNumberTheoremAnd.IEANTN.Li2Bounds (5.9s)
✔ [3751/3781] Built LeanCert.Tactic.IntervalAuto.ProveCommon (7.4s)
✔ [3755/3783] Built LeanCert.Engine.RootFinding.MVTBounds (9.6s)
✔ [3759/3796] Built LeanCert.Tactic.IntervalAuto.Basic (3.4s)
✔ [3867/3897] Built PrimeNumberTheoremAnd.IEANTN.PVIdentity (39s)
✔ [3868/3899] Built LeanCert.Engine.RootFinding.Contraction (8.9s)
✔ [3869/3899] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables (7.1s)
✔ [3870/3899] Built LeanCert.Tactic.VecUtil (6.8s)
✔ [3871/3900] Built LeanCert.Engine.RootFinding.Main (5.3s)
✔ [3872/3903] Built LeanCert.Engine.Optimization.Global (28s)
✔ [3874/3903] Built LeanCert.Tactic.FinSumExpand (3.9s)
✔ [3875/3913] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables (26s)
✔ [3880/3913] Built LeanCert.Engine.Optimization.BoundVerify (5.0s)
✔ [3881/3913] Built PrimeNumberTheoremAnd.IEANTN.LiSeries (16s)
✔ [3882/3920] Built LeanCert.Engine.Chebyshev.Psi (4.8s)
✔ [3883/3920] Built LeanCert.Validity.Bounds (11s)
✔ [3886/3921] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables (4.5s)
✔ [3888/3921] Built LeanCert.Engine.ChebyshevPsi (4.2s)
✔ [3889/3921] Built PrimeNumberTheoremAnd.Tactic.Simprocs (3.6s)
✔ [3890/3921] Built LeanCert.Tactic.IntervalAuto.OptBound (5.2s)
✔ [3891/3922] Built LeanCert.Tactic.IntervalAuto.Multivariate (8.5s)
✔ [3893/3922] Built LeanCert.Tactic.IntervalAuto.RootBound (3.8s)
✔ [3894/3923] Built PrimeCert.Interval (4.8s)
✔ [3895/3923] Built PrimeCert.Meta.PrimeCert (5.0s)
✔ [3896/3925] Built PrimeCert.Meta.SmallPrime (4.3s)
✔ [3897/3926] Built PrimeCert.PredMod (843ms)
✔ [3898/3937] Built PrimeCert.PowMod (3.5s)
⚠ [3901/3937] Built PrimeCert.Pocklington (7.8s)
warning: PrimeCert/Pocklington.lean:60:22: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3902/3937] Built PrimeCert.Wieferich (6.5s)
✔ [3903/3937] Built PrimeCert.SmallPrimes (5.8s)
✔ [3904/3937] Built LeanCert.Tactic.IntervalAuto.Bound (51s)
⚠ [3905/3937] Built PrimeCert.Pocklington3 (11s)
warning: PrimeCert/Pocklington3.lean:39:8: `Nat.factorization_prod_pow_eq_self` has been deprecated: Use `Nat.prod_factorization_pow_eq_self` instead
✔ [3906/3937] Built LeanCert.Tactic.IntervalAuto.Subdiv (15s)
⚠ [3907/3945] Built PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP (66s)
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`
✔ [3908/3947] Built LeanCert.Tactic.IntervalAuto.PointIneq (29s)
✔ [3910/3950] Built PrimeCert (5.2s)
✔ [3914/3959] Built PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev (10s)
✔ [3916/3959] Built LeanCert.Tactic.IntervalAuto.Adaptive (15s)
✔ [3918/3959] Built PrimeNumberTheoremAnd.IEANTN.PrimeTables (14s)
✔ [3919/3959] Built LeanCert.Engine.Chebyshev.Theta (19s)
⚠ [3920/3959] Built PrimeNumberTheoremAnd.IEANTN.Mertens (31s)
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`
⚠ [3921/3959] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (130s)
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`
✔ [3923/3959] Built PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly (3.6s)
✔ [3924/3959] Built LeanCert.Tactic.IntervalAuto (4.7s)
✔ [3925/3959] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (35s)
✔ [3927/3959] Built LeanCert.Engine.ChebyshevTheta (3.1s)
⚠ [3928/3959] Built PrimeNumberTheoremAnd.IwaniecKowalskiCh1 (11s)
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`
⚠ [3929/3959] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (9.6s)
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`
✔ [3930/3959] Built PrimeNumberTheoremAnd.PerronFormula (14s)
✔ [3931/3959] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (14s)
✔ [3932/3959] Built PrimeNumberTheoremAnd.IEANTN.LogTables (12s)
✔ [3933/3959] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (8.3s)
⚠ [3934/3959] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (13s)
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`
⚠ [3935/3959] Built LeanCert.Examples.BKLNW_a2_pow2 (48s)
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/3959] Built PrimeNumberTheoremAnd.IEANTN.Buthe (27s)
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/3959] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations (45s)
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.
⚠ [3938/3959] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (33s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [3939/3959] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (28s)
✔ [3940/3959] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (7.2s)
⚠ [3941/3959] Built LeanCert.Examples.BKLNW_a2_bounds (6.3s)
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`
✔ [3942/3959] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (43s)
⚠ [3943/3959] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (15s)
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`
✔ [3944/3959] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (6.8s)
⚠ [3945/3959] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (10s)
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`
✔ [3946/3959] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (97s)
✔ [3947/3959] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (135s)
⚠ [3948/3959] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (31s)
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`
✔ [3949/3959] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (10s)
⚠ [3950/3959] Built PrimeNumberTheoremAnd.IEANTN.Dusart (30s)
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`
✔ [3951/3959] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (15s)
⚠ [3952/3959] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (23s)
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`
⚠ [3953/3959] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (72s)
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/3959] 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`
⚠ [3955/3959] 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`
✔ [3956/3959] Built PrimeNumberTheoremAnd.IEANTN.Lcm (44s)
✔ [3957/3959] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (75s)
✔ [3958/3959] Built PrimeNumberTheoremAnd (2.7s)
Build completed successfully (3959 jobs).

blueprint_build exit 0 duration 4m 55s · created 6/4/2026, 10:15:45 AM

lake build :blueprint

✔ [9/35] Built Architect.Command:c.o (490ms)
✔ [11/35] Built Batteries.Lean.NameMapAttribute:c.o (734ms)
✔ [14/35] Built Architect.CollectUsed:c.o (138ms)
✔ [15/35] Built Architect.Tactic:c.o (366ms)
✔ [16/35] Built Architect.Basic:c.o (887ms)
✔ [18/35] Built Architect.Content:c.o (183ms)
✔ [20/43] Built Architect.Load:c.o (160ms)
✔ [21/43] Built Architect:c.o (54ms)
✔ [121/132] Built Architect.Attribute:c.o (1.0s)
✔ [122/132] Built Cli:c.o (53ms)
✔ [124/143] Built Cli.Extensions:c.o (784ms)
✔ [168/214] Built Architect.Output:c.o (1.6s)
✔ [861/977] Built Main (1.2s)
✔ [1188/1357] Built Main:c.o (233ms)
ℹ [3456/3667] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4286:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3474/3667] 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`
⚠ [3628/3849] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:322:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:341:8: declaration uses `sorry`
⚠ [3631/3849] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3685/3849] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2024:8: declaration uses `sorry`
⚠ [3686/3849] 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`
⚠ [3779/3849] 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`
⚠ [3781/3849] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:250:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:255:8: declaration uses `sorry`
⚠ [3907/4058] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [3909/4058] 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`
⚠ [3910/4058] 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`
⚠ [3912/4058] 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`
⚠ [3915/4058] 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`
⚠ [3916/4058] 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`
⚠ [3923/4058] 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`
⚠ [3924/4058] 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`
⚠ [3930/4058] 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`
⚠ [3931/4058] 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`
⚠ [3936/4058] 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`
⚠ [3946/4058] 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
⚠ [3947/4058] 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
⚠ [3953/4058] 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`
⚠ [3954/4058] 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`
⚠ [3955/4058] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [3961/4058] 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`
⚠ [3965/4058] 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`
ℹ [3971/4058] 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.
⚠ [3973/4058] 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`
✔ [3977/4058] Built Cli.Basic:c.o (4.2s)
✔ [3978/4058] Built extract_blueprint:exe (2.7s)
✔ [3979/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Auxiliary:blueprint (2.1s)
✔ [3980/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Sobolev:blueprint (2.1s)
✔ [3981/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Fourier:blueprint (2.2s)
✔ [3982/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic:blueprint (1.8s)
✔ [3983/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Rectangle:blueprint (1.9s)
✔ [3984/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.AdditiveCombination:blueprint (1.3s)
✔ [3985/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (12s)
✔ [3986/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaConj:blueprint (11s)
✔ [3987/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support:blueprint (1.2s)
✔ [3988/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SmoothExistence:blueprint (3.8s)
✔ [3989/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (47s)
✔ [3990/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.3s)
✔ [3991/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics:blueprint (1.8s)
✔ [3992/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults:blueprint (2.2s)
✔ [3993/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic:blueprint (2.2s)
✔ [3994/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg:blueprint (2.4s)
✔ [3995/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds:blueprint (2.3s)
✔ [3996/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BrunTitchmarsh:blueprint (2.2s)
✔ [3997/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Defs:blueprint (8.7s)
✔ [3998/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Wiener:blueprint (34s)
✔ [3999/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Consequences:blueprint (14s)
✔ [4000/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.2s)
✔ [4001/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (2.8s)
✔ [4002/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HadamardFactorization:blueprint (1.2s)
✔ [4003/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.HoffsteinLockhart:blueprint (2.4s)
✔ [4004/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions:blueprint (10s)
✔ [4005/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KLN:blueprint (2.8s)
✔ [4006/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta:blueprint (2.9s)
✔ [4007/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (25s)
✔ [4008/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.0s)
✔ [4009/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.7s)
✔ [4010/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (2.7s)
✔ [4011/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.4s)
✔ [4012/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (17s)
✔ [4013/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Li2Bounds:blueprint (6.2s)
✔ [4014/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PVIdentity:blueprint (3.4s)
✔ [4015/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LiSeries:blueprint (2.5s)
✔ [4016/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries:blueprint (3.2s)
✔ [4017/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (13s)
✔ [4018/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (8.5s)
✔ [4019/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables:blueprint (4.8s)
✔ [4020/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (25s)
✔ [4021/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables:blueprint (5.8s)
✔ [4022/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (8.3s)
✔ [4023/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (24s)
✔ [4024/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (7.0s)
✔ [4025/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (33s)
✔ [4026/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.0s)
✔ [4027/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (66s)
✔ [4028/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
✔ [4029/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (23s)
✔ [4030/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (5.6s)
✔ [4031/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables:blueprint (3.1s)
✔ [4032/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP:blueprint (4.7s)
✔ [4033/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (24s)
✔ [4034/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (21s)
✔ [4035/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (43s)
✔ [4036/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Tactic.Simprocs:blueprint (2.0s)
✔ [4037/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeTables:blueprint (2.6s)
✔ [4038/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.7s)
✔ [4039/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (56s)
✔ [4040/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (8.4s)
✔ [4041/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (7.9s)
✔ [4042/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (12s)
✔ [4043/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev:blueprint (2.8s)
✔ [4044/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (14s)
✔ [4045/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (43s)
✔ [4046/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (14s)
✔ [4047/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.7s)
✔ [4048/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations:blueprint (9.1s)
✔ [4049/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (22s)
✔ [4050/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IwaniecKowalskiCh1:blueprint (52s)
✔ [4051/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly:blueprint (4.2s)
✔ [4052/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (29s)
✔ [4053/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (5.3s)
✔ [4054/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (57s)
✔ [4055/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MellinCalculus:blueprint (23s)
✔ [4056/4058] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (61s)
ℹ [4057/4059] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (101ms)
info: Blueprint indexing
Build completed successfully (4059 jobs).

semantic_extract exit - duration 4h 0m · created 6/4/2026, 10:15:45 AM

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

lean semantic helper: stored compiled static runner cache 65f3b0b99855f93a49cf88bf2915f1de2063f50d1dc9b94aabcb09ce23a0de78
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-62-runtime-semantic_extract-35666-1780553664546287977-7