This is an unofficial reimagining of the Archive of Formal Proofs
Closest Pair of Points Algorithmsby Martin Rau and Tobias Nipkow
Multidimensional Binary Search Treesby Martin Rau