Comment by fsmv

The entire point of writing proofs is for advancing human understanding. A giant dump of symbols that passes the lean compiler is meaningless besides human beings understanding it.