Rendered at 19:16:52 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
sdenton4 1 days ago [-]
Feels like we need a new truth-state for mathematics: "Verified-but-Unproven" for results which we know to be true through formal verification, but without any coherent proof.
I would generally expect this state to resolve quickly to "Proven and Verified" (the tendency in mathematics historically has been for complicated first-proofs of results, followed by significant reductions in proof complexity as new tools and definitions become available), but may still be useful for assigning real credit to who/whatever produces reasonable proof for a brute-force-verified result.
bemtevi 21 hours ago [-]
> I would generally expect this state to resolve quickly to "Proven and Verified" (the tendency in mathematics historically has been for complicated first-proofs of results, followed by significant reductions in proof complexity as new tools and definitions become available),
A bit of an oversimplification, I think. Definitely there are some simplifications, but I wouldn't say really significant to the point where "resolve quickly" follows, along the lines of what you said.
Most complicated math is still nearly as complicated as when it was invented. Simplifications to presentation maybe, and some reduction in the proof difficulty yes, but not to the point of being significant in the way you describe. Any modern result that has been around for 20 years likely hasn't undergone a serious simplification, for example.
jerf 16 hours ago [-]
Last I checked (a few weeks ago, but things have been moving faster lately), the four-color theorem remains "computer proved". There has been work done on it since the original proof that has successfully simplified it, in the sense that those proofs involve less grinding through cases than the original. But it still involves grinding through more cases than can be sensibly labelled a "human comprehensible" proof, with some sort of insight into the problem space. It's still just a big set of cases being checked, and a useful final result, but no insight given in the proof.
This seems like an interesting test case to build up for AI models.
cadamsdotcom 24 hours ago [-]
Sounds like a 2x2 matrix.
aaron695 6 hours ago [-]
[dead]
vishna 1 days ago [-]
This is OpenAI’s etc version of getting unpaid internships from phd students
sebzim4500 20 hours ago [-]
How does any of this benefit OpenAI? They already got the headlines, it's not like its going to be front page news when the mathematical community actually understands the results that have already been claimed.
reasonableklout 18 hours ago [-]
I think the argument is that OpenAI should have done the work of cleaning up the proofs in the first place before dumping them onto the math community (or worked with mathematicians to guide the research process). It's as if an energy company dumped 20 tons of waste next to a village and the townspeople decided to clean it up. "How does this benefit the energy company" might not be the right question to be asking.
schiffern 6 hours ago [-]
>I think the argument is that OpenAI should have done the work of cleaning up the proofs in the first place
So the complaint is, OpenAI didn't replace the role of human mathematicians.... enough?
If this gets 'fixed,' I highly doubt the math community would be any happier.
simianwords 3 hours ago [-]
The complaint is that OpenAI is taking the job out of mathematicians. But obviously this doesn't sound that appealing of an argument so you get people piling on complaints like "this is slop and we have to clean it up". When in reality, the fact that they have anything to do at all is a privilege haha
howunfortunate 15 hours ago [-]
I'm struggling with the right analogy but the "waste" is more like...idk, hundreds of those giant crates they go through on antique shows.
The contents are actually extremely valuable, it's better to have them then not, but it still takes nontrivial expert work to sort and parse them.
simianwords 16 hours ago [-]
this is a strange analogy. no one is forcing the math community to read this
thatsabadlook 17 hours ago [-]
Uh the ultimate training data... Turning their slop into human accessible anything even if proven wrong is training data they should be paying tens of millions of dollars for.
sebzim4500 8 hours ago [-]
Maybe, but I don't see why it would be better than selecting random maths papers
thatsabadlook 4 hours ago [-]
Because it corrects the model output using model input
sebzim4500 4 hours ago [-]
If that's the goal then they can do it the other way round.
1. Pick random high quality maths papers that are outside of the training window
2. Convert them into a form which preserves the quality of the results but throws away the quality of the writing. For example, formalise them or keep only a high level summary of the proofs and throw away the introduction/conclusion
3. Generate full maths papers out of these summaries
4. Try to make the output maths papers be as similar as possible to the input papers.
You can see this as similar to training an auto-encoder, and I don't see any real downside to doing this over training on these corrected papers. Yes, the individual results would be less significant but you can't exactly mass produce training data by publishing papers and hoping someone fixes it.
curt15 22 hours ago [-]
The announcement doesn't say that the work will be using openai tools. If anything, the events over the past two months provide strong incentive to boost the capabilities of open-weight, local models.
1293475 1 days ago [-]
The authors are all in computational mathematics and AI. This is the soft power version of the OpenAI repo to get people to work for free. Maybe call it OpenOpenAI.
turzmo 1 days ago [-]
If mathematicians didn't enjoy digging their own graves with formalization before, perhaps they will enjoy digging their own unmarked, mass graves now?
pixl97 1 days ago [-]
We should burn the excavators and dig holes with our hands.
unknownian 17 hours ago [-]
“We should give the password for our university laptops running LaTeX to the robots and go sit at home.”
program_whiz 3 hours ago [-]
How about everyone just ignore this completely until OAI meets publication standards? Having a bunch of people reading and revising these proofs is just going to be used to train the AI to further displace mathematicians. Collective action problem, but just saying "these proofs are indiscernable and won't be accepted" should be permitted.
A human mathematician that turned in this kind of unreadable detritus wouldn't get published, and they would be laughed away.
This is just getting unpaid volunteers to wade through the AI slop, and refine / correct it for them (assuming there are no major errors).
dreijs 17 hours ago [-]
I have not been following recent developments, but does anyone know what the general sentiment among mathematicians is about these proofs: does it look like they hold up?
I know that at least two of the problems, the Unique Games Conjecture and Barnette's Conjecture, were very significant. It's probably too early to tell, but is there a feeling that these are now solved, or not?
QuesnayJr 15 hours ago [-]
The two most signficant number theory ones are considered solved: Quasi-Riemann and no Landau-Siegal zeros. Quanta has an article (https://www.quantamagazine.org/ai-proved-the-quasi-riemann-h...) reporting that experts agree that the Quasi-Riemann Hypothesis has been proven. The "no Landau-Siegal zeros" proof already has several manuscripts giving expositions of the proof.
I personally would never participate in this. I think clarifying proofs generated by a machine is a contemptible way to spend time. A lot of people will ask, isn't the purpose of math to generate results? I don't think so. I think the purpose of math is to gain a precise and clear understanding of the world through a shared human practice of math - human only.
I know most people here will disagree because most people here are at the top of the consumption food chain of just consuming the latest and greatest of whatever the world produces, so why not have more to consume? But slowly the joy is being sucked out of the world by AI for those not at the top and being replaced the narcissistic activity of enjoying superficial sensory stimulation in a vacuum.
A rather sad state of affairs...
_vertigo 12 hours ago [-]
Leaving your “math is for humans” take alone, if the purpose of math is to “gain a precise and clear understanding of the world”, why is clarifying results a contemptible way to spend time?
coderenegade 19 hours ago [-]
But pure math is a game that only cares about the rules and definitions as you choose to define them. It's not about understanding the world at all. The application of math in science (which is about understanding the world) is usually (but admittedly not always) after the fact.
ziiinq 20 hours ago [-]
[dead]
17 hours ago [-]
pred_ 13 hours ago [-]
How about instead, we reject the premise that OpenAI should get away with being lazy and incompetent by dumping a bunch of slop and letting researchers do all the work for free, while they still get credit?
If they want to pretend that they can do maths, they should do maths.
lukax 1 days ago [-]
And now they can train on everything this community does. And with new models this community won't be needed anymore.
nostrebored 1 days ago [-]
right, and this would be a positive for the world.
clircle 1 days ago [-]
It might be a positive. It might not be. Better to have some humility about the situation.
greyw 24 hours ago [-]
There are always people left behind by technological changes. Better move forward than cling to the past.
reasonableklout 18 hours ago [-]
Or we can show some compassion, and work towards a society that both benefits from technology and doesn't discard people at a moment's notice.
greyw 9 hours ago [-]
I feel for these people, certainly. There is no point lying to them though. We cant tell them everything is going to be alright just going to be how it used to be. That would be highly deceptive and immoral.
weknowbetter 23 hours ago [-]
Is your implication that progress is always generally positive for the average person?
greyw 23 hours ago [-]
My implication is that being left behind is worse than other choices.
fergonco 1 days ago [-]
For a world. A world some people will not be part of.
boothby 20 hours ago [-]
We’ve seen time and time again that "a positive for the world" is not something these companies align on
qwr186 1 days ago [-]
Yes, only Nvidia should exist. r/accelerate nutcase?
I would generally expect this state to resolve quickly to "Proven and Verified" (the tendency in mathematics historically has been for complicated first-proofs of results, followed by significant reductions in proof complexity as new tools and definitions become available), but may still be useful for assigning real credit to who/whatever produces reasonable proof for a brute-force-verified result.
A bit of an oversimplification, I think. Definitely there are some simplifications, but I wouldn't say really significant to the point where "resolve quickly" follows, along the lines of what you said.
Most complicated math is still nearly as complicated as when it was invented. Simplifications to presentation maybe, and some reduction in the proof difficulty yes, but not to the point of being significant in the way you describe. Any modern result that has been around for 20 years likely hasn't undergone a serious simplification, for example.
This seems like an interesting test case to build up for AI models.
If this gets 'fixed,' I highly doubt the math community would be any happier.
The contents are actually extremely valuable, it's better to have them then not, but it still takes nontrivial expert work to sort and parse them.
1. Pick random high quality maths papers that are outside of the training window 2. Convert them into a form which preserves the quality of the results but throws away the quality of the writing. For example, formalise them or keep only a high level summary of the proofs and throw away the introduction/conclusion 3. Generate full maths papers out of these summaries 4. Try to make the output maths papers be as similar as possible to the input papers.
You can see this as similar to training an auto-encoder, and I don't see any real downside to doing this over training on these corrected papers. Yes, the individual results would be less significant but you can't exactly mass produce training data by publishing papers and hoping someone fixes it.
A human mathematician that turned in this kind of unreadable detritus wouldn't get published, and they would be laughed away.
This is just getting unpaid volunteers to wade through the AI slop, and refine / correct it for them (assuming there are no major errors).
I know that at least two of the problems, the Unique Games Conjecture and Barnette's Conjecture, were very significant. It's probably too early to tell, but is there a feeling that these are now solved, or not?
I know most people here will disagree because most people here are at the top of the consumption food chain of just consuming the latest and greatest of whatever the world produces, so why not have more to consume? But slowly the joy is being sucked out of the world by AI for those not at the top and being replaced the narcissistic activity of enjoying superficial sensory stimulation in a vacuum.
A rather sad state of affairs...
If they want to pretend that they can do maths, they should do maths.