I would say that the vast majority of "real mathematicians" could not use such a proof system either - this is one of the major obstacles stopping the adoption

I would say that the vast majority of "real mathematicians" could not use such a proof system either - this is one of the major obstacles stopping the adoption of proof systems or proof assistants in the mathematical community. I think that even at the moment, what proof systems can prove is far far ahead of what regular users can easily express in those proof systems, and there really needs to be some programming language / human-computer-interaction work or research to bridge the gap there.