From 282714fd490780a46e10648ce5998c2a8c87a7c6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 6 May 2026 11:05:57 +1000 Subject: [PATCH] fix: update Chudnovsky problem source link and informal description The previous Springer link (10.1007/s40316-018-0102-6) is dead. Replace with Milla's arXiv paper (1809.00533), which Mathlib already cites as the detailed proof reference. Also spell out the formula in the notes and informal solution so the README is readable without resolving `chudnovskySum` in Mathlib. Co-Authored-By: Claude Opus 4.7 (1M context) --- generated/chudnovsky_formula_for_pi_inv/README.md | 6 +++--- manifests/problems.toml | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/generated/chudnovsky_formula_for_pi_inv/README.md b/generated/chudnovsky_formula_for_pi_inv/README.md index 712fdee..962cf63 100644 --- a/generated/chudnovsky_formula_for_pi_inv/README.md +++ b/generated/chudnovsky_formula_for_pi_inv/README.md @@ -5,9 +5,9 @@ Chudnovsky formula for pi inverse - Problem ID: `chudnovsky_formula_for_pi_inv` - Test Problem: no - 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. +- 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. Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the trusted benchmark and fixed by the repository. diff --git a/manifests/problems.toml b/manifests/problems.toml index 0bc4664..d0d66c4 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -40,9 +40,9 @@ test = false module = "LeanEval.Analysis.Chudnovsky" holes = ["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." +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." [[problem]] id = "pi1_circle_mulEquiv_int"