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.

https://youtu.be/Dp-mQ3HxgDE?si=8a0d6ci-7a-yfhou

▲

griffzhowl 5 days ago | parent | next [-]

He's one of the leaders of this project to formalise Fermat's last theorem too

	▲	ljlolel 5 days ago \| parent [-]
		He’s also commenting in this thread!

▲

monkeyelite 5 days ago | parent | prev [-]

Thanks