An Anecdote Against Slop Artifacts

For a formal proof related post, this is a bit weird. The author tells a story of their own mistake they found by accident. Then in closing they say "some people believe that you can simply slop out a proof" and how your have to be an expert to check it. It doesn't follow. At the very least they could've shown that LLMs can make a similar mistake. Would LLM be better or worse at spotting that omission? We don't know.