Hacker News Reader

Comment by ironSkillet | Hacker News Reader

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.

View on HN

> 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.

Just knowing something is true without knowing why is a lot less helpful in figuring out what else is true.

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.

That's great, but not relevant to mathematicians doing their jobs.

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.

Existence proofs remain popular however, as do establishing upper or lower bounds.

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

[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.

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.

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.

Reply on news.ycombinator.com