4 ms·
This. Mathematics is not really the study of what is the case, it’s the study of why. Even if this was accompanied by a full Coq proof it would be unsatisfactor
by moomin 9y ago
This. Mathematics is not really the study of what is the case, it’s the study of why. Even if this was accompanied by a full Coq proof it would be unsatisfactory because absolutely no insight is being provided.
- AstralStorm 9y agoThose proofs can be cleaned up and analysed. However generating a proof like that in the first place is a really tough task involving searches and codification of advanced known mathematics in Coq proof way. In this way, semi auto prover like Isabelke are nicer fort mathematicians as they will ask about holes...
- ilitirit 9y agoThings that provide no insight now may have theoretical or even practical applications in the future. https://mathoverflow.net/questions/116627/useless-math-that-became-useful/ https://mathoverflow.net/questions/116627/useless-math-that-... I'm not saying that this is the same of Mochizuki's work, but I would not dismiss it solely on the basis that it's "useles".
- moomin 9y agoI don't think anything on that list was bereft of insight, even at the time. This is a context issue: the problem with Mochizuki's work is that no-one has managed to point to a single insight other than the abc conjecture. Whilst it's possible to prove certain results by brute force manipulation, it's not common. High profile results tend to be accompanied with subsidiary insights. The applicability of these insights to real world problems is, for the purposes of this discussion, beside the point. Anyway, I'm basically repeating what people have already said. So I'll stop.