so on OpenAI's math proofs, which are generating a pile of Lean that compiles and may or may not match the problem statement

mathematicians are already saying this isn't useful, even if it does match the problem statement, which is years of work to determine that fewer and fewer people are willing to do for blatant spam

i am not a mathematician, but I'm getting the idea these "proofs" aren't useful in any applicable sense at all. are there any that are?