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:

• OpenAI already retracting a few papers

Let me know in the comments if you have any links I should to these lists!