[andrepd]

> My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance.

Oh but absolutely, I agree 100%. I consider it the "holy grail" of interactive proof assistants: an assistant that understands mathematics as written by humans in papers, plus is capable of filling in intuitively trivial/boring steps. In other words: an assistant that is usable by someone with training in mathematics but not necessarily requiring training in the tool itself.