4 ms·
A new way to write mathematics
- zepolud 13y agoThis 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.
- foobarbazqux 13y agoMore 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.
- tome 13y agoIs 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."
- Tichy 13y agoI really disagree. A proof is a proof, doesn't matter if it helps you understand anything or not.
- tome 13y agoBy definition yes, but it's much more valuable if it can also help you understand.
- phaemon 13y agoThat 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?
- Tichy 13y agoThe 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.
- phaemon 13y agoI 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"...
- Tichy 13y agoIt 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.
- phaemon 13y agoThe 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.
- phaemon 13y agoI 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"...
- strangestchild 13y agoHorses 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.