All pull requests

Pull requests

• blueprint updates + further modulization

  #1802·prestontranbarger opened Nov 2, 2026Contributor·

  ·

• feat(TMEEMT): fill the open Dusart restatements together

  aicursor
  #1799·chessing234 opened Oct 23, 2026Contributor·1 task·

  ·
  4

  1

• 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(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(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

• feat(IK): prove LSeries_liouville_eq

  awaiting-review
  #1533·giuseppesorge opened Jun 12, 2026Contributor·

  ·
  1

  6

• feat(Hadamard/Kadiri): connect Hadamard API to Kadiri’s Hadamard constant B and the -ζ'/ζ logarithmic-derivative formula

  #1505·or4nge19 opened Jun 7, 2026Contributor·

  ·
  1

• Partial work on remark_after_corollary_11

  #1403·Aaron1011 opened May 21, 2026Contributor·

  ·