3 ms·
I'm not saying that proof is bad or result isn't result enough, or that computer cannot help with math research — that would be ridiculous to say. But I strongl
by krick 12y ago
I'm not saying that proof is bad or result isn't result enough, or that computer cannot help with math research — that would be ridiculous to say. But I strongly feel that all the news these days about results like this one are something that could be called either "overreaction" or "misunderstanding". Using computer to brute-force through hypothesis might be useful, and works like Voevodsky's one are both cool and useful, but when something like that becomes overrated it seems kinda sad to me.
"Machines do the grunt work and leave humans free for deeper thinking", really? Let me put it this way: what is the most important thing about, say, Pythagorean theorem? From the engineer's point of view it could be ability to find the length of the side of right triangle given the other two or something like that. From the mathematical point of view the most important thing about that or any other theorem is its proof. It isn't actually that important that you cannot divide arbitrary angle by 3 equal parts using only compass and the ruler — the way how you prove it is what really matters.
So, once again, autoverifiers are wonderful and so on, but if someone thinks that writing incomprehensible, but correct proofs is as fine as it gets — it's huge mistake to think so. Math is not about constructing and computing, it is about understanding in the first place.
- Strilanc 12y agoThis was far more than a brute force search. Thomas Hales did a talk about the proof and during the QA he mentioned that the proof was improved a lot as part of formalizing it into HOL. The process even lead to solutions of other problems [1]. 1: http://youtu.be/DJx8bFQbHsA?t=40m57s http://youtu.be/DJx8bFQbHsA?t=40m57s
- sillysaurus3 12y agoThe four color theorem was proved by brute forcing every possible contradiction with a computer and finding that no contradiction existed. Therefore the four color theorem was proved to be true. Why is that a problem?
- lutusp 12y agoAt the time, the problem was that most reviewers couldn't understand the code that produced the result, so they felt that they were accepting a result they couldn't meaningfully review or independently confirm. A lesser issue was philosophical -- it didn't seem like mathematics was "supposed" to be conducted. This second issue has pretty much evaporated in the intervening years.
- nmrm2 12y ago> but if someone thinks that writing incomprehensible but correct proofs is as fine as it gets — it's huge mistake to think so. In the brute force case, it's simply a conceit of mathematicians that algorithms implemented in a programming language are incomprehensible. If our proofs can span hundreds of pages, why not also our programs? Accepting the premise that large algorithms and their results can be used as part of a proof, have you ever proven a program correct by hand? It's almost always tedious and unenlightening.