“…and the proof is checked in Lean”

This post is an attempt to explain in simple terms how to interpret claims of the form “this theorem is correct because it was checked in Lean”. The summary is: there is an important signal that can be extracted from Lean code, but if this code is AI-generated then you need to do some tests first. We explain the tests, and note that in many cases (such as the OpenAI theorem dump) these tests have not yet been systematically done. Introduction Last month’s theorem dump by OpenAI consisted of 722 mathematics papers, around 45% of which came with some Lean code. Three of the (non-Leanified) papers have since been retracted because of a sign error. Some people might say “well, the papers that come with Lean code are definitely correct because that’s how Lean works”. Others might say “well Lean had a soundness bug and could well have more, and AIs will reward hack, so Lean verification doesn’t tell us much at all”. The truth, unsurprisingly, is more subtle, and this post is an attempt to…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town