Verifying an Efficient Algorithm for Computing Bernoulli Numbers
by Manuel Eberl and Peter Lammich
In: Proceedings of ITP 2025
Abstract:
The Bernoulli numbers Bk are a sequence of rational numbers that is ubiquitous in mathematics, but difficult to compute efficiently (compared to e.g. approximating π).
In 2008, Harvey gave the currently fastest known practical way for computing them: his algorithm computes Bk mod p in time O(p log1+o(1) p). By doing this for O(k) many small primes in parallel and then combining the results with the Chinese Remainder Theorem, one recovers the value of Bk as a rational number in O(k2 log2 + o(1) k) time. One advantage of this approach is that the expensive part of the algorithm is highly parallelisable and has very low memory requirements. This algorithm still holds the world record with its computation of B108.
We give a fully verified efficient LLVM implementation of this algorithm. This was achieved by formalising the necessary mathematical background theory in Isabelle/HOL, proving an abstract version of the algorithm correct, and refining this abstract version down to LLVM using Lammich's Isabelle-LLVM framework, including many low-level optimisations. The performance of the resulting LLVM code is comparable with Harvey's original unverified and hand-optimised C++ implementation.
Download preprint PDF (770 KiB)
BibTeX:
@inproceedings{el25,
author="Eberl, Manuel and Lammich, Peter",
title="Verifying an Efficient Algorithm for Computing {B}ernoulli Numbers",
year="2025",
publisher="Leibniz International Proceedings in Informatics",
booktitle="16th International Conference on Interactive Theorem Proving (ITP 2025)",
editor="Forster, Yannick and Keller, Chantal",
address="Dagstuhl, Germany",
note="to appear"
}