It provided a formal proof in Lean.

Which is not the same thing that was written in informal prose & their proof has 8k non-computable axioms so you can't even write a program to verify their blowup example is actually a valid instance of a smooth flow that blows up.

> I am certain their Navier-Stokes proof is incorrect.

How much are you willing to bet on this?

Whatever you want, further scrutiny will reveal an error among the noncomputable axioms (8k of them) that were used in the proof.

here you go

https://polymarket.com/event/openai-retracts-navier-stokes-s...

https://polymarket.com/event/openai-retracts-navier-stokes-s...

i hope to hear all about your riches in 2027

Is this a joke? What amount are you betting?

are you a joke? what exactly do these words mean?

> I am certain their Navier-Stokes proof is incorrect.

i at no point said anything so stupid so i'm not betting anything.

I see, so you have no idea if the proof is correct or not & you have no clue how many non-computable axioms are in the lean certificate. Seems like I have wasted enough time here so good luck to you.

i asked you a pretty "computable" question: what exactly do these words mean?

> I am certain their Navier-Stokes proof is incorrect.

Just assume standard semantics & it should make sense.

Sorry I need you to state your axioms here because as I stated above, "standard" semantical interpretation of the word "certain" implies you should be betting lots of money. Since you're not, I have to conclude you have some goofy unorthodox semantical interpretation.

By standard semantics, if you state that believing with certainty that the proof is incorrect is stupid, then you surely believe with certainty that it's correct.

Unless you want the negate the certainty part, but then the nudge to gambling is less coherent.

> By standard semantics, if you state that believing with certainty that the proof is incorrect is stupid, then you surely believe with certainty that it's correct.

you might want to think a little bit harder on this

You're failing to apply de Morgan's laws correctly:

(X and Y) => Z

<=>

~Z => (~X or ~Y)

i think what they are saying is that if you really so certain that the proof is incorrect, you would put on that claim and rest assured that you would win. Especially since the position you are claiming is currently at less than 10%, you stand to win a large amount of money.

The person you are arguing with made no such claim of certainty either one way or the other, so they have no reason to bet anything.

I understood what they were saying but if they're not willing to bet any money then they should refrain from commenting entirely since that seems to be the bar they are setting for others.

> since that seems to be the bar they are setting for others

this is a very simple exercise in propositional logic (simple enough that i don't need to write a lean proof):

"if you are certain then you should bet"

<=>

"if you're not betting then you're not certain"

so i don't have a "bar" and i'm not saying you shouldn't comment, i'm simply calling you a liar.

this argument clearly does not make sense

It can be summed up as ‘put your money where your mouth is’.

Turnabout is fair play.

I think you misunderstood. His mouth was not at "the proof is correct". His mouth was at "you are not really certain that the proof is incorrect". Those two are not the same thing, so flipping the accusation back at him and saying "you should've bet on the proof being correct then" does not actually make any sense.

edit: in other words, if there is anything that he should bet on, it's "the other guy wasn't really certain that the proof is wrong, he is just bloviating". That's a different bet than "the proof is correct".

It's amazing how thick these dudes are <shrug>

"I am 100% sure Microsoft stock will go up 20% tomorrow!"

"i call bs. Why don't you bet your money on it then?"

"well you shouldn't be talking either, you haven't bet money on the stock going down!"

"I am 100% sure Microsoft stock will go up 20% tomorrow!"

"i call bs. Why don't you bet your money on it then?"

"well you shouldn't be talking either, you haven't bet money on the stock going down!"