Colloquium – Talk by Dr. Joseph Rabinoff (Duke University): March 19th, 2026
March 19, 2026 (Thursday), 4:10-5:00 PM SC 5211
Dr. Joseph Rabinoff-Duke University
The Chudnovsky Brothers’ Formula for 1/pi and Formalization
In 1988, David and Gregory Chudnovsky published a remarkable infinite sum formula for 1/pi. This sum converges extremely quickly, with each summand providing approximately 10 new decimal digits of precision; for this reason, it is the backbone of all modern world-record-setting computations of pi. I’ll give a survey of the mathematical ingredients underlying the algorithm, which are all classical and fit together in a beautiful way. Then I’ll discuss some challenges that need to be overcome in order to formalize the algorithm in Lean, the resolution of which would amount to an efficient, provably correct implementation.