Remix.run Logo
hodgehog11 2 hours ago

Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.

lumost an hour ago | parent [-]

How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”

adrianN 13 minutes ago | parent [-]

You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.