You're putting a lot of words in my mouth. What I'm saying is that whether or not it's a proof, it's useless: it does not improve human knowledge, because the only thing able to consume 10MB of Lean to build upon it is another LLM that's going to build a 50MB piece of shit.
It's very much likely a proof. It's also completely useless.
It's very much likely a proof. It's also completely useless.