Comment by ookdatnog
I watched this video years ago and found it interesting. It's a talk by Kevin Buzzard, a pure mathematician who got really interested in theorem proving software, and he explains his motivation.
I watched this video years ago and found it interesting. It's a talk by Kevin Buzzard, a pure mathematician who got really interested in theorem proving software, and he explains his motivation.
He's one of the leaders of this project to formalise Fermat's last theorem too