Re:Formalizing 100 Theorems
by contravariant on Friday November 03, 2023 @07:44AM
(#38127295)
> 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.
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.