AI Checked a 48-Year Math Breakthrough in 6 Days

Summary
Presented by the narrator of the “Adem B10” YouTube channel using hand-drawn style animations, the video breaks down the September 2026 proof that $\zeta(5)$ is irrational by Aabir Fauzan. It examines how automated theorem proving and AI models verified the 48-year-old mathematical milestone in just six days, contrasting this rapid verification with the mystery surrounding the extent of generative AI’s role in discovering the proof.

What is shown

• [00:00 - 00:33] Animation introducing Aabir Fauzan’s Zenodo preprint titled “$\zeta(5)$ is Irrational” posted on September 17, 2026, followed six days later by Alex Kontorovich sharing a complete Lean verification on GitHub.
• [00:34 - 01:02] Timeline comparing previous flawed proof attempts in 2011 and 2024 with the 1978 proof of $\zeta(3)$ and setting up three central questions: Is it true? Why does it work? Who wrote it?
• [01:03 - 02:26] Animated visual explanation of the Riemann zeta function at odd and even integers, Euler’s formulas linking even values to powers of $\pi$, and the definition of irrationality via non-repeating decimals.
• [02:27 - 03:34] Historical recap of Roger Apéry’s 1978 presentation in Marseille proving $\zeta(3)$ is irrational (Apéry’s constant), followed by Vadim Zudilin’s 2001 result showing at least one of $\zeta(5), \zeta(7), \zeta(9), \zeta(11)$ is irrational.
• [03:35 - 05:15] Discussion of how modern AI reviewed the preprint: tweets by Elliot Glazer citing OpenAI’s Astra model and Lech Mazur citing GPT-6 Pro, followed by Lean formalizations by Kontorovich (mo271/zeta5) and Dan Romik using Claude agents (29,400 lines), leading Google DeepMind to mark $\zeta(5)$ as solved on September 29.
• [05:16 - 06:35] Breakdown of mathematician Frank Calegari’s analysis of the proof mechanics (constructing polynomials that plunge below any hypothetical rational denominator floor) and its limitations beyond $\zeta(5)$.
• [06:36 - 08:06] Analysis of the author’s generative AI disclosure statement versus Calegari’s suspicion that the work was largely AI-generated, framing the inverted dynamic between 1978 (known human author, slow verification) and 2026 (instant machine verification, unknown creative origin).

Claims & numbers

• The presenter says Aabir Fauzan uploaded the preprint titled “$\zeta(5)$ is Irrational” to Zenodo on September 17, 2026, having never posted a research paper prior [00:09, 00:16].
• The presenter notes that previous failed proof attempts were posted in 2011 and 2024 [00:37].
• The presenter states Roger Apéry presented his proof that $\zeta(3)$ was irrational in June 1978 at age 64 in Marseille, which took two months to fully verify in Helsinki [02:27, 02:52].
• The presenter notes that in 2001, Vadim Zudilin proved at least one number among $\zeta(5), \zeta(7), \zeta(9), \zeta(11)$ is irrational, but could not determine which one [03:18].
• The presenter claims OpenAI’s Astra model and GPT-6 Pro were used to check the 2026 preprint within days of posting [03:47, 03:53].
• The presenter states mathematician Dan Romik used Claude agents to construct a 29,400-line formalization in Lean [04:36].
• The presenter states that on September 29, Google DeepMind marked $\zeta(5)$ as solved on its open problems list [05:08].
• The presenter notes that within 11 days of the preprint, researchers adapted the proof technique to other constants like $\text{Li}_2(1/2)$ and $\text{Li}_2(r)$ [06:24].

Notable quotes

• “The checking is finished. Now the understanding starts.” [05:41]
• “The turnstile tells you every step is allowed. It doesn’t tell you why the path works.” [05:26]
• “In 1978, everyone knew whose idea it was... In 2026, we knew it was true within a week. What we don’t know is whose idea it was.” [07:34, 07:44]

Assessment
An educational video essay and analysis of recent mathematical breakthroughs, illustrated with stylized hand-drawn whiteboard animations. It accurately synthesizes community reactions, published preprints, blog posts from prominent number theorists, and automated Lean formalizations without exaggerated hype.

Described by gemini-3.8-flash on 2026-10-13 from the video’s audio and frames.