All pull requests

Pull requests

• Prove the cotangent zeta expansion for |z| < 1

  #234·chessing234 opened Nov 13, 2026Contributor·2 of 3 tasks·

  ·
  1

• Prove the FKS2 theta floor on [2, exp 30]

  #233·chessing234 opened Nov 13, 2026Contributor·4 of 5 tasks·

  ·
  1

• Derive the finite Chebyshev bound from equation (3.35)

  #231·chessing234 opened Nov 13, 2026Contributor·2 of 3 tasks·

  ·

• Add examples for the finite, endpoint, and convergence hypotheses

  #230·chessing234 opened Nov 13, 2026Contributor·2 of 3 tasks·

  ·

• Add a reproducible audit manifest for a spin-off directory

  #229·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Write a Palomar project only from supplied pins

  #228·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Describe a narrow bridge application instead of guessing

  #227·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Plan node re-verification inside a compute budget

  #226·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Report transitive impact and a concrete repair

  #225·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Compare a spare justification without designating it

  #224·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Explain why a conclusion depends on each unproved leaf

  #223·chessing234 opened Nov 12, 2026Contributor·1 task done·

  ·

• Check optional source dossiers for edition, locator, and rounding

  #222·chessing234 opened Nov 12, 2026Contributor·2 of 3 tasks·

  ·

• Post the network-impact report as one pull request comment

  #221·chessing234 opened Nov 12, 2026Contributor·1 of 2 tasks·

  ·

• Roll back node lifecycle edits when a mutation fails

  #220·chessing234 opened Nov 12, 2026Contributor·1 of 2 tasks·

  ·

• Export the evidence graph as versioned JSON

  #218·chessing234 opened Nov 12, 2026Contributor·1 of 2 tasks·

  ·

• Add RosserSchoenfeld1962.v8: equation (3.19), log log x < ∑_{p≤x} 1/p, with a solution

  #217·mrdevonwright opened Nov 12, 2026·

  ·

• Land FKSNumerics.v1 and FKS.v3 with their Comparator receipts (supersedes #170)

  #216·teorth opened Nov 9, 2026Owner·

  ·

• ZetaZeroLocations v2–v11: the zeros of ζ up to height 10 000, and the count

  #212·Garald1 opened Nov 9, 2026Contributor·

  ·
  2

• Add ZetaZeroLocations.v1 and Schoenfeld1976Numerics.v1, with a solution

  #211·Garald1 opened Nov 8, 2026Contributor·

  ·
  1

• Add Schoenfeld1976.v1: Theorem 7* and Theorem 11

  #210·Garald1 opened Nov 8, 2026Contributor·

  ·
  4

• State the hypotheses the declarations already require

  #209·chessing234 opened Nov 8, 2026Contributor·

  ·
  1

• Add RosserYoheSchoenfeld.v1: RH up to 1894438.5122 (the first 3 502 5…

  #207·Garald1 opened Nov 7, 2026Contributor·

  ·
  1

• Handle quoted Lean identifiers in source checks

  #206·chessing234 opened Nov 6, 2026Contributor·

  ·

• Give new standalone solutions the pinned Lean toolchain

  #205·chessing234 opened Nov 6, 2026Contributor·

  ·

• Preserve nested solution modules in standalone exports

  #200·chessing234 opened Nov 5, 2026Contributor·

  ·
  2