It would be extremely unlikely human mathematicians able to solve these kinds of problems would accept not getting credit that would set them for life professionally.

Also lean proofs are notoriously tedious and slow to write so this level of output is very likely to be from LLMs. The number of people able to understand this level of math and prove it using Lean is a few hundred at most.