この記事の日本語版はまだありません。英語版を表示しています。

Apéry-style irrationality proofs: ζ(5) and Catalan's constant

A preprint proving that ζ(5) is irrational, now formalized in Lean by a third party, led Epoch AI to mark this open problem solved by human and AI; no primary source we found describes the AI's role.

問題
Can Apéry's 1979 recurrence method for the irrationality of ζ(3)\zeta(3) be extended to other famous constants?
貢献
Aabir Fauzan (ζ(5)); OpenAI internal model (Catalan's constant) · Human preprint with AI assistance per Epoch AI; separate OpenAI preprint
検証
Lean formalization of the ζ(5) proof (third party)Marked solved (human + AI) by Epoch AI
経緯
Apéry 1979 → ζ(5) preprint 2026-09-17 → Catalan preprint released 2026-10-06
出典
Epoch AI problem pageζ(5) preprint (Zenodo)Lean formalization of ζ(5)
未検証AI's role unconfirmed

The problem

In 1979 Roger Apéry proved that ζ(3)\zeta(3) is irrational using a pair of linear recurrences. Epoch AI's FrontierMath Open Problems, which rates this problem a "breakthrough", asks for proofs of the same kind for other famous constants.

What AI did

Two results are behind Epoch AI's "solved" label:

  • ζ(5)\zeta(5) is irrational. A preprint by Aabir Fauzan (Aalto University) was posted on Zenodo on 17 September 2026. Its proof is not in fact Apéry-style, but Epoch AI counts the problem as solved. Epoch says it believes the work meets its "human + AI" standard, but neither the preprint page nor the formalization's README mentions AI.
  • Catalan's constant is irrational. This is a preprint (dated 24 September) in the batch OpenAI released on 6 October 2026, result family 005.

How it was checked

GitHub user mo271 formalized the ζ(5)\zeta(5) proof in Lean. The formalization is complete, has no sorry, uses only the standard axioms, and is checked against the Formal Conjectures statement of the theorem. It departs from the paper in some constants and lemmas. The Catalan result has OpenAI's own Lean link and no independent check.

Limitations

The ζ(5)\zeta(5) proof has strong formal evidence behind it, but we could not confirm from a primary source what AI contributed to it, so we grade this record "unverified" until that is clear. Neither preprint has been peer reviewed. Problem description paraphrased from Epoch AI (CC BY 4.0).

∎