Are theorem provers like Coq mature enough to prove interesting stuff.
No.14397065 ViewReplyOriginalReport
Quoted By: >>14397087 >>14397157 >>14397175 >>14397180
I was wondering if theorem provers are still at this very early stage where they can only be used to prove toy problems like the sqrt(2) being irrational. Has anyone played with a theorem prover for a while, is it worth learning one?
