{"id":1724,"date":"2026-03-13T18:14:48","date_gmt":"2026-03-13T18:14:48","guid":{"rendered":"https:\/\/as.vanderbilt.edu\/math\/?p=1724"},"modified":"2026-03-13T18:15:22","modified_gmt":"2026-03-13T18:15:22","slug":"colloquium-talk-by-dr-joseph-rabinoff-duke-university-march-19th-2026","status":"publish","type":"post","link":"https:\/\/as.vanderbilt.edu\/math\/2026\/03\/13\/colloquium-talk-by-dr-joseph-rabinoff-duke-university-march-19th-2026\/","title":{"rendered":"Colloquium \u2013 Talk by Dr. Joseph Rabinoff (Duke University): March 19th, 2026"},"content":{"rendered":"<p>March 19, 2026 (Thursday), 4:10-5:00 PM SC 5211<\/p>\n<p>Dr. Joseph Rabinoff-Duke University<\/p>\n<p><strong><span class=\"a_GcMg font-feature-liga-off font-feature-clig-off font-feature-calt-off text-decoration-none text-strikethrough-none\"><span data-teams=\"true\">The Chudnovsky Brothers\u2019 Formula for 1\/pi and Formalization<\/span><\/span><\/strong><\/p>\n<p class=\"cvGsUA direction-ltr align-start para-style-body\"><span data-teams=\"true\">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\u2019ll give a survey of the mathematical ingredients underlying the algorithm, which are all classical and fit together in a beautiful way. Then I\u2019ll 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.<\/span><\/p>\n","protected":false},"excerpt":{"rendered":"<p>March 19, 2026 (Thursday), 4:10-5:00 PM SC 5211 Dr. Joseph Rabinoff-Duke University The Chudnovsky Brothers\u2019 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&#8230;<\/p>\n","protected":false},"author":208,"featured_media":1726,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":[],"categories":[7,6],"tags":[],"acf":[],"jetpack_featured_media_url":"https:\/\/as.vanderbilt.edu\/math\/wp-content\/uploads\/sites\/69\/2026\/03\/Joe-Rabinoff.jpg","_links":{"self":[{"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/posts\/1724"}],"collection":[{"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/users\/208"}],"replies":[{"embeddable":true,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/comments?post=1724"}],"version-history":[{"count":2,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/posts\/1724\/revisions"}],"predecessor-version":[{"id":1727,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/posts\/1724\/revisions\/1727"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/media\/1726"}],"wp:attachment":[{"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/media?parent=1724"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/categories?post=1724"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/as.vanderbilt.edu\/math\/wp-json\/wp\/v2\/tags?post=1724"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}