3 ms·
The thing is, I'm not sure if it's quite a matter that most theorems haven't been proven automatically and rather a matter that using an automatically proven th
by joe_the_user 8y ago
The thing is, I'm not sure if it's quite a matter that most theorems haven't been proven automatically and rather a matter that using an automatically proven theorem in another theory to be automatically proven just isn't as easy as using an existing theorem in an ordinary proof.
IE, one definition of a Turing machine might exist but it might not that usable for a given proof's purposes.
I see a bunch of proof referenced here and I recall more elsewhere;
https://madiot.fr/coq100/ https://madiot.fr/coq100/