Pith. sign in

REVIEW 3 cited by

The Lean mathematical library

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1910.09336 v2 pith:OIP547UN submitted 2019-10-21 cs.LO math.LO

The mathlib Community This is my paper
classification cs.LOmath.LO
keywords libraryassistantleanmathematicsorganizationproofarchitectureautomation
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led us here.

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4

    cs.LO 2026-02 conditional novelty 7.0 of 10

    A finite set of atomic Lean tactics plus a transposing atomization algorithm lets a small graph neural network, Nazrin, be trained on converted proofs and prove held-out formal theorems.

  2. Exploring Formal Math on the Blockchain: An Explorer for Proofgold

    cs.LO 2025-09 accept novelty 6.0 of 10

    The authors present the first web explorer for the Proofgold formal-math blockchain, including case studies of category theory formalizations.

  3. Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification

    cs.CL 2025-06 conditional novelty 6.0 of 10

    Safe uses step-level formal verification in Lean 4, aggregated by a small LSTM and combined with process reward scores, to improve best-of-n accuracy for LLM mathematical reasoning.

Pith tools