4 ms·

The article touches on it a little bit, but I think the main reason mathematicians are hesitant to accept the value of machines is that although they generate a

The article touches on it a little bit, but I think the main reason mathematicians are hesitant to accept the value of machines is that although they generate a "proof" in the technical sense, they usually don't generate "understanding", which is really the currency of mathematicians. What good is a proof if literally no human being can understand it? It won't lead to any new mathematics, or new conjectures to think about etc.

mherrmann 6y ago
> What good is a proof if literally no human being can understand it? It establishes the universal truth of a statement. So we absolutely do learn something. Until you have a proof, the statement might also be false.
- kd0amg 6y ago
  Just knowing something is true without knowing why is a lot less helpful in figuring out what else is true.
  - wisnesky 6y ago
    You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineering. For example, when a browser establishes a secure session with an encryption protocol, the reason it is secure has to do with the difficulty of finding a proof that eg certain numbers factor, but no human cares about this proof. As another example, a compiler can use a proof that a program is type correct to optimize it, but humans would not find such proofs interesting at all.
    - sukilot 6y ago
      That's great, but not relevant to mathematicians doing their jobs.
      - whatshisface 6y ago
        Knowing which conjectures were true would probably help mathematicians work more efficiently. At the very least nobody would spend time searching for counterexamples to true conjectures.
  - zxcmx 6y ago
    Existence proofs remain popular however, as do establishing upper or lower bounds.
ur-whale 6y ago
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.

mherrmann 6y ago

> What good is a proof if literally no human being can understand it? It establishes the universal truth of a statement. So we absolutely do learn something. Until you have a proof, the statement might also be false.

kd0amg 6y ago
Just knowing something is true without knowing why is a lot less helpful in figuring out what else is true.
- wisnesky 6y ago
  You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineering. For example, when a browser establishes a secure session with an encryption protocol, the reason it is secure has to do with the difficulty of finding a proof that eg certain numbers factor, but no human cares about this proof. As another example, a compiler can use a proof that a program is type correct to optimize it, but humans would not find such proofs interesting at all.
  - sukilot 6y ago
    That's great, but not relevant to mathematicians doing their jobs.
    - whatshisface 6y ago
      Knowing which conjectures were true would probably help mathematicians work more efficiently. At the very least nobody would spend time searching for counterexamples to true conjectures.
- zxcmx 6y ago
  Existence proofs remain popular however, as do establishing upper or lower bounds.

ur-whale 6y ago

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.