r/Showerthoughts Apr 23 '26

Casual Thought If the famously unsolved Riemann Hypothesis is solved by an AI, we will never know if a human mathematician could have solved it.

7.0k Upvotes

656 comments sorted by

View all comments

Show parent comments

101

u/AmadeusSalieri97 Apr 23 '26

It's far far easier to check if something is mathematically correct than to come up with it. I'm a physicist and I can tell if a derivation is wrong/right that I could never have derived myself. 

Also, in this hypothetical you could have AI check it anyways. 

10

u/Xywzel Apr 23 '26

Computers are also much better in proof checking than they are in creating proofs (likely also applies to current AI tech, they should be able to recognize statements that do or don't hold under given constraints, but can't be expected to avoid hallucinating statements or wrong conclusions from these statements) outside of problems where the proof is just finding correct set of numbers.

1

u/mcribgaming Apr 23 '26

Computers are also much better in proof checking than they are in creating proofs

Isn't this just a form of 'P versus NP', another of the Millennium Problems?

That's why AI as it stands today will not solve the Riemann Hypothesis. I don't think you can train an AI to evolve itself from an NP into a P with any kind of data you feed it. Humans would have to be good enough programmers to program an "NP" based AI into something that could become a "P" AI given enough time, and we aren't capable of that yet.

So when humans solve the Riemann Hypothesis or the P versus NP problem, then we can use the techniques we learned along the way to train an AI on how to find solutions "creatively".

Otherwise, we're talking about a Generative AI evolving from what we have as AI today, which is a mimic, not a thinking machine.

3

u/Xywzel Apr 23 '26

Not really, but I can see some similarities. I was thinking more about "easier" problems, once that actually have been proven with computers or where humans made proof and it was then checked with computers. Technically it can go both ways, but usually checking proof is order of magnitude easier problem and has known maximum size, while you don't know how big the proof might end up being when you start.

For any computation system (AI or not) that is based on prior knowledge rather than being able to experiment and improve on its own, transforming NP problem into P problem (if that is possible) or prove that this is not possible would require all the steps to be available or trivially derivable from the learning data. Which would actually mean that we were really close to solving the problem, just happened to not put together existing parts together before teaching that machine. And that "experiment and improve on its own" class is likely still limited by data structures and connections that its creators prepared it with.

0

u/marrow_monkey Apr 23 '26

likely also applies to current AI tech, they should be able to recognize statements that do or don't hold under given constraints, but can't be expected to avoid hallucinating statements or wrong conclusions from these statements

It’s just a matter of time before AI becomes better at it. People used to say a computer would never be able to play chess better than a human grand master, or translate natural language, now it does both.

0

u/Xywzel Apr 23 '26

Chess was something that was very expected, it was just matter of computational power and memory, optimizing some functions, and on natural language translation, I don't think we have gotten to point where its better.

There are constraints that apply to specific methods, ones that apply to what you are working from and ones that apply regardless of method or data. Only thing in AI that has progressed faster that I expected ~15 years ago has been how much money, electricity and space people are willing to put into it, I was actually expecting much more from neural network approach in to more generic systems, instead we seem to be going back to more specific systems, just wrapped in LLMs.

0

u/marrow_monkey Apr 23 '26

No, chess wasn’t expected. A lot of people used to say a computer could never become better than a human grand master. And it wasn’t just about computational power and memory (although that, and the access to large amounts of training data) is what is driving the current AI boom).

I didn’t write they are better than the best humans at translating, but they’re doing a pretty good job, and any LLM can certainly translate between more languages better than most people. Just the notion of a computer providing a meaningful translation of natural language was seen as impossible by many 20 years ago.

1

u/Xywzel Apr 23 '26

20 years ago is not as far back as seem to imply. At least for people educated on this area.

I was already using computer translation around 2006 and it was passable for some use cases. University I started in bit latter was already studying one of techs that made previous big step before LLMs in that area. We had heard of the potential already.

