This is an unofficial reimagining of the Archive of Formal Proofs
Optimal Binary Search Treesby Tobias Nipkow and Dániel Somogyi