Email Gateway (Jul 08 2026 at 22:04): Email Gateway (Jul 08 2026 at 22:04):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Very happy to announce 6 (in words: six) new AFP entries by Manuel Eberl (in one case jointly with Larry Paulson).
At the same time, we are celebrating AFP the 1000th entry (strictly speaking, entries number 1000 to 1005). I suggest treating the entry by Manuel and Larry as AFP entry number 1000, even if dependency-wise this is not the first one to come.
I wished I could say more about the mathematics, but the author(s) have prepared abstracts with beautifully typeset mathematical formulas—to avoid butchering them in this email, I omit them: please click on the links. I will point out that Manuel still has not formalized the Geothmetic Meandian (https://xkcd.com/2435/)—a major omission. Perhaps he is saving this for his 100th AFP entry, which he is rapidly approaching.
Manuel Eberl, Complete Elliptic Integrals and the Arithmetic–Geometric Mean, https://isa-afp.org/entries/Arithmetic_Geometric_Mean.html
Manuel Eberl, Bessel Functions of the First Kind, https://isa-afp.org/entries/Bessel.html
Manuel Eberl, The Exponential and Logarithmic Integral, https://isa-afp.org/entries/Exp_Log_Integral.html
Manuel Eberl, Generalised Hypergeometric Series, https://isa-afp.org/entries/Generalized_Hypergeometric_Series.html
Manuel Eberl, The Incomplete Gamma Function, https://isa-afp.org/entries/Incomplete_Gamma.html
Manuel Eberl and Lawrence C. Paulson, Rademacher's Series for the Partition Function, https://isa-afp.org/entries/Rademacher_Series.html
Enjoy x 6!
Last updated: Jul 22 2026 at 14:00 UTC