[digama0]

If you ever use another proof assistant, you will find that too much documentation is much better than not enough. You can certainly skip the documentation in the main pages if you get the gist. I think Metamath is most suited for a certain kind of person, the one who asks "why" incessantly and is attracted to precision of language. The best part is that you don't need to know any mathematics at all to understand it - everything is defined in excruciating detail, so it's completely self-contained.

[pcstl]

Too much documentation is definitely better than too little. But throwing all the documentation you have up front at a new user instead of having it tucked away where it can be easily browsed when needed can make for an intimidating first contact.