The Lean Mathematical Library
summary
A community-driven library for Lean 3 assembles a large body of formalized mathematics plus automation: 74 contributors and a maintainer team that grows to 13 produce a library with topology, linear algebra (reused by other projects), a general definition of manifolds, and tactics for algebraic normalization and linear arithmetic. The codebase embeds meta-programming tools for linting and doc generation, organizes structures with a type class hierarchy, and faces a planned but non-backward-compatible port to Lean 4 that will require migration.
AI-written summary · about
chapters (7)
- 0:00Start
- 4:52History
- 7:19Library contents
- 11:33Library highlights: linear algebra
- 15:00Tactics and infrastructure
- 17:02Community organization
- 18:11The future
related talks
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
19mA General Library of Legal Components
20mImplementation and Synthesis of Math Library Functions
20mFormalizing polynomial laws and the universal divided power algebra
01h 01mMulti-Modal Verification of Distributed Systems in Lean
28mCertifying rings of integers in number fields
58mFrom Formal Verification to Correctly Rounded Math Libraries
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs