That AI companies are pouring huge resources into strip mining outstanding problems for bragging rights rather than introducing the technology responsibly in a way that benefits the field.

Somebody will now respond that it doesn't matter that it doesn't benefit the field if it can produce the product without the mathematicians, but the whole point is that an LLM-generated Lean proof isn't the product. The proof of a singularity in Navier-Stokes is of zero commercial value (except bragging rights) in itself. If it ever results in something of commercial value it will be far downstream, after any new, valuable ideas in it have been digested, explored, explained, etc. This is work for mathematicians that LLMs cannot (currently) do.

And next someone will respond that LLMs will be able to do that work, however that is a prediction that is yet to come about. It might happen, it might not. To tear down something valuable now on the assumption that it will become obsolete in the future is wildly irresponsible.

▲

fragmede a day ago | parent [-]

I think a million dollars has commercial value, but maybe that's just me.

	▲	nicf a day ago \| parent \| next [-]
		By all accounts this result cost far more than a million dollars to produce, and either way OpenAI announced they won't be accepting the prize.
	▲	omnicognate a day ago \| parent \| prev [-]
		Missing the point by the widest conceivable margin. The million dollars is an award from the Clay Institute. It doesn't represent value in the proof itself, but rather is offered as a reward for an activity that, when done the human way, is expected to result in valuable ideas. As the Clay Institute says on their website, on the Navier-Stokes page: > Why ask for a proof? Because a proof gives not only certitude, but also understanding. It's also a fraction of the amount OpenAI invested in generating the proof, and its value to them is dwarfed by that of "bragging rights".