Comment by YetAnotherNick

Lean went other way on automation that there is no automation. Isabelle users frequently point that decades old isabelle is better than Lean on this. In the end Lean approach proved to be better with LLM as the outer loop is automation.