Not really sure if it's sarcasm, but let me make a side remark. It's really stunning how much more effective the "Standard ML" notation (embraced by Haskell, L

Not really sure if it's sarcasm, but let me make a side remark. It's really stunning how much more effective the "Standard ML" notation (embraced by Haskell, Lean etc.) is compared to writing proofs in classical logic. This "UX problem" is, I think, the reason why is mathematical community embracing automated provers maybe 50 years later than they could have. Automated people wanted the better language, but the mathematicians largely resisted. So seeing this, it would be preposterous for me to think that any language, natural or not, has the last say in this. We're gonna be stuck with learning new languages and formalisms for a long time.