> If yes, proof assistants have to be improved on conciseness, imho TBF the proof is written for readability, not concision. But also, this happens in program

> If yes, proof assistants have to be improved on conciseness, imho TBF the proof is written for readability, not concision. But also, this happens in programming as well: "A search function looking for `x` in a sorted list that starts in the middle of the list, compares the element to `x`, and then recursively searches the front half or back half of the list" "A valid HTML document with one button that, when clicked, downloads a text file containing the md5sum of the page" "A facebook clone"