3 ms·

Things immediately spring to mind: 1. What good is a proof if you don't understand it. My answer: it is super useful. You now know something is true. You may n

Things immediately spring to mind: 1. What good is a proof if you don't understand it. My answer: it is super useful. You now know something is true. You may not understand why it is true, but you can use it and build on it. For example, if I write a piece of code that relies on an impossible to understand proof generated by a machine and gain a x1000 speedup with a guarantee that my shortcut will always work, there's a ton of value in there. But the utility argument is rarely something that resonates with Mathematician, they usually leave these disgustingly material details to others. 2. The modern "proofs" of important theorems, albeit produced by humans, are equivalently impossible to understand to the vast majority of Mathematicians. Mochizuki's Inter-universal Teichmüller theory is an extreme example of this (exactly one person on the planet understands the proof, assuming he's not a full-blown charlatan), but it's the same deal in other sub-fields of Maths. Can you claim to be able to explain/understand the classification of finite groups? The proof is so large and assembled by so many people it basically takes investing one's entire career to come to grasp with it. 3. It won't lead to new mathematics. I don't think it's true, for two reasons: a) who's to say the machines won't invent new mathematics. 2) falling back on humans, once you know something is true, even if you don't understand why, it's like a guiding lightbeam in a dark forest and there's a very good chance that knowing something is true will lead to a simpler, human-graspable proof. There's is a very strong reek of stakhanovism [1] that emanates from the whole "math against the machine stance", it's just sad. [1] https://en.wikipedia.org/wiki/Alexey_Stakhanov https://en.wikipedia.org/wiki/Alexey_Stakhanov [EDIT]: an one more thing : what is this "understanding" you speak of? that's a rather fuzzily defined concept. One way to codify "understanding" is to make something graspable by a human mind, by - sort of - compressing/reducing it to things that are already known/grasped. But then, there's a very good chance that some things just won't lend themselves to such treatment (incompressible if you will, such as theorem whose minimal proof just won't fit in a human mind). I'd still like to know that they're true.

fspeech 6y ago
Try to actually formalize some math. Just definitions and constructions without proofs. See the challenge for yourself. You might gain some different perspective and sympathy for the mathematicians you are ridiculing. Consider this question: how do you know the string of symbols you wrote down actually correspond to the mathematical objects in my head? Conversely, Voevodsky advocated that mathematicians should formalize their reasoning to flush out the subtle bugs from differences in understanding. But representing mathematical concepts is a huge challenge.
ironSkillet 6y ago
Fair points, but you are minimizing the important detail that mathematics is also a social activity, and so any argument about what constitutes mathematics should be viewed with that in mind. Mathematicians are interested in math because they want to understand things (meaning they can construct abstractions and develop logical lines of reasoning that fit within the limits of human cognition), so that they can develop new concepts and utilize existing ones in novel ways. Using a computer to prove a theorem allows you to add to the ledger of "things that are true" (which certainly has value, like you mention), but unless the proof is understandable, you don't harvest any of the other fruit that would normally come over the course of proving the theorem "the natural way" (new abstractions to ponder, new conjectures etc). I would argue that Mochizuki's "proof" occupies the same territory as a 100 GB formal logic proof generated by a computer, if the end result is that the proof is not communicable in a way that other mathematicians can relate to. I'm not against creating machine generated proofs. We just shouldn't pretend they have the same status within "mathematics as a social construct" that a human written proof does.

fspeech 6y ago

Try to actually formalize some math. Just definitions and constructions without proofs. See the challenge for yourself. You might gain some different perspective and sympathy for the mathematicians you are ridiculing. Consider this question: how do you know the string of symbols you wrote down actually correspond to the mathematical objects in my head? Conversely, Voevodsky advocated that mathematicians should formalize their reasoning to flush out the subtle bugs from differences in understanding. But representing mathematical concepts is a huge challenge.

ironSkillet 6y ago

Fair points, but you are minimizing the important detail that mathematics is also a social activity, and so any argument about what constitutes mathematics should be viewed with that in mind. Mathematicians are interested in math because they want to understand things (meaning they can construct abstractions and develop logical lines of reasoning that fit within the limits of human cognition), so that they can develop new concepts and utilize existing ones in novel ways. Using a computer to prove a theorem allows you to add to the ledger of "things that are true" (which certainly has value, like you mention), but unless the proof is understandable, you don't harvest any of the other fruit that would normally come over the course of proving the theorem "the natural way" (new abstractions to ponder, new conjectures etc). I would argue that Mochizuki's "proof" occupies the same territory as a 100 GB formal logic proof generated by a computer, if the end result is that the proof is not communicable in a way that other mathematicians can relate to. I'm not against creating machine generated proofs. We just shouldn't pretend they have the same status within "mathematics as a social construct" that a human written proof does.