On: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

[scuppernong]

this is not a rumor (the allegation, anyway), it's reported in the new york times

[jcranmer → scuppernong]

Newspapers are not above printing rumors.

See, e.g., Barak Ravid regularly reporting in Axios the impending ceasefire negotiation progress in the Iran War, which largely have failed to come to pass.