Verification run

Run 61

AlexKontorovich/PrimeNumberTheoremAnd branch main triggered via poller

failed commit 163b038df52a toolchain lean-v4-30-0 prover lean took 19m · finished 4w ago

lake build failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase lake build)

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

$ git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-501-source
exit_code=Some(0) duration_ms=788
stderr:
Cloning into '/var/lib/apodeixis/repos/job-501-source'...


$ git checkout 163b038df52ab9bca713fcab4638ace08bc5813e
exit_code=Some(0) duration_ms=24
stderr:
Note: switching to '163b038df52ab9bca713fcab4638ace08bc5813e'.

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 163b038 chore: remove some linarith calls whose replacement is trivial (#1406)

Resolved source revision: 163b038df52ab9bca713fcab4638ace08bc5813e

Detected prover: lean
Detected requested toolchain: lean-v4-30-0
Materialized Lean semantic helper assets
Prepared source: revision=163b038df52ab9bca713fcab4638ace08bc5813e provenance={"branch":"main","checked_out_revision":"163b038df52ab9bca713fcab4638ace08bc5813e","clone_url_hash":"a03bacf7666a5db5fc46a6063d1ab504468fa73929987cbd844a193cbaeaf0a3","credential_mode":"none","local_clone":false,"requested_commit_sha":"163b038df52ab9bca713fcab4638ace08bc5813e","used_missing_commit_fetch":false}
Resolved toolchain: lean-v4-30-0 (image: ghcr.io/gogopex/apodeixis/verifier-lean-base:elan)
Restored Lean workspace build cache
Restored 13 Lean dependency package snapshot(s)
Prepared 13 shared Lean git mirror alias(es)
Lean semantic module cache: pre-semantic phase failed; not running semantic extraction

$ lake exe cache get
exit_code=Some(137) duration_ms=43525
stdout:
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 4 KB/s], Decompressed: 11
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 16 KB/s], Decompressed: 34
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 44 KB/s], Decompressed: 64
Downloaded: 96 file(s) [attempted 96/8459 = 1%, 51 KB/s], Decompressed: 89
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 370 KB/s], Decompressed: 121
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 59 KB/s], Decompressed: 131
Downloaded: 206 file(s) [attempted 206/8459 = 2%, 445 KB/s], Decompressed: 131
Downloaded: 248 file(s) [attempted 248/8459 = 2%, 696 KB/s], Decompressed: 240
Downloaded: 285 file(s) [attempted 285/8459 = 3%, 1004 KB/s], Decompressed: 278
Downloaded: 329 file(s) [attempted 329/8459 = 3%, 147 KB/s], Decompressed: 323
Downloaded: 364 file(s) [attempted 364/8459 = 4%, 89 KB/s], Decompressed: 357
Downloaded: 401 file(s) [attempted 401/8459 = 4%, 1150 KB/s], Decompressed: 398
Downloaded: 446 file(s) [attempted 446/8459 = 5%, 317 KB/s], Decompressed: 432
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 27 KB/s], Decompressed: 477
Downloaded: 518 file(s) [attempted 518/8459 = 6%, 731 KB/s], Decompressed: 514
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 57 KB/s], Decompressed: 556
Downloaded: 597 file(s) [attempted 597/8459 = 7%, 308 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 244 KB/s], Decompressed: 627
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 254 KB/s], Decompressed: 675
Downloaded: 713 file(s) [attempted 713/8459 = 8%, 289 KB/s], Decompressed: 710
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 226 KB/s], Decompressed: 751
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 146 KB/s], Decompressed: 792
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 71 KB/s], Decompressed: 833
Downloaded: 874 file(s) [attempted 874/8459 = 10%, 155 KB/s], Decompressed: 864
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 295 KB/s], Decompressed: 908
Downloaded: 953 file(s) [attempted 953/8459 = 11%, 847 KB/s], Decompressed: 946
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 154 KB/s], Decompressed: 991
Downloaded: 1037 file(s) [attempted 1037/8459 = 12%, 736 KB/s], Decompressed: 1032
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 257 KB/s], Decompressed: 1073
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 509 KB/s], Decompressed: 1100
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 365 KB/s], Decompressed: 1141
Downloaded: 1187 file(s) [attempted 1187/8459 = 14%, 186 KB/s], Decompressed: 1182
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 270 KB/s], Decompressed: 1223
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 632 KB/s], Decompressed: 1254
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 264 KB/s], Decompressed: 1295
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 161 KB/s], Decompressed: 1345
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 463 KB/s], Decompressed: 1384
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 61 KB/s], Decompressed: 1425
Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 25 KB/s], Decompressed: 1466
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 53 KB/s], Decompressed: 1507
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 118 KB/s], Decompressed: 1550
Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 136 KB/s], Decompressed: 1589
Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 1056 KB/s], Decompressed: 1627
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 76 KB/s], Decompressed: 1665
Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 922 KB/s], Decompressed: 1706
Downloaded: 1752 file(s) [attempted 1752/8459 = 20%, 686 KB/s], Decompressed: 1747
Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 53 KB/s], Decompressed: 1785
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 554 KB/s], Decompressed: 1822
Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1760 KB/s], Decompressed: 1860
Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 227 KB/s], Decompressed: 1901
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 654 KB/s], Decompressed: 1942
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 75 KB/s], Decompressed: 1976
Downloaded: 2017 file(s) [attempted 2017/8459 = 23%, 58 KB/s], Decompressed: 2014
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 143 KB/s], Decompressed: 2052
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1094 KB/s], Decompressed: 2096
Downloaded: 2134 file(s) [attempted 2134/8459 = 25%, 260 KB/s], Decompressed: 2130
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 83 KB/s], Decompressed: 2168
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 111 KB/s], Decompressed: 2209
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 157 KB/s], Decompressed: 2253
Downloaded: 2303 file(s) [attempted 2303/8459 = 27%, 2016 KB/s], Decompressed: 2298
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 85 KB/s], Decompressed: 2332
Downloaded: 2374 file(s) [attempted 2374/8459 = 28%, 231 KB/s], Decompressed: 2360
Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 44 KB/s], Decompressed: 2407
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 655 KB/s], Decompressed: 2445
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 119 KB/s], Decompressed: 2483
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 585 KB/s], Decompressed: 2527
Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 159 KB/s], Decompressed: 2568
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 395 KB/s], Decompressed: 2613
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 59 KB/s], Decompressed: 2654
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 803 KB/s], Decompressed: 2688
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 584 KB/s], Decompressed: 2729
Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 1200 KB/s], Decompressed: 2729
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 730 KB/s], Decompressed: 2733
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 305 KB/s], Decompressed: 2856
Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 686 KB/s], Decompressed: 2897
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 990 KB/s], Decompressed: 2931
Downloaded: 2974 file(s) [attempted 2974/8459 = 35%, 284 KB/s], Decompressed: 2969
Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 616 KB/s], Decompressed: 3010
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 309 KB/s], Decompressed: 3051
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 296 KB/s], Decompressed: 3082
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 331 KB/s], Decompressed: 3123
Downloaded: 3168 file(s) [attempted 3168/8459 = 37%, 66 KB/s], Decompressed: 3164
Downloaded: 3212 file(s) [attempted 3212/8459 = 37%, 79 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 352 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 131 KB/s], Decompressed: 3284
Downloaded: 3322 file(s) [attempted 3322/8459 = 39%, 83 KB/s], Decompressed: 3314
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 896 KB/s], Decompressed: 3362
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 206 KB/s], Decompressed: 3403
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 584 KB/s], Decompressed: 3444
Downloaded: 3487 file(s) [attempted 3487/8459 = 41%, 480 KB/s], Decompressed: 3475
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 372 KB/s], Decompressed: 3520
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 449 KB/s], Decompressed: 3564
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 170 KB/s], Decompressed: 3605
Downloaded: 3659 file(s) [attempted 3659/8459 = 43%, 593 KB/s], Decompressed: 3653
Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 189 KB/s], Decompressed: 3677
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 234 KB/s], Decompressed: 3722
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 1042 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 218 KB/s], Decompressed: 3811
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 85 KB/s], Decompressed: 3852
Downloaded: 3902 file(s) [attempted 3902/8459 = 46%, 397 KB/s], Decompressed: 3889
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 73 KB/s], Decompressed: 3920
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 105 KB/s], Decompressed: 3958
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 269 KB/s], Decompressed: 4002
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 253 KB/s], Decompressed: 4054
Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 3591 KB/s], Decompressed: 4088
Downloaded: 4142 file(s) [attempted 4142/8459 = 48%, 67 KB/s], Decompressed: 4129
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 308 KB/s], Decompressed: 4160
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 201 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 32 KB/s], Decompressed: 4249
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 1197 KB/s], Decompressed: 4293
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 223 KB/s], Decompressed: 4331
Downloaded: 4366 file(s) [attempted 4366/8459 = 51%, 24 KB/s], Decompressed: 4358
Downloaded: 4400 file(s) [attempted 4400/8459 = 52%, 163 KB/s], Decompressed: 4396
Downloaded: 4447 file(s) [attempted 4447/8459 = 52%, 94 KB/s], Decompressed: 4444
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 241 KB/s], Decompressed: 4488
Downloaded: 4531 file(s) [attempted 4531/8459 = 53%, 449 KB/s], Decompressed: 4526
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 914 KB/s], Decompressed: 4553
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 404 KB/s], Decompressed: 4591
Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 147 KB/s], Decompressed: 4632
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 95 KB/s], Decompressed: 4680
Downloaded: 4728 file(s) [attempted 4728/8459 = 55%, 37 KB/s], Decompressed: 4721
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 22 KB/s], Decompressed: 4755
Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 392 KB/s], Decompressed: 4793
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 601 KB/s], Decompressed: 4834
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 34 KB/s], Decompressed: 4868
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 380 KB/s], Decompressed: 4919
Downloaded: 4962 file(s) [attempted 4962/8459 = 58%, 538 KB/s], Decompressed: 4957
Downloaded: 4992 file(s) [attempted 4992/8459 = 59%, 1037 KB/s], Decompressed: 4988
Downloaded: 5034 file(s) [attempted 5034/8459 = 59%, 154 KB/s], Decompressed: 5029
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 512 KB/s], Decompressed: 5073
Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 50 KB/s], Decompressed: 5111
Downloaded: 5149 file(s) [attempted 5149/8459 = 60%, 114 KB/s], Decompressed: 5142
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 153 KB/s], Decompressed: 5186
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 244 KB/s], Decompressed: 5231
Downloaded: 5281 file(s) [attempted 5281/8459 = 62%, 1168 KB/s], Decompressed: 5275
Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 222 KB/s], Decompressed: 5313
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 653 KB/s], Decompressed: 5347
Downloaded: 5393 file(s) [attempted 5393/8459 = 63%, 121 KB/s], Decompressed: 5388
Downloaded: 5433 file(s) [attempted 5433/8459 = 64%, 74 KB/s], Decompressed: 5423
Downloaded: 5476 file(s) [attempted 5476/8459 = 64%, 149 KB/s], Decompressed: 5467
Downloaded: 5512 file(s) [attempted 5512/8459 = 65%, 114 KB/s], Decompressed: 5505
Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 1057 KB/s], Decompressed: 5546
Downloaded: 5589 file(s) [attempted 5589/8459 = 66%, 54 KB/s], Decompressed: 5583
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 1278 KB/s], Decompressed: 5628
Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 570 KB/s], Decompressed: 5659
Downloaded: 5710 file(s) [attempted 5710/8459 = 67%, 202 KB/s], Decompressed: 5700
Downloaded: 5748 file(s) [attempted 5748/8459 = 67%, 357 KB/s], Decompressed: 5744

