4 ms·
For math as an art form (a lot of theoretical math), are computer aided proofs destroying the core value of the endeavor?
by smabie 6y ago
For math as an art form (a lot of theoretical math), are computer aided proofs destroying the core value of the endeavor?
- ogogmad 6y agoI guess the problem with many Computer Assisted Proofs is that they don't explain "why" something is true, only that something is true. But if that's the best you can do, then it's certainly better than nothing. Also, advances in CAPs can have applications outside of pure maths. Finally, CAPs are not common enough - or viable enough in most cases - to make a dent in the practice of pure maths. At least that's the impression I get.
- throwaway_pdp09 6y agoI guess if a human can't do it and a computer can, then no, it's not. What would be the other side to that argument?
- plafl 6y agoI think the art is moved from the proof itself to translating the proof to computer language. Edit: typo
- FartyMcFarter 6y agoThe article explains that the translation from the original problem to the computer-checked problem was quite ingenious. Turning a problem about continuous space to a graph problem, and then using a computer to check the graph problem does not kill much (or any) of the art form I would think.
- kevinventullo 6y agoI think one could only claim destruction if there was evidence that other forms of math were in decline due to computer-aided proofs. As much as we hear about computer-aided proofs and theorem proving software here on HN, these topics are still somewhat niche in mathematics as a whole.