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!
True, but its a different form of disrespect, where they outwardly steal the style and aesthetics of the discipline to try to claim its legitimacy. Like the endless “whitepapers” pumped out by cryptobros.
That’s fair. I deliberated a while over how I might describe their relation to CS.