Comment by whack | Hacker News Reader

Comment by whack | Hacker News Reader

The core thesis seems to be that the "real value" is not in producing/proving theorems, but in understanding them. AI might be good at producing and proving theorems, but it fails utterly at getting humans to understand them. Even worse, humans have no interest in working on theorems that have already been proven, so we end up with theorems that will never be understood by humans.

I can understand why this is a major concern for mathematicians. They got into their field because they love the beauty of mathematics, and the intellectual satisfaction of understanding non-obvious insights. But to put it crudely, this sounds like a you problem. As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology. And their practical applications in human life. I have zero understanding of the math behind cryptography, but I still deeply appreciate the practical value they have provided humanity.

If AI systems start churning out accurate theorem-proofs, and we are able to use those theorems to build things that improve human quality of life, it doesn't bother me one bit that those theorems have not been understood by humans. If this offends your aesthetics, you are certainly entitled to your opinion and your preferences, but that does not make it a societal problem

They got into their field because they love the beauty of mathematics… As someone who isn't a mathematician, the main value I get out of math is its practical applications in science and technology

I have some sad news for you. 99% of the work mathematicians do has no immediate application, nor even an obvious path toward application in the near future. You mentioned cryptography, so for an example consider number theory: no apparent practical applications, going back thousands of years to the time of Euclid and earlier.

It’s been religion, philosophy, and recreation that have provided the motivations to study mathematics all these years, not applications. Applications have almost always followed long after the development of the pure mathematical theory. For number theory, that was the development of cryptography during WW2, millennia after the ancients laid those foundations.

Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.

> Most unfortunately, it’s the truth value and the understanding which drive applications of mathematics, not the proof work itself. If the AI revolution decapitates the institution of mathematics which produces the understanding, and is unable to replace it, then the applications will cease as well.

In a world with no AI, it is vital for humans to understand math, in order to derive practical applications. But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.

But in a world where AI is able to both produce math theorems, and figure out practical applications for them, human understanding has minimal practical value to society.

We have examples of AI producing theorems but there is no evidence that AI will be able to find all of the practical applications of mathematics, at least not any time soon.

As I understand it, most of the theorem proving work done by AI today consists entirely of “glue code” style work: combining a bunch of different known results to prove a new result. This is great for those who desire completeness in the mathematical project but it’s often outside the areas of interest for mathematicians who are pursuing “big idea” problems whose solutions likely require development of entire new branches of mathematics. One famous example of such was Fermat’s Last Theorem.

It is like an idiot savant, just really widely read enough to seem creative when it tries some obscure thing. see First Proof though if you haven’t.

More divergent type than convergent like ramanujan.

Then you have to make sure that the AIs understand the theorems (sort of build a "world" for that - otherwise how'd there be confidence in the use of said theorems?

If cryptography didn't exist but the maths did, how'd you use it?

Reply on news.ycombinator.com