It’s far easier for Lean because the human has to read very little compared to generating whole programs.