The post says there's a Lean certificate for this and other proofs ("some [...] not all of them").

> This looks like an AI IPO PR powerplay,

Interestingly, the post has actually also an argument for this:

> Experience has shown that, even now, there will still be people explaining in patronizing tones why none of this is real and none of it counts. If such people were capable of being impressed by anything that happens in the empirical world, of updating on anything, they would’ve already been impressed and already updated several years ago, long before things had reached the point of an actual Mathocalypse.

> So, they’ll say, maybe the alleged solutions are not solutions at all, but just “AI slop.”

▲

smcg 2 hours ago | parent [-]

It's on OpenAI and Anthropic to prove that they obtained these results legitimately and credited all researchers who deserve credit. They do not get the benefit of the doubt.

▲

pizza234 25 minutes ago | parent | next [-]

Have you actually read the article? It's been actually written, among the other things, because the author's wife has been trying to solve one of the problems for her whole life.

▲

Kotlopou 2 hours ago | parent | prev [-]

But if you think they got them illegitimately, then how did they get them? And why are mathematicians reacting to this as a sudden explosion of new results that have resisted sustained effort? Where is the sudden productivity rise coming from?

	▲	za_creature an hour ago \| parent [-]
		I'd say it comes from the same mathematicians that were strongly encouraged to use the machine to solve their problems for the last 2 years or so. There's clear benefit in a babelfish that can coordinate disparate efforts, the only problem with the current iteration is giving credit to said efforts. Google went quite far down the road to hell, but stopped short of taking credit for websites' content since the company understood that poisoning the well only goes so far. At this point, one can safely conclude that _Chat_GPT was an intentional attempt to squeeze out more data once they mined the internet dry.