All pull requests

Pull requests

• Chore: bump deps to V4.35.0

  #1798·ajirving opened Oct 17, 2026Contributor·

  ·

• chore(deps): bump leanprover/lean-action from 1.6.0 to 1.6.2

  dependenciesgithub_actions
  #1797·dependabot[bot] opened Oct 16, 2026Bot·

  ·

• feat(support): generalize Mellin support lemmas

  aigpt
  #1795·Chessing234 opened Oct 4, 2026Contributor·

  ·

• feat(integrals): expose Fubini and support localization API

  aigpt
  #1794·Chessing234 opened Oct 4, 2026Contributor·

  ·

• feat(limits): generalize Perron constant-limit helpers

  aigpt
  #1793·Chessing234 opened Oct 4, 2026Contributor·

  ·

• refactor(contours): expose contour limits without Perron

  aigpt
  #1792·Chessing234 opened Oct 4, 2026Contributor·

  ·

• feat(LSeries): add convergent prime-power sum API

  aigpt
  #1791·Chessing234 opened Oct 4, 2026Contributor·

  ·

• feat(LSeries): package multiplicative terms as arithmetic functions

  aigpt
  #1790·Chessing234 opened Oct 4, 2026Contributor·

  ·

• feat(LSeries): compare convergence at the coefficient level

  aigpt
  #1789·Chessing234 opened Oct 4, 2026Contributor·

  ·

• feat(IK): add additive arithmetic function power API

  aigpt
  #1788·Chessing234 opened Oct 4, 2026Contributor·

  ·

• Chore StrongPNT: use some existing results

  #1786·ajirving opened Oct 1, 2026Contributor·

  ·

• feat(LSeries): bound nonnegative series on right half-planes

  #1785·Chessing234 opened Oct 1, 2026Contributor·

  ·
  1

• feat(Mellin): generalize Haar power substitution to RCLike

  #1784·Chessing234 opened Oct 1, 2026Contributor·

  ·

• fix(ci): detect core modules outside the root import closure

  #1783·Chessing234 opened Oct 1, 2026Contributor·

  ·

• feat(TMEEMT): fill Dusart θ bound from Table 4.2 k=1 row

  aiawaiting-reviewcursor
  #1778·Chessing234 opened Sep 16, 2026Contributor·1 task·

  ·
  1

  1

• feat(TMEEMT): fill Dusart θ bounds from Table 4.2 k=3 rows

  aiawaiting-reviewcursor
  #1777·Chessing234 opened Sep 16, 2026Contributor·1 task·

  ·
  1

  1

• feat(TMEEMT): fill Dusart θ bounds from Table 4.2 k=2 rows

  aiawaiting-reviewcursor
  #1776·Chessing234 opened Sep 16, 2026Contributor·1 task·

  ·
  1

  1

• feat(IK): combine Ch1 divisor, zeta^4, and Liouville proofs

  aiawaiting-reviewcursor
  #1772·Chessing234 opened Sep 16, 2026Contributor·2 tasks·

  ·
  1

• feat(BKLNW): formalize Lemma 10

  aiclaude
  #1768·lsmeng opened Aug 27, 2026·

  ·

• feat(TMEEMT): fill Dusart1999.pi_inequality from Dusart corollary 5.3(a)

  aiawaiting-reviewcursor
  #1767·Chessing234 opened Aug 26, 2026Contributor·2 tasks·

  ·
  1

  4

• feat(StrongPNT): formalize Zero-Free Strip log-deriv bounds and contour estimates (I2New, I3New, I4New)Feat/strong pnt delta range bound

  #1752·navindutta opened Aug 19, 2026·

  ·
  5

• chore(IK): golf LSeries_totient_eq proof

  awaiting-review
  #1731·pink-iguana opened Aug 2, 2026·

  ·
  1

  2

• feat(IK): prove zeta_mul_zeta_mul_zeta_mul_zeta_eq (IK 1.28)

  aiclaude
  #1730·Robby955 opened Aug 1, 2026Contributor·5 of 6 tasks·

  ·
  1

• Chore (MediumPNT): Move an golf some residue results

  #1637·ajirving opened Jul 11, 2026Contributor·

  ·

• IK: fill three divisor-sum infra lemmas (#1011)

  aiawaiting-reviewclaude
  #1554·Robby955 opened Jun 13, 2026Contributor·5 of 6 tasks·

  ·
  6