News · 2026-09-28

Epoch marks a claimed AI-assisted ζ(5) proof as solved, with public Lean code but no settled consensus

Epoch has marked its Apéry irrationality target as solved “human + AI” after a September preprint claimed a proof that ζ(5) is irrational and linked public Lean formalization. The event is unusually checkable for an AI-math claim, but it is not yet the same as a theorem accepted through independent human mathematical review.

Key facts

• Status: Epoch's problem page labels the target “Solved (human + AI)” and “Breakthrough.”
• Preprint: Aabir Fauzan's Zenodo record, “ζ(5) is irrational,” is dated 17 September 2026.
• Formal artifact: Epoch links the public mo271/Zeta5 Lean repository.
• Important limit: the model is unnamed, the source's AI contribution is unclear and independent acceptance is not established.

The target is a classic-looking problem with modern visibility. Apéry proved ζ(3) irrational in 1978, but individual irrationality of ζ(5) remained a natural open question. Epoch's page is specifically about a family of Apéry-style irrationality targets and records the result as human-plus-AI rather than crediting a named model. The paper claims a proof; calling it the first proof or a settled theorem would go beyond the evidence.

Why is this story different from a typical “AI solved math” post? There is a receipt. The preprint is public, the formal repository is public, and the code has a theorem endpoint referring to riemannZeta. A reader with the relevant environment can inspect and attempt to build the artifact. That is much stronger evidence than an unnamed lab saying its model found many solutions without publishing any of them.

But formal verification has a precise boundary. A proof assistant is like an exceptionally strict accountant: it checks that every formally stated line follows from its declared rules and imports. It does not decide whether the formalization matches the informal paper at every conceptual turn, whether a dependency carries an assumption the author overlooked, whether the theorem is novel or whether an AI did the work attributed to it. The repository itself identifies an imported Prime Number Theorem dependency; a separate audit-oriented repository makes an explicit axiom boundary visible.

The primary number to hold onto is not a benchmark score but the date: 17 September. This is fresh enough that the social process of proof validation has barely begun. Epoch's FAQ says its verifiers can provide strong numerical evidence without constituting a full proof and that mathematician confirmation is a separate milestone. The checked public problem page does not name the mathematician who performed such confirmation.

Reaction among mathematically engaged readers is cautious. A technical Persiflage discussion traces the construction to established moment, Hankel and Padé-style machinery while questioning what is new. A MathOverflow thread records both interest in the Lean artifact and skepticism about provenance and the claimed role of AI. These are reactions, not proof audits; their value is showing where the live dispute lies.

The strongest counterargument is that a public Lean repository can create an illusion of closure. It is an unusually valuable artifact, but only if experts verify the specification, dependencies and correspondence to the paper. Conversely, dismissing it because the preprint may have involved AI would miss the methodological advance: it gives critics something concrete to inspect.

This is an ideal case study for proof assistants and autoformalization. The honest headline is not that AI has definitively settled number theory. It is that a claimed AI-assisted result on a real target comes with a formal object whose trust boundary can be examined in public. The verification bottleneck has moved—from “show us anything” to “show that the formal artifact, paper and attribution line up.”

Primary source, verified: read the paper →

Ground Truth. (2026, September 28). Epoch marks a claimed AI-assisted ζ(5) proof as solved, with public Lean code but no settled consensus. Ground Truth. https://groundtruth.day/news/epoch-zeta5-claimed-ai-assisted-proof-lean.html

@misc{groundtruth:epoch-zeta5-claimed-ai-assisted-proof-lean,
  title  = {Epoch marks a claimed AI-assisted ζ(5) proof as solved, with public Lean code but no settled consensus},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/news/epoch-zeta5-claimed-ai-assisted-proof-lean.html}
}

Topics: research · mathematics · proof-assistants · evaluation · ai-for-science