Rendered at 04:36:34 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
matt3210 1 days ago [-]
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.
nomel 1 days ago [-]
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".
throwaway81523 7 hours ago [-]
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.
benoq 1 days ago [-]
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.
cman1444 20 hours ago [-]
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.
curt15 18 hours ago [-]
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?
cman1444 17 hours ago [-]
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.
gus_massa 6 hours ago [-]
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.)
T-A 1 days ago [-]
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.
mrkn1 1 days ago [-]
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
gus_massa 4 hours ago [-]
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...
rafaelRiv 1 days ago [-]
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.
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".
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.
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.
I don't understand why there seems to be a fundamental limitation on that front.
> 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.)
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.
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...