If those OpenAI proofs are unpublishable garbage then our concept of publishing has to change. Pure math will probably shift from journals publishing PDFs to individuals (or their agents) posting Lean code in Git repos.
That’s like skipping to the end of an important novel and thinking you got something out of it.
The issue is that the auto-formalization step itself is not trivial. There is no formal verification which proves the translation correct, so it is up to mathematicians to hand-check the formalization to make sure it’s saying the same thing. Unfortunately, this problem is undecidable in general.
We’ve already had a paper showing that auto-formalization can’t be trusted implicitly [1], so a GitHub repo of a bunch of Lean code can’t be trusted to prove what the title claims is being proved.
Wasn't it just a few years ago that there were all sorts of apps ("Blinkist" ?) being pushed hard that did just that: give you the TLDR on some publication so that you could pretend to have read & understood it?