The Paradox of the Proof

Thanks. Didn't have the chance to check this morning.

I must have read the article differently from you. I sensed there was a positive attitude towards him, but I didn't feel they were trying to say he had proven the theorem or was so brilliant no one else could grasp it. On the contrary, it seemed like they were saying "This person has been brilliant for quite some time, but this 'proof' seems entirely nonsensical even to the experts in the field."

So to me, that read more as, this is a curiosity that has a deep and interesting past and an even more interesting present.

> I wanted to present an alternative possibility which seems to be disregarded at the moment

That is entirely fair and valid. I just misread your comment as more along the lines of "Does no one else see how obvious it is that this guy is crazy?!" My fault.

> On the topic of Perelman

Yes I was already corrected. I couldn't remember with certainty whether he did or didn't. I thought he had, but then what I remembered about his personality made me reconsider that.

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.

Something like this? http://www.templeos.org/

To me, the most interesting observation about this came from computability theory, of all places.

To some extent, in CS we study completely arbitrary constructs--Turing machines. Turing machines, indeed, are just tools: they're a simple model of a computing machine that makes sense just based on existing technology. Or perhaps we study the lambda calculus which, while less arbitrary than a Turing machine, is still obviously a tool created by a mathematician to perform a particular task. Or maybe we study existing programming languages which are even more arbitrary and contrived than Turing machines.

All these models? Obviously just tools created by people, often for very specific tasks.

But then a surprising fact emerges: no matter which tool we use, we can accomplish exactly the same things! The set of programs we can run is the same--these arbitrary models are all Turing-complete. Somehow, the notion of Turing completeness is extremely robust against all the different models of computation we've come up with.

In fact, it turns out that any "reasonable" model is going to have the same power. And in this case, "reasonable" actually is reasonable--the main restriction is that the model can only do a finite amount of work at each step.

So while any given model is arbitrary, the class of problems they can solve isn't. Rather, this class naturally emerges from the models. It's a natural property of computation rather than merely a human contrivance.

A similar thing happens when you look at programming and logic. We all know about Curry-Howard: it turns out that writing a program and writing a proof are analogous actions. You can map proof from a logic system to a program in a programming language and vice versa. While both logic systems and programming languages are somewhat arbitrary themselves, the fact that they're somehow equivalent hints at some underlying principle.

And that is why I'm fascinated by category theory, which seems to embody this underlying principle. It unifies proofs and programs with categories in what is very much like an extension of Curry-Howard. But then it goes further, and uses exactly the same model to talk about a whole bunch of different things: set theory, topology and even theoretical physics! (And, doubtless, countless more I'm simply unaware of.) While any of these fields are again just tools--including categories themselves--it seems that they all reflect some deep underlying structure.

Now, of course, I haven't addressed a very important point: is this "underlying structure" a reflection of the universe or just a reflection of the human mind? Is it perhaps a reflection of the underlying structure of reasoning itself?

Coming up with a reasonable answer to any of these questions is going to take a lot more thought and a lot more writing, but I lean towards the latter. The underlying ideas--the minimal starting points that are enough to uncover the structures I talked about--are far too simple to just be an artifact of the human mind which is itself wantonly complex.

So perhaps I am a Platonist myself. I've never thought about it in those terms, but it seems broadly consistent with my general ideas about life, the universe and everything.