They should use LLM to verify/prove Lean soundness first before working on something that relies on Lean.

"Chain of soundness" i think.