http://www21.in.tum.de/~ballarin/
This is an unofficial reimagining of the Archive of Formal Proofs
A Case Study in Basic Algebraby Clemens Ballarin
Fast Fourier Transformby Clemens Ballarin