REVIEW 9 cited by
The Lean mathematical library
Not yet reviewed by Pith; the record is open.
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
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.
Forward citations
Cited by 9 Pith papers
-
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Agentic LLM framework autoformalizes 32 Putnam problems and main theorems plus proofs from five STOC papers into Lean 4, with two proofs using only kernel axioms.
-
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
An orchestrator-driven agentic pipeline using general coding LLMs autoformalizes 32 PutnamBench problems and the main theorems plus proofs from five STOC papers into Lean 4, with two proofs using only the kernel.
-
Formalizing Mathematics at Scale
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable for...
-
Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4
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.
-
To Throw a Stone with Six Birds: On Agents and Agenthood
Six Birds Theory defines agents as maintained theory objects with feasible policies that make counterfactual differences, operationalized via ledger feasibility, viability kernels, empowerment, and packaging maps, and...
-
Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts
Proof-Refactor is a four-phase agentic system that refactors LLM-generated Lean proofs from PutnamBench and Putnam2025 into more modular forms, outperforming a Claude Code baseline on rubric scores for signature quali...
-
Exploring Formal Math on the Blockchain: An Explorer for Proofgold
The authors present the first web explorer for the Proofgold formal-math blockchain, including case studies of category theory formalizations.
-
Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
An agentic theorem prover in Lean uses a control plane to route actions based on cost and success estimates, achieving 28.9% lower average cost than a fixed-step baseline on a PutnamBench subset while preserving performance.
-
Saturating Scaling Laws for Equational Discovery: A Phenomenology of Growth Dynamics in Three Toy Substrates with Two Real-World Replications
Growth of equational discoveries follows power laws whose exponent and saturation behavior are conditional on the substrate, with a heuristic saturating model fitting some real-world cases better than pure power laws.
Discussion (0). Sign in to comment.