3 ms·
The situation described strikes me as a contemporary analogue of the sorts of dilemmas we might expect in a future of increasingly complex AIs -- more and more
by patcon 11y ago
The situation described strikes me as a contemporary analogue of the sorts of dilemmas we might expect in a future of increasingly complex AIs -- more and more solutions to problems that even the best among us can't possibly understand fully...
- 336f5 11y agoIt also sounds like a motivating example for machine-checked proofs: if one could feed Mochizuki's proof into Coq or something and be assured that it was correct, even if only in a purely formal sense, I suspect there would be much more interest in grappling with the concepts to understand what the proof is doing, whether it's acceptable, and why the proof is correct. As it stands, there's the risk of a wild goose chase.
- jordigh 11y agoIf Mochizuki were able to write a machine-checkable proof, he would also be able to write a human-checkable proof, which is far easier to write.
- kinghajj 11y agoWell, supposedly he did write a human-checkable proof--it's just that the reviewer must be familiar with several of his novel ideas. Like any human-intended proof, there's an assumption of foreknowledge.
- the8472 11y agoAIs are dynamic systems though. You can prod pieces and see what happens. There's no interactive debugger for proofs written in prose.
- asgard1024 11y agoI agree. I am just reading through Gowers paper on automatic theorem proving. I think once the machines are capable of automatic definitions (according to some definition of beautiful which limits to what humans consider beautiful, for example one based on entropy), all the bets are off. Humans will then struggle to understand the concepts involved with their limited brains.
- david_ar 11y ago> In the face of metahuman science, humans have become metascientists. http://www.nature.com/nature/journal/v405/n6786/full/405517a0.html http://www.nature.com/nature/journal/v405/n6786/full/405517a...