This is an unofficial reimagining of the Archive of Formal Proofs
Open Inductionby Mizuhito Ogawa and Christian Sternagel