This is an unofficial reimagining of the Archive of Formal Proofs
Digit Expansionsby Jonas Bayer, Marco David, Abhik Pal and Benedikt Stock