CYK - Archive of Formal Proofs