This is just not accurate.

"I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research." Peter Scholze [1].

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