Because they have hundreds of potential proofs they were sitting on, and lack the internal expertise to judge them. It seems like they're working to formalize all of the in Lean, but that takes time.