So the boosters are making a big deal about the dump of “proofs” OpenAI has made recently, so I thought I would collect some relevant links in one place…
Stuff on autoformalization:
- A short blog post breaking down some of the bugs found and potential for more
- preprint discussing the problems with natural language to lean in detail and pointing out some blatant inconsistencies in the recent Navier-stokes “proof”
- /r/betteroffline discussion of above preprint
- Some of our very good friends are aware of the problem! Of course, this is lesswrong, so there is a tinge of “this is why we need to be careful with using this sort of approach to make our AI God”.
- The soundness bug that led to the fallacious disproof of the Collatz Conjecture
And some other related links:
Let me know in the comments if you have any links I should to these lists!
Thread: https://bsky.app/profile/gro-tsen.bsky.social/post/3mxeqyegazk2h
The theory on the thread that
seems like a plausible explanation? I’ll guess we’ll if OpenAI moves on now that they’ve “solved” math or if they follow up with a few more drops of “proofs”.