4 ms·
I think this points out the necessity to develop better proof assistant systems [1], in particular for automated proof checking [2]. However, I have never inter
by adlq 13y ago
I think this points out the necessity to develop better proof assistant systems [1], in particular for automated proof checking [2]. However, I have never interacted with such systems and thus don't know whether it will be possible to just feed Mochizuki's formidable constructions into it.
[1] http://en.wikipedia.org/wiki/Proof_assistant http://en.wikipedia.org/wiki/Proof_assistant
[2] http://en.wikipedia.org/wiki/Automated_proof_checking http://en.wikipedia.org/wiki/Automated_proof_checking
- kd0amg 13y agoI would not expect so. Mechanized proof systems tend to require a lot more detail than one would put into a proof meant for humans to read. There's been a lot of work in automating part of the generation of a proof, but that still requires a human to look at what the automation came up with and intervene to guide it in the right direction.
- akjj 13y agoDon't forget that you would need to put not just Mochizuki's work into a proof checker, but also everything that it depends on. From what I understand, this is far too much work to be feasible with currently available proof checkers and changing that would require more than incremental improvements.