5 ms·

Proof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexi

by fmap 9y ago

Proof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexity theory for you...

soberhoff 9y ago
Well, I'm sure we can all agree that the mathematical paper we're discussing could be formalized into a proof that could be checked in linear time.
- Blaisorblade0 9y ago
  That's only obvious in a vacuous sense. As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians: https://mathoverflow.net/q/226966/36016 https://mathoverflow.net/q/226966/36016 Of course, your claim is vacuously true, since you can add a trace of all steps of a proof verifier. It's also vacuously true because you can add a dump of the Internet to the proof. Neither thing is insightful. > what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step Also, for the record: actual formal proofs for (say) standard ZFC are exponentially bigger than anything you want to work with. EDIT: To clarify, I didn't mean to imply I'm some authority, just to suggest I'm not so obviously* an idiot. Which was maybe stupid anyway.
  - 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 ago
      Wow, 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

by fmap 9y ago

Proof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexity theory for you...

soberhoff 9y ago

Well, I'm sure we can all agree that the mathematical paper we're discussing could be formalized into a proof that could be checked in linear time.

Blaisorblade0 9y ago
That's only obvious in a vacuous sense. As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians: https://mathoverflow.net/q/226966/36016 https://mathoverflow.net/q/226966/36016 Of course, your claim is vacuously true, since you can add a trace of all steps of a proof verifier. It's also vacuously true because you can add a dump of the Internet to the proof. Neither thing is insightful. > what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step Also, for the record: actual formal proofs for (say) standard ZFC are exponentially bigger than anything you want to work with. EDIT: To clarify, I didn't mean to imply I'm some authority, just to suggest I'm not so obviously* an idiot. Which was maybe stupid anyway.
- 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 ago
    Wow, 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