This is an unofficial reimagining of the Archive of Formal Proofs
Completeness theoremby James Margetson and Tom Ridge