Oai-math-revised: a community hub for revising OpenAI's math write-ups

vishna

This is OpenAI’s etc version of getting unpaid internships from phd students

1293475

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

If mathematicians didn't enjoy digging their own graves with formalization before, perhaps they will enjoy digging their own unmarked, mass graves now?

sdenton4

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.

lukax

And now they can train on everything this community does. And with new models this community won't be needed anymore.

athrowaway3z

This experiment might be relevant: https://github.com/offline-ant/wiggums-proof-loop

GoWaitInTheVan

Have we ruled out Trisolarian involvement? IYKYK

bemtevi

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...

dreijs

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?

pred_

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.