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.
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.