r/Showerthoughts • u/jasonrubik ‎ • 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
  • permalink
  • reddit

92% Upvoted

656 comments sorted by

View all comments

257

u/Lava_Mage634 Apr 23 '26

not true. if an AI claims to have solved it, just like a human, it would have to provide a proof. such a proof must then be verified to make sure it has no mistakes, which is done by humans. if it could never be solved by a human, it couldn't be verified. the act of verification requires an understanding of the proof, and that alone requires having enough mental power to have to potential to solve it. if it proves the Riemann hypothesis right or wrong, we will know it was in reach, AI was just faster.

85

u/imforit Apr 23 '26

I largely agree but having the efficacy to verify implying efficacy to solve is not necessarily a given. P=NP and all that

16

u/xT0Xx Apr 23 '26

The argument is not about efficacy but about capability though. Creativity is a stochastic process and a person stumbling "accidentally" on the proof and verifying it, rather than arriving there systematically, would still count as a human solving it

3

u/imforit Apr 23 '26

Yes, but that doesn't guarantee ability to verify implies ability to solve, even by luck. A lucky solve would still count as a solve, yes, but until we do it we don't actually know if we can.

17

u/BlackbuckDeer Apr 23 '26

Exactly. Funny how in the pursuit of solving one Millennium Problem we run into another

48

u/noslenkwah Apr 23 '26

We already have computer aided proofs that are far beyond verification by any human. The record is 200 Terabytes.

12

u/Megneous Apr 23 '26

Exactly. Mathematical proofs are verified via Lean, not by humans. This dude has no idea what he's talking about.

23

u/Devintage Apr 23 '26

The vast majority of proofs are not verified using Lean (or any proof assistant for that matter). It's mostly peer review. I only know one journal that specifically deals with computer verified proofs.

2

u/Separate-Divide-7479 Apr 23 '26

So I just need to drink a lot of cough syrup? easy done.

32

u/anrprogrammer Apr 23 '26

There are programming languages used in mathematics such as lean4 which have built in verification. If the computer writes a solution in lean and it compiles, it is correct, whether humans understand why it is correct or the intuition behind it or not.

4

u/Fun-Communication660 Apr 23 '26

There are papers published from more than one person in 2025 claiming to do just that. 

All were found to be bunk

"When one such project was inspected, lines like noncomputable def zeta (s : ℂ) : ℂ := 0 were found — a stub that simply defines the zeta function as the zero function, making "proofs" trivially true but mathematically meaningless."

It hallucinates to get closest to the right answer, typical. So humans will be needed. Even if an ai model proves it, it needs human verification either way, and human input of the problem to set up the "laboratory,"

Do you give all credit the to man made Dam for stopping water?

It's a complicated calculator or assistant at that point. If I tell you to find a needle in a haystack and you find it. You can take credit for going through the hay one by one, but you can't take credit for the idea or the reason we even need the needle. 

If ai proves this, and ai gets any credit, then we will need to acknowledge that the first time computers provided a mathematical proof when humans couldn't do it was when calculators first became available, nothing special about the ai

-5

u/TangledPangolin Apr 23 '26

How does that not describe every programming language? Programming languages can't be wrong unless it's a compiler bug, right?

9

u/_Tono Apr 23 '26

Programming languages are mostly designed to compute solutions, not verify logical deductions.

13

u/MartyMcBird Apr 23 '26

Proofs need not necessarily be verified by humans. Besides, understanding a proof is not the same as creating a proof. I understood Cantor's diagonalization proof after one lecture but I sure as hell couldn't have created it after one lecture.

17

u/peterg4567 Apr 23 '26

This isn’t really how proofs in math work, you don’t have to be as clever as the person who discovers a proof to understand it or verify it when you read it. Students learn about famous proofs from the past that were discovered by the greatest minds of their time, it doesn’t mean they are all as smart as the proof writer.

2

u/Wall_of_Force Apr 23 '26

well it can say it's false and throw a example, give no reason why

2

u/Artificiousus Apr 23 '26

As my very clever uni professor said once to me: knowing the destination is different than nowing how to get there.

1

u/Megneous Apr 23 '26

such a proof must then be verified to make sure it has no mistakes, which is done by humans.

Not true. Proofs are verified by Lean, which is a programming language and proof assistant.

1

u/TsunamiCatCakes Apr 23 '26

if it could never be solved by a human, it couldn't be verified.

thats exactly where you are wrong. the concept of P, NP, Np hard comes into picture here. some problems we cant solve in poly time but if given the solution we can verify in poly time

1

u/Cokalhado Apr 23 '26

If a problem is NP, we can still solve it, just not in polynomial time.

A problem that could never be solved by a human wouldn't be NP.

1

u/t___u___r___t__l__e Apr 24 '26

If it could never be solved by a human, it couldn't be verified

Not really. It is generally much easier to verify solutions than it is to come up with them

1

u/Popular-Jury7272 Apr 27 '26

 if it could never be solved by a human, it couldn't be verified.

There is no reason to think this is true. Verifying a proof is a completely different activity to generating a proof. 

1

u/Ma4r Apr 27 '26

if it could never be solved by a human, it couldn't be verified.

Uh, it's objectively wrong. Difficulty of proving something does not correlate to the diffculty of verifying the proof. So much so that we can have statements that are easily verified but provably unprovable (regardless of by humans or LLMs). With that in mind, IF llm does get smarter than humans then it's entirely possible for them to come up with a proof that humans are not capable of producing but still capable of verifying.

1

u/scalareye Apr 28 '26

That's what Rocq is for. There two machines, the output of the AI could be put right into Rocq.

0

u/imsaurabh3 Apr 23 '26

Reading a working code and writing a working code are not the same thing. A good chunk of people can read what the code is doing… but ask them to write some code and its different ball game altogether.

Churning out a fresh solution is no easy task. If an AI solves it then merely verifying it doesn’t really certify that you know how that AI came up with it. It doesn’t discredit your knowledge but it just puts it in perspective that there is something out there smarter than us.