lake_cache failed; continuing (non-fatal phase).

$ lake build
exit_code=None duration_ms=30156
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
podman cleanup removed verifier container apx-verifier-job-501-runtime-lean_checker-282038-1781635753364854016-1

$ lake build :blueprint
exit_code=Some(0) duration_ms=823239
stdout:
✔ [16/35] Built Batteries.Lean.NameMapAttribute:c.o (760ms)
✔ [28/35] Built Cli.Basic:c.o (3.3s)
✔ [30/35] Built Cli.Extensions:c.o (588ms)
✔ [33/41] Built Cli:c.o (68ms)
ℹ [3595/3612] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3629/3642] Built PrimeNumberTheoremAnd.StrongPNT (182s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3630/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (67s)
✔ [3634/3643] Built PrimeNumberTheoremAnd.BorelCaratheodory (10s)
✔ [3636/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (10s)
⚠ [3768/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3896/3909] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
⚠ [3960/3988] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3962/3988] 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`
⚠ [3964/3988] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3977/3996] 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:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [4109/4125] 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`
⚠ [4113/4181] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4116/4181] 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:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4120/4181] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
ℹ [4139/4200] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359: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.
⚠ [4158/4206] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4162/4206] 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`
⚠ [4189/4206] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
⚠ [4204/4251] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: 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/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  ring
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
  theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    x hx₁
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    (by
      cases x₂ <;> norm_num at *; · exact_mod_cast hc;
      · exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
  [apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
    Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4674:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4701:8: declaration uses `sorry`
⚠ [4256/4267] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4258/4267] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:203:39: missing space in the source

This part of the code
  '(3/2) 0.8476'
should be written as
  '(3 / 2)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
⚠ [4273/4325] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
⚠ [4280/4356] 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`
⚠ [4300/4395] 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`
ℹ [4326/4395] 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.
⚠ [4327/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
⚠ [4334/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4346/4395] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries (28s)
✔ [4372/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (41s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4392/4395] Built PrimeNumberTheoremAnd (156s)
✔ [4393/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (275s)
ℹ [4394/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (314ms)
info: Blueprint indexing
Build completed successfully (4396 jobs).

stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Command runs

git_clone exit 0 duration 788 ms · created 6/16/2026, 7:03:37 PM

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

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

git_checkout exit 0 duration 24 ms · created 6/16/2026, 7:03:37 PM

git checkout 163b038df52ab9bca713fcab4638ace08bc5813e

Note: switching to '163b038df52ab9bca713fcab4638ace08bc5813e'.

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 163b038 chore: remove some linarith calls whose replacement is trivial (#1406)

lake_cache exit 137 duration 44s · created 6/16/2026, 7:03:37 PM

lake exe cache get

Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 13 file(s) [attempted 13/8459 = 0%, 4 KB/s], Decompressed: 11
Downloaded: 37 file(s) [attempted 37/8459 = 0%, 16 KB/s], Decompressed: 34
Downloaded: 66 file(s) [attempted 66/8459 = 0%, 44 KB/s], Decompressed: 64
Downloaded: 96 file(s) [attempted 96/8459 = 1%, 51 KB/s], Decompressed: 89
Downloaded: 131 file(s) [attempted 131/8459 = 1%, 370 KB/s], Decompressed: 121
Downloaded: 165 file(s) [attempted 165/8459 = 1%, 59 KB/s], Decompressed: 131
Downloaded: 206 file(s) [attempted 206/8459 = 2%, 445 KB/s], Decompressed: 131
Downloaded: 248 file(s) [attempted 248/8459 = 2%, 696 KB/s], Decompressed: 240
Downloaded: 285 file(s) [attempted 285/8459 = 3%, 1004 KB/s], Decompressed: 278
Downloaded: 329 file(s) [attempted 329/8459 = 3%, 147 KB/s], Decompressed: 323
Downloaded: 364 file(s) [attempted 364/8459 = 4%, 89 KB/s], Decompressed: 357
Downloaded: 401 file(s) [attempted 401/8459 = 4%, 1150 KB/s], Decompressed: 398
Downloaded: 446 file(s) [attempted 446/8459 = 5%, 317 KB/s], Decompressed: 432
Downloaded: 487 file(s) [attempted 487/8459 = 5%, 27 KB/s], Decompressed: 477
Downloaded: 518 file(s) [attempted 518/8459 = 6%, 731 KB/s], Decompressed: 514
Downloaded: 559 file(s) [attempted 559/8459 = 6%, 57 KB/s], Decompressed: 556
Downloaded: 597 file(s) [attempted 597/8459 = 7%, 308 KB/s], Decompressed: 593
Downloaded: 641 file(s) [attempted 641/8459 = 7%, 244 KB/s], Decompressed: 627
Downloaded: 686 file(s) [attempted 686/8459 = 8%, 254 KB/s], Decompressed: 675
Downloaded: 713 file(s) [attempted 713/8459 = 8%, 289 KB/s], Decompressed: 710
Downloaded: 754 file(s) [attempted 754/8459 = 8%, 226 KB/s], Decompressed: 751
Downloaded: 795 file(s) [attempted 795/8459 = 9%, 146 KB/s], Decompressed: 792
Downloaded: 836 file(s) [attempted 836/8459 = 9%, 71 KB/s], Decompressed: 833
Downloaded: 874 file(s) [attempted 874/8459 = 10%, 155 KB/s], Decompressed: 864
Downloaded: 912 file(s) [attempted 912/8459 = 10%, 295 KB/s], Decompressed: 908
Downloaded: 953 file(s) [attempted 953/8459 = 11%, 847 KB/s], Decompressed: 946
Downloaded: 994 file(s) [attempted 994/8459 = 11%, 154 KB/s], Decompressed: 991
Downloaded: 1037 file(s) [attempted 1037/8459 = 12%, 736 KB/s], Decompressed: 1032
Downloaded: 1076 file(s) [attempted 1076/8459 = 12%, 257 KB/s], Decompressed: 1073
Downloaded: 1107 file(s) [attempted 1107/8459 = 13%, 509 KB/s], Decompressed: 1100
Downloaded: 1148 file(s) [attempted 1148/8459 = 13%, 365 KB/s], Decompressed: 1141
Downloaded: 1187 file(s) [attempted 1187/8459 = 14%, 186 KB/s], Decompressed: 1182
Downloaded: 1230 file(s) [attempted 1230/8459 = 14%, 270 KB/s], Decompressed: 1223
Downloaded: 1268 file(s) [attempted 1268/8459 = 14%, 632 KB/s], Decompressed: 1254
Downloaded: 1309 file(s) [attempted 1309/8459 = 15%, 264 KB/s], Decompressed: 1295
Downloaded: 1346 file(s) [attempted 1346/8459 = 15%, 161 KB/s], Decompressed: 1345
Downloaded: 1388 file(s) [attempted 1388/8459 = 16%, 463 KB/s], Decompressed: 1384
Downloaded: 1429 file(s) [attempted 1429/8459 = 16%, 61 KB/s], Decompressed: 1425
Downloaded: 1473 file(s) [attempted 1473/8459 = 17%, 25 KB/s], Decompressed: 1466
Downloaded: 1514 file(s) [attempted 1514/8459 = 17%, 53 KB/s], Decompressed: 1507
Downloaded: 1555 file(s) [attempted 1555/8459 = 18%, 118 KB/s], Decompressed: 1550
Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 136 KB/s], Decompressed: 1589
Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 1056 KB/s], Decompressed: 1627
Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 76 KB/s], Decompressed: 1665
Downloaded: 1709 file(s) [attempted 1709/8459 = 20%, 922 KB/s], Decompressed: 1706
Downloaded: 1752 file(s) [attempted 1752/8459 = 20%, 686 KB/s], Decompressed: 1747
Downloaded: 1788 file(s) [attempted 1788/8459 = 21%, 53 KB/s], Decompressed: 1785
Downloaded: 1826 file(s) [attempted 1826/8459 = 21%, 554 KB/s], Decompressed: 1822
Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1760 KB/s], Decompressed: 1860
Downloaded: 1908 file(s) [attempted 1908/8459 = 22%, 227 KB/s], Decompressed: 1901
Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 654 KB/s], Decompressed: 1942
Downloaded: 1983 file(s) [attempted 1983/8459 = 23%, 75 KB/s], Decompressed: 1976
Downloaded: 2017 file(s) [attempted 2017/8459 = 23%, 58 KB/s], Decompressed: 2014
Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 143 KB/s], Decompressed: 2052
Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 1094 KB/s], Decompressed: 2096
Downloaded: 2134 file(s) [attempted 2134/8459 = 25%, 260 KB/s], Decompressed: 2130
Downloaded: 2178 file(s) [attempted 2178/8459 = 25%, 83 KB/s], Decompressed: 2168
Downloaded: 2219 file(s) [attempted 2219/8459 = 26%, 111 KB/s], Decompressed: 2209
Downloaded: 2257 file(s) [attempted 2257/8459 = 26%, 157 KB/s], Decompressed: 2253
Downloaded: 2303 file(s) [attempted 2303/8459 = 27%, 2016 KB/s], Decompressed: 2298
Downloaded: 2336 file(s) [attempted 2336/8459 = 27%, 85 KB/s], Decompressed: 2332
Downloaded: 2374 file(s) [attempted 2374/8459 = 28%, 231 KB/s], Decompressed: 2360
Downloaded: 2411 file(s) [attempted 2411/8459 = 28%, 44 KB/s], Decompressed: 2407
Downloaded: 2448 file(s) [attempted 2448/8459 = 28%, 655 KB/s], Decompressed: 2445
Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 119 KB/s], Decompressed: 2483
Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 585 KB/s], Decompressed: 2527
Downloaded: 2572 file(s) [attempted 2572/8459 = 30%, 159 KB/s], Decompressed: 2568
Downloaded: 2616 file(s) [attempted 2616/8459 = 30%, 395 KB/s], Decompressed: 2613
Downloaded: 2657 file(s) [attempted 2657/8459 = 31%, 59 KB/s], Decompressed: 2654
Downloaded: 2691 file(s) [attempted 2691/8459 = 31%, 803 KB/s], Decompressed: 2688
Downloaded: 2733 file(s) [attempted 2733/8459 = 32%, 584 KB/s], Decompressed: 2729
Downloaded: 2774 file(s) [attempted 2774/8459 = 32%, 1200 KB/s], Decompressed: 2729
Downloaded: 2818 file(s) [attempted 2818/8459 = 33%, 730 KB/s], Decompressed: 2733
Downloaded: 2859 file(s) [attempted 2859/8459 = 33%, 305 KB/s], Decompressed: 2856
Downloaded: 2900 file(s) [attempted 2900/8459 = 34%, 686 KB/s], Decompressed: 2897
Downloaded: 2938 file(s) [attempted 2938/8459 = 34%, 990 KB/s], Decompressed: 2931
Downloaded: 2974 file(s) [attempted 2974/8459 = 35%, 284 KB/s], Decompressed: 2969
Downloaded: 3013 file(s) [attempted 3013/8459 = 35%, 616 KB/s], Decompressed: 3010
Downloaded: 3054 file(s) [attempted 3054/8459 = 36%, 309 KB/s], Decompressed: 3051
Downloaded: 3088 file(s) [attempted 3088/8459 = 36%, 296 KB/s], Decompressed: 3082
Downloaded: 3126 file(s) [attempted 3126/8459 = 36%, 331 KB/s], Decompressed: 3123
Downloaded: 3168 file(s) [attempted 3168/8459 = 37%, 66 KB/s], Decompressed: 3164
Downloaded: 3212 file(s) [attempted 3212/8459 = 37%, 79 KB/s], Decompressed: 3205
Downloaded: 3249 file(s) [attempted 3249/8459 = 38%, 352 KB/s], Decompressed: 3242
Downloaded: 3287 file(s) [attempted 3287/8459 = 38%, 131 KB/s], Decompressed: 3284
Downloaded: 3322 file(s) [attempted 3322/8459 = 39%, 83 KB/s], Decompressed: 3314
Downloaded: 3366 file(s) [attempted 3366/8459 = 39%, 896 KB/s], Decompressed: 3362
Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 206 KB/s], Decompressed: 3403
Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 584 KB/s], Decompressed: 3444
Downloaded: 3487 file(s) [attempted 3487/8459 = 41%, 480 KB/s], Decompressed: 3475
Downloaded: 3523 file(s) [attempted 3523/8459 = 41%, 372 KB/s], Decompressed: 3520
Downloaded: 3568 file(s) [attempted 3568/8459 = 42%, 449 KB/s], Decompressed: 3564
Downloaded: 3612 file(s) [attempted 3612/8459 = 42%, 170 KB/s], Decompressed: 3605
Downloaded: 3659 file(s) [attempted 3659/8459 = 43%, 593 KB/s], Decompressed: 3653
Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 189 KB/s], Decompressed: 3677
Downloaded: 3725 file(s) [attempted 3725/8459 = 44%, 234 KB/s], Decompressed: 3722
Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 1042 KB/s], Decompressed: 3766
Downloaded: 3814 file(s) [attempted 3814/8459 = 45%, 218 KB/s], Decompressed: 3811
Downloaded: 3855 file(s) [attempted 3855/8459 = 45%, 85 KB/s], Decompressed: 3852
Downloaded: 3902 file(s) [attempted 3902/8459 = 46%, 397 KB/s], Decompressed: 3889
Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 73 KB/s], Decompressed: 3920
Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 105 KB/s], Decompressed: 3958
Downloaded: 4009 file(s) [attempted 4009/8459 = 47%, 269 KB/s], Decompressed: 4002
Downloaded: 4057 file(s) [attempted 4057/8459 = 47%, 253 KB/s], Decompressed: 4054
Downloaded: 4102 file(s) [attempted 4102/8459 = 48%, 3591 KB/s], Decompressed: 4088
Downloaded: 4142 file(s) [attempted 4142/8459 = 48%, 67 KB/s], Decompressed: 4129
Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 308 KB/s], Decompressed: 4160
Downloaded: 4208 file(s) [attempted 4208/8459 = 49%, 201 KB/s], Decompressed: 4204
Downloaded: 4252 file(s) [attempted 4252/8459 = 50%, 32 KB/s], Decompressed: 4249
Downloaded: 4297 file(s) [attempted 4297/8459 = 50%, 1197 KB/s], Decompressed: 4293
Downloaded: 4334 file(s) [attempted 4334/8459 = 51%, 223 KB/s], Decompressed: 4331
Downloaded: 4366 file(s) [attempted 4366/8459 = 51%, 24 KB/s], Decompressed: 4358
Downloaded: 4400 file(s) [attempted 4400/8459 = 52%, 163 KB/s], Decompressed: 4396
Downloaded: 4447 file(s) [attempted 4447/8459 = 52%, 94 KB/s], Decompressed: 4444
Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 241 KB/s], Decompressed: 4488
Downloaded: 4531 file(s) [attempted 4531/8459 = 53%, 449 KB/s], Decompressed: 4526
Downloaded: 4564 file(s) [attempted 4564/8459 = 53%, 914 KB/s], Decompressed: 4553
Downloaded: 4601 file(s) [attempted 4601/8459 = 54%, 404 KB/s], Decompressed: 4591
Downloaded: 4642 file(s) [attempted 4642/8459 = 54%, 147 KB/s], Decompressed: 4632
Downloaded: 4683 file(s) [attempted 4683/8459 = 55%, 95 KB/s], Decompressed: 4680
Downloaded: 4728 file(s) [attempted 4728/8459 = 55%, 37 KB/s], Decompressed: 4721
Downloaded: 4762 file(s) [attempted 4762/8459 = 56%, 22 KB/s], Decompressed: 4755
Downloaded: 4796 file(s) [attempted 4796/8459 = 56%, 392 KB/s], Decompressed: 4793
Downloaded: 4837 file(s) [attempted 4837/8459 = 57%, 601 KB/s], Decompressed: 4834
Downloaded: 4878 file(s) [attempted 4878/8459 = 57%, 34 KB/s], Decompressed: 4868
Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 380 KB/s], Decompressed: 4919
Downloaded: 4962 file(s) [attempted 4962/8459 = 58%, 538 KB/s], Decompressed: 4957
Downloaded: 4992 file(s) [attempted 4992/8459 = 59%, 1037 KB/s], Decompressed: 4988
Downloaded: 5034 file(s) [attempted 5034/8459 = 59%, 154 KB/s], Decompressed: 5029
Downloaded: 5077 file(s) [attempted 5077/8459 = 60%, 512 KB/s], Decompressed: 5073
Downloaded: 5118 file(s) [attempted 5118/8459 = 60%, 50 KB/s], Decompressed: 5111
Downloaded: 5149 file(s) [attempted 5149/8459 = 60%, 114 KB/s], Decompressed: 5142
Downloaded: 5190 file(s) [attempted 5190/8459 = 61%, 153 KB/s], Decompressed: 5186
Downloaded: 5234 file(s) [attempted 5234/8459 = 61%, 244 KB/s], Decompressed: 5231
Downloaded: 5281 file(s) [attempted 5281/8459 = 62%, 1168 KB/s], Decompressed: 5275
Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 222 KB/s], Decompressed: 5313
Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 653 KB/s], Decompressed: 5347
Downloaded: 5393 file(s) [attempted 5393/8459 = 63%, 121 KB/s], Decompressed: 5388
Downloaded: 5433 file(s) [attempted 5433/8459 = 64%, 74 KB/s], Decompressed: 5423
Downloaded: 5476 file(s) [attempted 5476/8459 = 64%, 149 KB/s], Decompressed: 5467
Downloaded: 5512 file(s) [attempted 5512/8459 = 65%, 114 KB/s], Decompressed: 5505
Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 1057 KB/s], Decompressed: 5546
Downloaded: 5589 file(s) [attempted 5589/8459 = 66%, 54 KB/s], Decompressed: 5583
Downloaded: 5631 file(s) [attempted 5631/8459 = 66%, 1278 KB/s], Decompressed: 5628
Downloaded: 5669 file(s) [attempted 5669/8459 = 67%, 570 KB/s], Decompressed: 5659
Downloaded: 5710 file(s) [attempted 5710/8459 = 67%, 202 KB/s], Decompressed: 5700
Downloaded: 5748 file(s) [attempted 5748/8459 = 67%, 357 KB/s], Decompressed: 5744

lean_checker exit - duration 30s · created 6/16/2026, 7:03:37 PM

lake build

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
podman cleanup removed verifier container apx-verifier-job-501-runtime-lean_checker-282038-1781635753364854016-1

blueprint_build exit 0 duration 13m 43s · created 6/16/2026, 7:03:37 PM

lake build :blueprint

✔ [16/35] Built Batteries.Lean.NameMapAttribute:c.o (760ms)
✔ [28/35] Built Cli.Basic:c.o (3.3s)
✔ [30/35] Built Cli.Extensions:c.o (588ms)
✔ [33/41] Built Cli:c.o (68ms)
ℹ [3595/3612] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3629/3642] Built PrimeNumberTheoremAnd.StrongPNT (182s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3630/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (67s)
✔ [3634/3643] Built PrimeNumberTheoremAnd.BorelCaratheodory (10s)
✔ [3636/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (10s)
⚠ [3768/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3896/3909] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
⚠ [3960/3988] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
  [apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3962/3988] 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`
