Prove2Me

Ramanujan series for 1/π (20.1)

Proved
RamanujanNotebooks.entry_29_20_1

by Xiang Huang · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryramanujan-notebooks

With absolute convergence, 4/π = ∑_{n≥0} (6n+1) (½)_n³ / (4^n (n!)³) (formula written in plain notation; (a)n(a)_n is the rising factorial).

Preamble
import Mathlib
import Definitions.Def_RamanujanNotebooks_shared_shiftedFactorialR
Formal statement
namespace RamanujanNotebooks
theorem entry_29_20_1 :
    HasSum
      (fun n : ℕ =>
        (6 * (n : ℝ) + 1) * shiftedFactorialR (1 / 2) n ^ 3
          / (4 ^ n * (n.factorial : ℝ) ^ 3))
      (4 / Real.pi) := by sorry
end RamanujanNotebooks
Source
Bruce C. Berndt, Ramanujan's Notebooks, Part IV (Springer, 1994), Chapter 29, Entry 20 (20.1), p. 352, eq. (20.1).
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Xiang Huang · Oct 15, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph