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!


It’s really fucking me up the way AI boosters and friends are treating mathematics as a natural science whose goal is to uncover mathematical facts in the number mines. I’m not even staunchly opposed to platonism, but my god. That’s not even how natural science works!
Random idiot on r/singularity
Also look out for the new obnoxious metaphor of “what if aliens descended from the sky and handed us their science and proofs, how is this different”. First of all shut up. Secondly we should assume the aliens in this scenario have reason, intent, and the ability to communicate through language. You’re imagining they’re using the scientific method and not divination from wiggling their proboscis in the fourth dimension. Which is quite different from OpenAI’s big dump on scientific practice.
The aliens metaphor is already on Scott’s blog: https://scottaaronson.blog/?p=10169#comment-2041386
The AI-as-aliens metaphor has existed for a lot longer
It’s amazing, I saw it once randomly yesterday from some obnoxious bluskyer and I saw it a dozen more times today. It’s nice they all got the press release!
also maths are not a science there i said it
Someone on Scott Aaronson’s blog suggested math will become an empirical field now, where they run “experiments” by asking AI for lean proofs.
So yeah, it seems like this idiotic view is pretty popular among boosters.