The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Dear coq-club,

You may be interested in the slides of a talk given by Neil Stickland
at the Homotopy Type Theory Workshop, a few weeks ago in Oxford. It
reads as an experience report of something relatively experienced with
proof assistants trying to prove a basic mathematic fact (there are
infinitely many primes) and listing the hurdles (in tooling,
documentation, web search, etc.) along the way.

  http://www.qmac.ox.ac.uk/events/Talk%20slides/Neil%20Strickland.pdf

You will probably find little surprising there, but I think that
seeing those pain-points in the context of a concrete use-case --
instead of problems in the abstract -- helps.