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.

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

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.

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.

> arrival of a machine that helps me dig faster

This is usually wrong for the current SotA of ITPs.

One important difference between verified programs (that the article mentions is useful) and mathematical results is that the former usually involves properties that are very complicated to state with many moving parts, but are usually straightforward to prove. On the other hand, mathematical results usually have a straightforward central concept, and the complicated details (if there are) can be altered to slightly change the result.

To the mathematician, these complicated details are understood to be nonessential to the result and can be omitted, or reduced to a a comment or reference. And if the theorem is wrong, it can usually be salvaged.

But with provers, you are forced to get bogged down in the details.

The analogy to mining machines is wrong; the appropriate comparison is something more like writing in Python vs. writing in assembly. Writing in assembly you have a better guarantee that the computer is behaving exactly as you told it to.

But it's less portable (e.g. you must decide to encode tuples primarily as a product, or as a finite sequence, one of many nonessential decisions that are important to a prover), just as asm is less portable than a python program. You have to get bogged down in details that you can make errors in that you don't in Python; (respectively, informal proof). It's harder for peers to understand the thrust of what is happening. etc.

Imagine that careful examination of the mineshaft helps determine where the most profitable place to dig next might be... And then imagine a machine that only produced mine shafts that tell you nothing.

Sometimes the machine might be very useful! It would allow scaling up solutions for downstream users. For example, if you have more people who want solutions to many slightly-different complicated integrals that we don't have a good overarching theory to solve.

But in other cases, knowing /where/ to dig is much more important than how fast you dig.

Suppose there was a machine that was a black box where you could ask it whether a result was true or false, and it spit out a truth certificate that was not humanly understandable, but it could be mechanically verified.

I would find this incredibly disappointing. The appeal of mathematics is not just that I know things are true -- I know why they're true. I know why x + y = y + x, why there are infinitely many primes, why the derivative of x^2 is 2*x. Working out a proof isn't tedium -- it's the point.

I have no idea why you would find the existence of this machine disappointing. If you wanted to work out something for yourself then you still can.

What you say my be true in your corner of the world. I'm going to go on a limb and say you've not done or used much applied math in your work.

For the rest of humanity, those who build things using maths and have deadlines to meet to deliver working thins, knowing something is true for sure has incredible utility.

Understanding why it is true is most certainly nice, but it's just the icing on the cake: they have bigger fishes to fry.

Please keep personal swipes out of your comments here. They're against the rules (https://news.ycombinator.com/newsguidelines.html). We've had to ask you this before.

I'm actually an applied mathematician, so no.

You don't want to understand things? You don't care at all? All that matters to you is making that better widget? Meet that deadline?

I think having a tool but not being able to know how it works can be both amazing and frustrating at the same time (depending on the perspective of someone using the tool vs someone wanting to make the tool better).

Both perspectives are equally valid.

As a concrete example, suppose an alien cube suddenly appeared on Earth that, with a push of a button, would emit a pill.

It was discovered that the pill could cure half (but only half) of all known forms of cancer.

However, no matter how hard anyone tried, it was impossible to understand how the cube or the pill it created worked.

For those with cancer that took the pill and were cured, the cube was an amazing magical device.

For the people that took the pill and it didn't help them, the cube was worthless, since doctors couldn't tell them anything about why it didn't work, or what they could do to make it work.

For researchers it was frustrating because the cube showed some cancers are curable, but gave no reason why.

For the cancers it did cure, they didn't know why, and for those it didn't cure they also didn't know why.

Further it gave no insight into why only half were curable.

Was it because the cube was imperfect, or was that really the best that could be achieved?

For all intents and purposes, cancer research and treatment didn't really change. If you had cancer, you tried the magic pill. If it worked great. If it didn't, then doctor's were back to traditional techniques.

Thus from a knowledge perspective of one day curing all cancer, the cube didn't help, because the knowledge of how it worked couldn't be expanded to cure all cancer.

For someone cured by the cube, it was an amazing device, and nothing could change their mind.

For a cancer researcher, the cube was useless, and the only thing that could change their mind was if its mechanisms could be understood.

It is similar for math. As a tool, it is good enough to just know that the theorem is valid.

However, if you want to expand on that tool, develop more tools, or create different ways of looking at the problem, you need to understand why the theorem is true.

Your need for utility will mostly likely be met by a symbolic algebra system not a formal reasoning system.

If you were a miner, that tool that helps you dig faster would put you out of a job, because now they only need half the miners to do the same amount of work.

If you were an artist, a lot of the point is the material things, or the process. Why on earth use oil paint than instead of Photoshop or other digital tools? Why do people use paper at all? It's so inefficient. But art really is personal and inefficient most of the time.

It's a bit more complicated, and the facile 'luddite' retort doesn't help.

Humans need something to do. In times immemorial, something to do entails running around the savanna looking for edible scraps, collecting them, bringing them home and raising the next generation to repeat the process. A perfect machine that produces and delivers edible scraps with zero human effort required leaves actual humans with nothing to do. Having nothing to do is spiritually unsustainable. There is so much leisure or travel. There is so much make-believe work. After a while though, people will need something meaningful to do, something that undeniably pushes the inexorable wall of unbeing a bit further.

This is exacerbated by social effects. We confer value to other people by their ability to provide meaningful work. Assuming a perfect machine that does all the meaningful work, there is zero reason to confer value to any other human being. This is a recipe for disaster, and will hit us much sooner than the angst of nothing to do.