Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results.

As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.

▲

auggierose an hour ago | parent | next [-]

The Lean proof is published, you can download it. The clock definitely is ticking.

Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.

▲

adastra22 32 minutes ago | parent | next [-]

Publish in academic language means accepted peer-reviewed paper.

	▲	auggierose a few seconds ago \| parent [-]
		Accepted by whom? Peer-reviewed by whom? I guess these little questions are what this article is really about.

▲

raegis 35 minutes ago | parent | prev [-]

If I recall (too lazy to check) folks made slight improvements to Perelman's work and published it in mainstream journals, satisfying the "qualifying outlet" requirement.

▲

baby an hour ago | parent | prev [-]

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

	▲	seanhunter 24 minutes ago \| parent \| next [-]
		You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/
	▲	rramadass an hour ago \| parent \| prev [-]
		If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic. Humans need to verify everything.