# Mathlib

21 Hacker News commenters recommended Mathlib and 8 criticized it, November 2025 to November 2026. It was recommended in 9 of 13 months. It meets the Hacker Approved badge rule.

**Verdict:** Free, community-built Lean library of formalized mathematics, praised for its broad coverage, reusable proofs and well-designed API. Critics say it is slow and cumbersome for newcomers.

## Why people recommend it

- Broad library of formalized mathematics (3 comments): "Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics." ([source](https://news.ycombinator.com/item?id=48694801)) "Lean's mathlib has done most of the underlying work so that you have its axioms and necessary lemmas baked in." ([source](https://news.ycombinator.com/item?id=49650586)) "mathlib is only 2.3 million lines of code, and took nine years to write." ([source](https://news.ycombinator.com/item?id=49113586))
- Reusable proofs and lemmas (3 comments): "Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool!" ([source](https://news.ycombinator.com/item?id=49141629)) "Lean's mathlib has done most of the underlying work so that you have its axioms and necessary lemmas baked in." ([source](https://news.ycombinator.com/item?id=49650586)) "I generally rather rely on someone else getting the category theory and algebraic structures right" ([source](https://news.ycombinator.com/item?id=49063008))
- Flexible proof style, good API (2 comments): "Whatever style of proof you're used to, you can write in that style with mathlib." ([source](https://news.ycombinator.com/item?id=49940638)) "mathlib is very well-designed and has a very good API" ([source](https://news.ycombinator.com/item?id=49325035))
- Open source community project (2 comments): "is organized like an open source community with pull requests" ([source](https://news.ycombinator.com/item?id=45791335)) "Mathlib for instance is of course a phenomenal project" ([source](https://news.ycombinator.com/item?id=49112227))

## What people warn about

- Slow builds and checks (2 comments): "Lean4 with a mathlib project seems really slow" ([source](https://news.ycombinator.com/item?id=46616094)) "so slow with the main math package" ([source](https://news.ycombinator.com/item?id=47103576))
- Cumbersome for researchers and newcomers (2 comments): "mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry" ([source](https://news.ycombinator.com/item?id=48493147)) "the default Mathlib4 style is really unapproachable without the tooling" ([source](https://news.ycombinator.com/item?id=48796508))
- Some formal statements are wrong (2 comments): "Mathlib is not perfect, and it's not hard at all to have a Lean statement that isn't what you think it is." ([source](https://news.ycombinator.com/item?id=50035848)) "the Lean formalization of the Riemann Hypothesis in Mathlib was incorrect" ([source](https://news.ycombinator.com/item?id=50008345))
- Monolithic package, heavy dependency (2 comments): "having a mathlib dependency just to build a programming language is a big ask for people" ([source](https://news.ycombinator.com/item?id=50130541)) "they like sticking everything into Mathlib and not splitting off smaller packages" ([source](https://news.ycombinator.com/item?id=49327872))

## Cite as

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