it's a bit dated, but Terence Tao has a video of formalizing a proof with LLMs from 9 months ago which should be illuminating
Or is it as long as you formalize your theorem correctly, a valid lean program is an academically useful proof?
Are there any minimal examples of programs which claim to prove the thing without actually proving the thing in a meaningful way?
Otherwise, if you check that no custom axiom has been used (via print axioms), the proof is valid.
It's easy to construct such an example: Prove that for all a, b, c and n between 3 and 10^5, a^n=b^n+c^n has no solution. The unmeaningful proof would enumerate all ~10^20 cases and proof them individually. The meaningful (and probably even shorter) proof would derive this from Fermat's theorem after proving that one.