Chudnovsky formula for pi inverse

← All problems

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.

Source: https://link.springer.com/article/10.1007/s40316-018-0102-6

Informal solution: Evaluate the Chudnovsky series and prove that it sums to 1 / pi.

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

Solved by

Not yet solved.