3 ms·
Well, I've spent a lot of time with theorem provers as well as with normal mathematics. I've never experienced an exponential blowup when formalizing mathematic
by soberhoff 9y ago
Well, I've spent a lot of time with theorem provers as well as with normal mathematics. I've never experienced an exponential blowup when formalizing mathematical ideas. It would always boild down to step-by-step verification. And I don't see any reason to suspect that the paper under discussion uses non-standard techniques.
- evincarofautumn 9y agoWow, this got more replies than I expected. I was partly kidding, in that I don’t think it’s a huge concern for humans, but for example the tableau decision procedure[1] for modal logics such as epistemic logic is EXPTIME-complete[2]. [1]: https://en.wikipedia.org/wiki/Method_of_analytic_tableaux https://en.wikipedia.org/wiki/Method_of_analytic_tableaux [2]: https://arxiv.org/abs/0808.4133 https://arxiv.org/abs/0808.4133