AI Proof WatchKeep up with AI contributions

Irrationality of Volkenborn-normalized 2-adic zeta values

Which individual odd 2-adic zeta values are irrational? The recorded targets narrow Lai’s four-value alternative to smaller lists and then to the project-defined Volkenborn-normalized value zeta2(7)=J(6)/768.

Why it matters and what counts as progress

Why it matters: Identifying one irrational value is stronger than proving that at least one member of a list is irrational.

What counts as progress: A proved irrationality statement with convergence of the defining J(s) limits and normalization explicit, or a shorter irrationality alternative under the same convention.

How the problem developed

  1. 3 Apr 2023 · Partial result [1]

    Li Lai Proved that at least one of the classical 2-adic zeta values ζ₂(7), ζ₂(9), ζ₂(11), and ζ₂(13) is irrational.

  2. 25 Sept 2026 · Formal result [2][3]

    Gaurav Devi and Claude agents Reported a Lean formalization narrowing the alternative to at least one irrational value among the project-defined ζ₂(7), ζ₂(9), and ζ₂(11); a later result narrowed this further to the pair 7 and 9.

  3. 30 Sept 2026 · Formal result [4]

    Gaurav Devi and Claude agents Reported a Lean proof that the project-defined Volkenborn-normalized ζ₂(7) is irrational and that the limits used in its definition exist.

AI contributions 3

Sources

  1. Li Lai, On the irrationality of certain 2-adic zeta values
  2. 2-adic zeta theorem and provenance
  3. 2-adic zeta theorem and provenance
  4. 2-adic zeta proof, provenance and scope
  5. Completed Lean solution
  6. Lean checking report
  7. Identification with classical 2-adic zeta values
  8. Completed Lean solution
  9. Lean proof census and checking report
  10. Completed Lean solution
  11. Lean proof census and checking report
Website timeline

Publication dates and editorial changes.