+1. And there's no guarantee that OpenAi haven't stolen unpublished research from multiple professors and PhD students.
replyThey have formal proofs included, that’s the point.
replyUnless humans have gone through the proofs line by line and verified them, this all remains unproven.
replyIf you're hoping for these results to be fake, you're going to have a bad time. A really bad time.
replydeleted
replyYeah but how am I meant to verify that the proof is proving what it says it is?
replyVerify the statement is correct + it doesn't introduce any new axioms + doesn't use "sorry" etc.
replyOrder of magnitudes easier than verifying the whole thing by hand and gives a much better guarantee of correctness
Do you know what "sorry" means in the context of Lean?
replyHow am *I* meant to do that
replyNote true for all of them.
replyWho made the formal proofs and who checked them?
reply