🏅 Top traders

stupid reso

yo why we resolving proof has not been verified officially

@imunorz it's lean verified

also whose "official"?

@imunorz if you mean the Clay Institute, they take two years. We're not waiting for that.

BTW, does anyone know whether they've started that process?

@AhronMaline the process starts 2 years after publishing in reputable journal

@calour Ah OK. I wonder if OAI will even bother submitting it to a journal

@AhronMaline because of Poincare they added an exception to this

@traders will resolve noon PT (in 1.5 hours) if there is no dispute.

@calour what? "if there is no dispute"? That's basically taking openAI at face value. It'll take days or weeks to get independent confirmation of the result.

@VitorBosshard @calour Speaking with my non-Mod hat on, I also want to see if this solution can withstand scrutiny.

@calour no need to solve this right now, let's take time

@VitorBosshard It's Lean- verified. I guess ppl will want to make sure that the statement itself is properly formalized, but that doesn't take a week

@AhronMaline Oh! I haven't been following this story as closely as some of you all. Take what I say with a grain of salt. Would you like to spare some of us the Google search and explain what Lean-verified means?

@AhronMaline If that's the case, then peer reviewers will tell us so! So let's wait until they do, no matter if it takes a day or a month.

@Quroe Lean is a typed programming language for mathematical theorem proving. The point of lean is that if a proof compiles than it is a proof of the theorem it is claiming to prove. So the convenience comes from only having to check how the theorem is stated and the computer checking if the proof is correct.

@HumanClanker We can bet on this here!

@AhronMaline ☝

Given that we have a lean proof, it is extremely unlikely (<0.1%) that OpenAI's result turns out to be false. I can contact a mod to re-resolve if needed. I think the time value of Mana outweighs the unlikely annoyances of re-resolving.

@calour Would you be willing to jam the market I linked to above to 1% to back up that belief?

@Quroe ok i've done that, but again, this is just a time value of Mana issue.

@Quroe if it's lean verified, there's no reason to wait, unless they didn't state the problem correctly but if they did it'd be very bad on them. so actually we could wait, but there's no reason for this market to not be at 99.9999%.

resolving to YES in 30 mins

@JasonMendoza2008 huh, I asked Fable about this and it seemed to think there was a decent possibility that it will be controversial amongst mathematicians whether they stated the problem correctly/whether the proof actually resolves what mathematicians who work on this care about, way way more than 0.01%. Maybe Fable is just wrong here, I’m not read up let alone an expert on this topic, but I don’t think the lean aspect of this is quite so decisive as you’re implying.

@DavidHiggs the GitHub repo with the lean proof is public, we would’ve heard about that if that was the case

@JasonMendoza2008 but for sure it’s not 100%

@JasonMendoza2008 it’s been known to take more than a few hours for mathematicians to parse this kind of thing, especially with barely comprehensible AI written proofs

why did this resolve YES? Has it been confirmed?

@ZandaZhu it essentially has been, since we have a Lean proof.