A new way to write mathematics | Hacker News Reader

A new way to write mathematics

rjlipton.wordpress.com

17 pointsqubitsam11 comments

This is extremely shallow. This guy deliberately focuses on the most tabloid-style reporting of the HoTT book he could find, a New Scientist piece, and then uses it to attack the book itself for having unsubstantiated grandiose claims. Well, guess what -- you're reading a New Scientist article, what did you expect?

Perhaps it would be more befitting to a person in his position (a CS professor, it appears) to actually critique the book itself. Judging by his rant, it's doubtful he even read it. Otherwise he would have known that the most controversial thing about it is a preference of constructive proof, when possible, as they are generally both more illuminating and rely on fewer assumptions.

More broadly it seems that he's oblivious to the field of automated theorem proving altogether. Why would people devote their lives to ATP if it weren't useful? Of course humans need to derive insight from proofs, but it's also important for them not to have mistakes.

Is he really attacking the book, though?

"I feel compelled to say something about not his work, but the New Scientist article. The article is at best in my opinion misleading."

Horses for courses. Whilst I'm skeptical that we're at the stage where mechanical proof-checking is viable, such a technique would be immensely valuable.

On the other hand, it is of course true that if the proof itself is mechanistic, most mathematicians would feel that a lot of the important essence of the result had been lost.

Voevodsky's work is apparently in the former, and the blog author conflates this with the latter in order to (wrongly) criticise it.

I really disagree. A proof is a proof, doesn't matter if it helps you understand anything or not.

By definition yes, but it's much more valuable if it can also help you understand.

That can't be right. Otherwise you might as well just churn out billions of proofs like "Proof that 34634+7684=42318". Surely the only value in a proof is whether or not it helps you understand something?

The value of a proof is a different matter.

And for example knowing e=mc^2 might be valuable in itself, independent of understanding relativity theory.

I don't know what you mean. e=mc^2 requires at least some understanding to make any use of it, lest you suppose burning a single lump of coal will keep your power station running all week ;-)

And even then, you need to know that "e" stands for "energy"...

It wasn't the best example, but let's take the area of a circle, which is r^2*PI. I don't even know the proof for that by heart, but I can still make use of the information. A proof simply tells me that something is true. Further understanding is just a bonus.

The understanding here is that πr^2 is the area of a circle.

You are saying that this understanding is important/useful even without the proof.

This is in direct contradiction to what you said earlier, where you said the proof was important/useful even without the understanding.

Perhaps we're using the word "understanding" to mean two different things here and that's where the contradiction lies.

Reply on news.ycombinator.com