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.
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.
If mathematicians didn't enjoy digging their own graves with formalization before, perhaps they will enjoy digging their own unmarked, mass graves now?
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.
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.
Sounds like a 2x2 matrix.
This is OpenAI’s etc version of getting unpaid internships from phd students
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.
If mathematicians didn't enjoy digging their own graves with formalization before, perhaps they will enjoy digging their own unmarked, mass graves now?
We should burn the excavators and dig holes with our hands.
This experiment might be relevant: https://github.com/offline-ant/wiggums-proof-loop
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.
Have we ruled out Trisolarian involvement? IYKYK
And now they can train on everything this community does. And with new models this community won't be needed anymore.
right, and this would be a positive for the world.
It might be a positive. It might not be. Better to have some humility about the situation.
There are always people left behind by technological changes. Better move forward than cling to the past.
Is your implication that progress is always generally positive for the average person?
My implication is that being left behind is worse than other choices.
For a world. A world some people will not be part of.
Yes, only Nvidia should exist. r/accelerate nutcase?