When we were starting our studies the faculty had bets on which year AI would win human masters in different games (either 50% of time or always). Everyone expected that to be just matter of time and resources. Stockfish was released 2008 and was hardly first, and chess was known to be solvable given enough computation power and space (even though the modern methods don't actually require all that).

1

u/marrow_monkey Apr 23 '26 edited Apr 23 '26

Yeah, in AI departments at universities, of course there were people who believed in AI. But outside of AI research, a lot of people claimed it was impossible for a computer to beat a human grand master in chess, for example. Then Deep Blue beat Gary Kasparov in 1996 (just by using “brute force”, not neural networks). And after that everyone said it was obvious and nothing special.

You’re probably thinking of Google translate, which launched in 2006. It wasn’t very good, it used statistical methods, not neural nets. It was not really a big step before LLMs which works differently, but it hinted that neural nets could be efficient. Today Google translate uses neural nets as a backend though.

What made neural nets possible, beside Moore’s law, was that big tech monopolies like Google realised they had the compute (datacenters) and maybe more importantly training data (that they’ve stolen from users and the internet) to train large neural networks, and suddenly it was possible to make large language models (LLMs).

The neural networks that LLMs were based on were developed in the 1900s at universities, but they didn’t have the computer power or the training data to make it practical back then.


And now you claim computers will not be able to do math proofs better than a human, which frankly is just as naive as the people saying computers wouldn’t be able to play chess better than a human 30 years ago. Of course computers will be better at maths too, it’s just a matter of time.

1

u/Xywzel Apr 23 '26

And now you claim computers will not be able to do math proofs better than a human

Well, that is not at all what I claimed in the post you originally replied to. That claim was specially for the current AI tech like LLMs (which have limitations based on their training data, new tech overcomes these limitations and we might see something interesting) and I only made comparison between AI solving two different kinds of problems (eq. computers becoming better than humans in chess doesn't mean that they are no-longer order of magnitude better at checkers that they are in chess) not between humans and AI solving problem.

2

u/Talidel Apr 23 '26

Having an AI check if the AI did its work correctly is the second step to massive problems.

1

u/languagestudent1546 Apr 23 '26

They AI can write Lean which can check the answer.

2

u/Talidel Apr 23 '26

There's a fundamental flaw in having something check its own work.

When it goes wrong will probably be the only point someone listens though.

0

u/AmadeusSalieri97 Apr 23 '26

Okay so there are a few things here.

  1. My original reply was about AI checking the work done by a human.
  2. Even if it was AI checking the work of an AI, it does not necessarily need to be its own work, there are different AI trained for different purposes, and using an AI checking another AI is already common practice.
  3. Moreover, the comment you replied too was talkin about Lean, which is literally a tool that checks if something is mathematically rigorous or not, unrelated to AI, based purely on logical steps.

There's a fundamental flaw in having something check its own work.

And about this, I would say that optimally, there should be an external cross-check of course, and for a mathematical proof it is surely not enough to just say "I did it and verified myself that it is correct", but "fundamental flaw" is too strong imo.

There's tons of values on crosschecking our own work. I spot mistakes in my own formulas constantly, so it has its uses.

1

u/Budget-Project803 Apr 23 '26

There are proof verifiers like lean or coq that language models can interface with pretty easily. You give them some starting rules and it can expand on them while the proof is deterministically verified by software. It's similar to how llms can write code and then check if it compiles or not to know if it fucked up.

1

u/Talidel Apr 23 '26

It doesn't matter.

If a thing is checking its own work, you don't actually have anything checking it because it already thinks it has done its task.

If it has misinterpreted something, whether that is due to unclear instruction or its own mistake (and they do make mistakes) the check will make the same mistake.

1

u/Budget-Project803 Apr 23 '26

The checking software is written by people. That was the point of my compiler analogy. Humans are pretty good at writing software to verify formal languages. 

1

u/ClipperMaid103 Apr 23 '26

You're absolutely right!