Comment by egl2020

Maybe we need "de Moura complexity": the shortest Lean proof of a theorem.