even if a proof is well established, porting it to a proof language allows other proofs to build upon it, like importing dependencies in traditional software de

even if a proof is well established, porting it to a proof language allows other proofs to build upon it, like importing dependencies in traditional software development. And the bigger the library of proofs gets, the more possibilities there are for things like automating proofs using search/AI. But I think on top of that, it just serves as a cool milestone because I've heard some people say porting all of mathemetics will take decades, so seeing fundamental theorems like this make it in marks great progress.