AI Proved the Quasi-Riemann Hypothesis. What Happens Now? | Hacker News Reader

AI Proved the Quasi-Riemann Hypothesis. What Happens Now?

quantamagazine.org

48 pointsibobev14 comments

It might have proved it, but the higher level of understanding which was expected from the process is not there, so there is no benefit.

Third paragraph from the end of TFA:

Mathematicians are both frustrated and excited by OpenAI’s work. Sarnak, for his part, said in an email that he won’t be satisfied that it’s “a Theorem” until humans check and understand all the details. But “the general feeling is one of relief,” Radziwiłł said. There are scores of results across not just number theory but also geometry and theoretical computer science that the proofs of quasi-Riemann will, in a swift stroke, establish as mathematical truths.

Is that a requirement though? If the AI used existing understanding/methods (which I assume it did) then there's nothing really "new" there, right? Shouldn't it be possible to get understanding from how the existing methods were used? Or, even knowing it's true, cull an incredible number of paths from the problem space around it, to make finding understanding easier?

I'm not a mathematician, but I've always been able to find understandings from exploring the paths starting from either direction of the conceptual graph that exists between a "problem" and a "solution".

Not to any great extent.

It’s the equivalent of unrolling a loop into a series of individual linear statements. You’ll never derive monadic forms from that. It requires a far greater intelligence to think that up. As nature can’t speak our language, we have to rely on the stupidity of humans instead to help discover its beauty. So we are stuck with mathematicians.

People, mathematicians, of course care about answers. But they deeply care about how those answers were derived and they’ll duel if they find a given thing looks ugly. People have invented entire fields because shit didn’t look right or left gaps in reasoning or understanding. Take quaternions. Take calculus.

AIs aren’t super intelligent and these grifters and charlatans need to be laughed out of the room.

It is unfortunate to see what happened to terry tao but not at all surprising. He endorsed the snake early on thinking the snake was a friend. It was only a question of time before it would turn on him to bite him.

What is the reason that we won't eventually be able to ask AI to simplify the lean proof, or make it more readable to humans? Or to read the swarm communication logs and summarize the process by which they arrived at the solution?

I don't understand why there seems to be a fundamental limitation on that front.

There's no reason to think the LLM can't be prompted to improve its presentation. Still, can one internalize math simply by reading solution manuals?

Yes? Isn't that what humans do when teaching each other math? I don't see why, however any human prefers to teach/learn math, LLMs can't do that too.

I think the point of the "solution manuals" reference is that you have to do math to learn it, not just read the solution that someone else has written.

Would knowing that it's true cull an incredible number of paths? Well, it's either true or it's false. So imagine setting half of the world's mathematicians on proving "true" and the other half on proving "false". Being told in advance by an oracle that "true" is the right answer at best doubles the number of mathematicians you can deploy on making an understandable proof.

There's a joke telling what purportedly happened after the famously abrasive physicist Wolfgang Pauli died and went to heaven. Pauli supposedly got to meet God, and asked God why the fine structure constant had the value 1/137.08 or whatever it is. God said "good question!" and started covering a blackboard with equations. Pauli marveled at the mathematical elegance, said "that's wonderful", etc. until God got to a certain point in the calculation, where Pauli said "that's wrong!!!".

We want explanations, not just answers like 1/137.08.

The benefit is in:

> Mathematicians have been studying the paper intensely in the couple of weeks since its release. Peter Sarnak, a prominent number theorist at Princeton University, has decided to repurpose a course he’s teaching this semester to study it. Radziwiłł says he can now sketch the proof’s arguments in half a page, while more involved write-ups by other mathematicians range from seven to 13 pages. (As of this writing, these have not yet been published, but are circulating privately.)

7/8 result is already Lean-verified, yet experts are spending their time on the unverified 11/12 paper because it’s shorter and the only one a human edited

The fact that a piece of software compiles does not necessarily mean that it is correct. The same applies to Lean; in fact, some type theorists are not particularly satisfied with the current state of Lean or the direction in which it is heading.

Mathematician, but not my area. I'd do the same.

Probably the 7/8 has more tricks and special cases to get the better bound. Also, to make the English version close to the Lean version it probably expands some details. So it's longer.

The idea is to understand the 11/12 version, add a few intermediate steps, and get an intuitive understanding of it. Then in a second step go for the 7/8 paper, hopping it's an extension of the 11/12 paper.

Then try to guess 5/6, perhaps as centaur math...

I kinda hate the hard statement that AI "proved" something, when no expert human actually had a chance to look and digest properly the so-called "proof". IMO this whole proof-dump looks like a publicity stunt; just imagine that you have access to a very potent tool, and you strongly believe that it is capable of tackling problems of QRH level, why would you dump hundreds of hard proofs targeted at different areas, rather than focusing on a couple of problems, verifying the bits on the go with experts? It is almost like a company that was caught doing loud yet somewhat empty statements previously, once again is trying to hit the biggest PR coverage rather than trying to cooperate with mathematicians to actually solve those problems.

Reply on news.ycombinator.com