Hacker News Reader

Comment by pcstl | Hacker News Reader

This seems very interesting and something which might catch a lot more interest than it probably will if its homepage didn't look so dated and text-heavy.

I'm very much in favor of initiatives to make math more accessible to laypeople and this is right in my ballpark, but just reading over the homepage gave me visual fatigue.

View on HN

Metamath is very different from an initiative to make math more accessible. This is a specialist project to write formal/mechanical proofs of many theorems.

I would be curious to discuss how this can be useful in practice for laypeople, but I don't see any.

The way it is described (especially the emphasis on how variable substitution is used as the single primitive instead of many different techniques which can take years to learn - a phrase which is repeated many times on the website) suggests to me that accessibility to people who would not usually write proofs is a concern of the project. If it is not, the project might not be doing a good job of communicating its goals clearly.

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.

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.

I'll take text-heavy over javascript-heavy any day.

Sure, same here. However, I’m not talking about that tradeoff. I’m talking about organizing all the text a little better.

Reply on news.ycombinator.com