Hacker News Reader

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

[2] http://en.wikipedia.org/wiki/Automated_proof_checking

View on HN

I 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.

Don'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.

Reply on news.ycombinator.com