The difference is that in a proof assistant, you cannot gloss over a detail. So many of the lines establishes well-known facts which a mathematician has internalized in their brain.
You could store that in a library (and many proof assistants do!) but then the proof would probably be harder to follow for a first time reader.
The end goal of proof assistance are simpler proofs. Telling the system system something like: "Proof. search by pigeonhole. crush. Qed." and all the details would be established by the assistant itself. This allows for concise proofs, especially in software where many proofs amounts to the invocation of some induction scheme and solving by rote substitution and rewriting.
> The difference is that in a proof assistant, you cannot gloss over a detail. So many of the lines establishes well-known facts which a mathematician has internalized in their brain.
Maybe an intermediate DSL that would allow some "fallacies" or shortcuts would also render the proof more readable to more people. And the weakness in the reasoning could be easily spotable by special keywords.
> You could store that in a library (and many proof assistants do!) but then the proof would probably be harder to follow for a first time reader.
I'm not sure I agree with that. There is a middle ground to find between rewriting a sort function everytime it is needed, and encapsulating everything in a main() function. Creating an API/DSL/Vocabulary is not easy, but def required to attract more developers.
> 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"
True, but in other languages, developers try to fill the gap with numerous libraries and languages on top of each others, with abstractions on top of abstractions. Proof assistants feel "stuck" at a low level, with high expertise required to use them.
The original proof I posted was organized slightly differently from your argument.
Some of those 120 lines were commentary, blanks and things like "qed". Also, I tried to used small steps in the proof. You can have a more concise proof if you are willing to take larger steps and rely more on automation. The cost is that the justification for the steps might become opaque to humans.
> The cost is that the justification for the steps might become opaque to humans.
If the machine can tell "this proof is correct". Does the proof really need to be reviewed by humans? As long the human can easily read the problem which is proved, if the machine says the proof is complete, it should be good enough.
If yes, proof assistants have to be improved on conciseness, imho