Yes, but humans using the proof assistants need to be able to read and understand the proofs while they are constructing them.