Funny.

The problem is that this is not something that LLMs (currently) can do.

Lean has nothing to do with understanding and intuition.

Brevity of proofs are also not the target.

The target isn't undergrads, either, but all of this is pointless because LLMs aren't up to this task (p.t.).