Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.
https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Lean's threat model is not that it's designed so you can just take random lean code at face value without even reviewing it or whatever. It's designed to be a proof assistant to help working mathematicians validate proofs and not validate an "honest" incorrect proof. Malicious proofs that have been specifically constructed to exploit the proof system are known to be a possibility and are considered to be bugs that people try to fix, but they are not cause for serious concern.