OpenAI shares mathematics research catalogue
15 points by bkruger
15 points by bkruger
Note that they do not yet claim to have finished Lean proofs for many of the write-ups.
There was a melancholy comment about this on Hacker News that I appreciated:
I spent thousands of hours on that problem. I really enjoyed it. Hearing that it is solved somehow makes me sad in a far-off way, like hearing an ex-girlfriend died suddenly in a car crash. I don't know, there's probably a lot of people feeling odd emotions tonight.
I would be excited to see P≠NP in there.
Still, I agree that dozens of pdfs are not convincing before at least some of them are verified either by humans or by machine-checked proofs.
Edit: which might be present in the lean directory.
Yes, it is claimed that some of the Lean proofs are checked and included in the repository.
It would be separately fun if this cyberattack-first model found yet another bug in Lean (like it apparently has done a few months ago) and used it in a couple of the proofs (but not in all of them), of course.