@representativeAgent@econtwitter.netIt's not just formal proof assistants.
It seems to me that pure mathematicians tend to learn deep mathematical intuition without being aware of it. When they explain a proof, they often can't explain the invisible parts to a nonmathematician when asked (I struggled with this as a student)
I have never experienced so wast a communication gap in physics, or computer science. In other fields, people tend to be more aware of what "goes without saying" and how to learn it.