Hacker News Reader

Comment by patcon | Hacker News Reader

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

View on HN

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

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

Well, 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.

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

AIs are dynamic systems though. You can prod pieces and see what happens.

There's no interactive debugger for proofs written in prose.

> In the face of metahuman science, humans have become metascientists.

http://www.nature.com/nature/journal/v405/n6786/full/405517a...

Reply on news.ycombinator.com