# Metamath

14 Hacker News commenters recommended Metamath and 4 criticized it, November 2025 to November 2026. It was recommended in 7 of 13 months. It meets the Hacker Approved badge rule.

**Verdict:** People recommend Metamath for its tiny, simple verifier kernel and the free book that teaches formal proofs. The most common caveat is that its tooling and interface feel archaic.

## Why people recommend it

- Tiny kernel, simple to implement (4 comments): "metamath's design really speaks to me" ([source](https://news.ycombinator.com/item?id=47634932)) "it's very simple, so much so that there are many implementations of checkers" ([source](https://news.ycombinator.com/item?id=47927210)) "Tiny checker kernel, no complicated dependent types, way less to go wrong." ([source](https://news.ycombinator.com/item?id=49572173))
- Free book explains how it works (3 comments): "If one takes the time to read the free book accompanying the metamath software, and re implements it in about a weekend time, you learn to understand how it works internally." ([source](https://news.ycombinator.com/item?id=46252847)) "If one takes the time to read the free book accompanying the metamath software" ([source](https://news.ycombinator.com/item?id=46251071)) "the website does a good job at introducing the system, while also offering a complete reference" ([source](https://news.ycombinator.com/item?id=46942234))
- Separate, trustworthy kernel and verifiers (3 comments): "At least the metamath verifiers will not bend over backwards and come up with absurd inconsistent counterarguments." ([source](https://news.ycombinator.com/item?id=49948684)) "seems to have a more trustable kernel wrt. the independent verifiers" ([source](https://news.ycombinator.com/item?id=49141629)) "prover and verifier are essentially separate code bases" ([source](https://news.ycombinator.com/item?id=46250943))
- Proofs hide nothing; transparent design (2 comments): "In Metamath the proofs hide absolutely nothing." ([source](https://news.ycombinator.com/item?id=49110439)) "metamath's design really speaks to me" ([source](https://news.ycombinator.com/item?id=47634932))

## Alternatives hackers recommend

- [Lean 4](https://hackerapproved.com/p/lean.md): 268 recommend
- [Rocq](https://hackerapproved.com/p/rocq.md): 25 recommend
- [Coq](https://hackerapproved.com/p/coq.md): 24 recommend
- [Agda](https://hackerapproved.com/p/agda.md): 19 recommend
- [Isabelle](https://hackerapproved.com/p/isabelle.md): 14 recommend

## Cite as

Hacker Approved, "Metamath", https://hackerapproved.com/p/metamath/ (counts from 1,795,640 Hacker News comments, November 2025 to November 2026).