Can you explain why the author makes this remark? I'm not a math person. I thought having a Lean formalized proof was the only way these models were able to get through complex math proofs. My naive thought was that you could set an LLM loose on a math problem and it would try to build the Lean to get you from your starting point to a proven result. And the fact that Lean is machine checkable is how AI tools are able to do this autonomously.

So why would the author claim there isn't a Lean proof available? Shouldn't there be?