I wonder how are they sure the proof is correct before making a Lean translation. How is the work loop organised to force LLMs to reach a valid solution. I thought the ability to make it possible was the main advantage of using Lean.