It's not out of the question for research-level math to be formalized in proof assistants. Most notably, a landmark paper by Peter Scholze (a Fields medalist) was, at his request, formalized in Lean. Or at least, the important part was formalized in about 6 months. See [1] for the post where Scholze asks for help in formalizing the proof and explains why he thinks it's important - in this case it was a very gnarly proof of a theorem that could hopefully be used as a black box by other mathematicians. See [2] for Scholze's thoughts after the project succeeded, 6 months later.

[1] https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...

[2] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...