> But seems odd to me there isn't more of a movement to formalise all proofs. Well, from the perspective of mathematicians all known proofs are formalized by d

> But seems odd to me there isn't more of a movement to formalise all proofs. Well, from the perspective of mathematicians all known proofs are formalized by definition (to some extent anyway). Putting them through a proof checker is not completely without merit, but is not exactly highest priority. As for discovering new proofs, it's a bit tricky to tell a computer what to find interesting. And the reasoning behind a proof is often more important than the exact steps themselves.