⚠ [3964/3988] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3977/3996] 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:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
⚠ [4109/4125] 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`
⚠ [4113/4181] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4116/4181] 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:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4120/4181] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
ℹ [4139/4200] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359: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.
⚠ [4158/4206] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245: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.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4162/4206] 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`
⚠ [4189/4206] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
⚠ [4204/4251] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: 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/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
  ring
Please focus on the current goal, for instance using `·` (typed as "\.").

Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.

Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
  theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    x hx₁
    (by
      cases x₂ <;> norm_num at *; · linarith;
      · exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
    (by
      cases x₂ <;> norm_num at *; · exact_mod_cast hc;
      · exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
  [apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
    Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.

Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
  [apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4674:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4701:8: declaration uses `sorry`
⚠ [4256/4267] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4258/4267] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.

Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:203:39: missing space in the source

This part of the code
  '(3/2) 0.8476'
should be written as
  '(3 / 2)'


Note: This linter can be disabled with `set_option linter.style.whitespace false`
⚠ [4273/4325] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.

Note: This linter can be disabled with `set_option linter.style.show false`
⚠ [4280/4356] 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`
⚠ [4300/4395] 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`
ℹ [4326/4395] 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.
⚠ [4327/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline

Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
⚠ [4334/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4346/4395] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries (28s)
✔ [4372/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (41s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4392/4395] Built PrimeNumberTheoremAnd (156s)
✔ [4393/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (275s)
ℹ [4394/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (314ms)
info: Blueprint indexing
Build completed successfully (4396 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes