They only proved that one exists; computing the actual construction is non-obvious (the naive way to construct it is computationally infeasible).