Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com