-
Notifications
You must be signed in to change notification settings - Fork 112
Pull requests: AlexKontorovich/PrimeNumberTheoremAnd
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat(StrongPNT): formalize Zero-Free Strip log-deriv bounds and contour estimates (I2New, I3New, I4New)Feat/strong pnt delta range bound
#1752
opened Aug 19, 2026 by
navindutta
Loading…
[StrongPNT]: Log Deriv Zeta Log Squared Estimate
#1751
opened Aug 18, 2026 by
prestontranbarger
Contributor
Loading…
chore(IK): give the comparison-test lemma its own blueprint label
#1750
opened Aug 17, 2026 by
Chessing234
Contributor
Loading…
feat(IK): prove the three divisor-decomposition lemmas locally
#1749
opened Aug 17, 2026 by
Chessing234
Contributor
Loading…
feat(IK): prove zeta_pow_four_eq and zeta_pow_three_eq_alt from the Euler-product zeta^3
#1748
opened Aug 17, 2026 by
Chessing234
Contributor
Loading…
feat(IK): prove isCompletelyMultiplicative_liouville
ai
Formalised using AI.
claude
Formalised using Claude models by Anthropic.
#1746
opened Aug 14, 2026 by
Chessing234
Contributor
Loading…
2 of 3 tasks
chore(IK): golf LSeries_totient_eq proof
awaiting-review
#1731
opened Aug 2, 2026 by
pink-iguana
Loading…
feat(IK): prove zeta_mul_zeta_mul_zeta_mul_zeta_eq (IK 1.28)
ai
Formalised using AI.
claude
Formalised using Claude models by Anthropic.
#1730
opened Aug 1, 2026 by
Robby955
Contributor
Loading…
5 of 6 tasks
Chore (MediumPNT): some proof simplification
#1714
opened Jul 25, 2026 by
ajirving
Contributor
Loading…
Chore (MediumPNT): Move an golf some residue results
#1637
opened Jul 11, 2026 by
ajirving
Contributor
Loading…
IK: fill three divisor-sum infra lemmas (#1011)
ai
Formalised using AI.
awaiting-review
claude
Formalised using Claude models by Anthropic.
#1554
opened Jun 13, 2026 by
Robby955
Contributor
Loading…
5 of 6 tasks
feat(IK): prove LSeries_liouville_eq
awaiting-review
#1533
opened Jun 12, 2026 by
giuseppesorge
Contributor
Loading…
ProTip!
Follow long discussions with comments:>50.