Chudnovsky formula for pi inverse

chudnovsky_formula_for_pi_inv

Submitter: Kim Morrison.

Notes: Uses the existing Mathlib definition of the Chudnovsky series and asks for the missing identity with pi inverse. The Chudnovsky formula states 1/π = (12 / 640320^(3/2)) · ∑_{n=0}^∞ (-1)^n · (6n)! · (545140134·n + 13591409) / ((3n)! · (n!)^3 · 640320^(3n)).

Source: https://arxiv.org/abs/1809.00533

Informal solution: Prove that the Chudnovsky series 1/π = (12 / 640320^(3/2)) · ∑_{n=0}^∞ (-1)^n · (6n)! · (545140134·n + 13591409) / ((3n)! · (n!)^3 · 640320^(3n)) holds, e.g. following Milla's detailed complex-analytic proof.

theorem declaration uses `sorry`chudnovsky_formula_for_pi_inv :
    chudnovskySum = π⁻¹ := by⊢ chudnovskySum = π⁻¹
  sorryAll goals completed! 🐙

Solved by

• @ldct with Claude Opus 4.8 + Fable 5 (multi-agent) on Jul 5, 2026

• @rishistyping with Stealth Model on Jul 5, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jul 21, 2026