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