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

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-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...