Formal knowledge
Formal library
A maintained collection of definitions, theorems, proofs, and their relationships.
Definition
Formal library
A formal library stores reusable declarations in a form that its proof system can check.
The library supplies vocabulary and results for later work. mathlib is the principal mathematical library for Lean; the Axeyum Library is a separate, much smaller fact ledger with several evidence routes.
01
Example
A linear-algebra theorem can reuse earlier declarations about fields, vectors, matrices, and finite sums.
02
Important distinction
Library size alone does not measure trust, coverage, ease of use, or the assumptions behind individual declarations.
After reading this article, you should be able to
- Define Formal library in the sense used on this site.
- Explain how a formal library reduces repeated work in later proofs.