Remix.run Logo
an0malous 2 hours ago

It sounds like he hasn't verified the results of a problem that he has personally worked on, so how many of these problems have actually been verified?

margorczynski an hour ago | parent | next [-]

From what I understand all of them have Lean proofs/certificates thus are basically 100% proven without a doubt.

samrus 2 minutes ago | parent | next [-]

We recently saw that lean itself isnt proven correct. Its not likely but i wouldnt call it verified if its only verified in lean

https://x.com/gro_tsen/status/2082483878480977959

voxl 13 minutes ago | parent | prev [-]

Incorrect. The statement in Lean can itself be wrong. Moreover, they could be exploiting a kernel bug in Lean, of which we had one published literally a week ago.

gpm an hour ago | parent | prev [-]

I mean, they're verified in the sense that the lean proof checks out... and presumably OpenAI read them.

an hour ago | parent [-]
[deleted]