Open utterances-bot opened 2 years ago
I think the biggest reason for formalization right now might be to enable large machine learning models to learn theorem proving. That could automate away a lot of low level (or maybe even high level) theorem proving.
What is the point of formalising mathematics?
https://lawrencecpaulson.github.io/2022/06/22/Why-formalise.html