Re:Formalizing 100 Theorems
by BeetleB on Friday November 03, 2023 @12:42PM
(#38131271)
> I don't know much about modern mathematics. But seems odd to me there isn't more of a movement to formalise all proofs.
Only a tiny percentage of mathematicians use such systems. Historically they arose from CS, not math, so most mathematicians aren't trained in it. And until recently, the two camps spoke different languages (i.e. different terminology for the same concept), so there was a barrier for a given mathematician to learn, say, Coq.
It's also very time consuming. A proof a mathematician can write down in 10 minutes may take him a day to formalize in a proof assistant.
Still, things are changing, and more mathematicians are toying with them. You can see Terence Tao experimenting with Lean on his Mastodon account: https://mathstodon.xyz/@tao
Only a tiny percentage of mathematicians use such systems. Historically they arose from CS, not math, so most mathematicians aren't trained in it. And until recently, the two camps spoke different languages (i.e. different terminology for the same concept), so there was a barrier for a given mathematician to learn, say, Coq.
It's also very time consuming. A proof a mathematician can write down in 10 minutes may take him a day to formalize in a proof assistant.
Still, things are changing, and more mathematicians are toying with them. You can see Terence Tao experimenting with Lean on his Mastodon account: https://mathstodon.xyz/@tao