Lesson 09

How a formal library reuses checked facts

What must a library retain so that one checked result can support another?

A formal library stores exact declarations and their dependencies. Axeyum's fact ledger also records evidence routes, provenance, status, and assumptions for results produced by several components.

Core component Open the LIBRARY implementation page

After this lesson, you should be able to

Trace dependencies and dependents through a small declaration graph.
Read a fact record by separating its statement, status, evidence, provenance, and axiom footprint.
Explain how the Axeyum Library differs from mathlib in scope and representation.

9.1

A declaration carries more than a title

The formal statement fixes the proposition. The proof route says how it was checked. Dependencies identify earlier facts used by the route, and provenance records where the statement and evidence came from.

A prose description helps a reader find and understand the fact, but it cannot replace the formal statement. Generated descriptions must also be marked when no person has checked their mathematical meaning.

9.2

Edges support later work

If theorem B uses theorem A, then A is a dependency of B and B is a dependent of A. The distinction supports impact analysis: changing A can affect B, while adding B increases the known uses of A.

A dependency graph can also guide new work. A missing fact that blocks many useful targets may deserve attention before an isolated fact of similar difficulty.

9.3

Several evidence routes share one ledger

A solver fact may carry a model or certificate. A computer-algebra fact may carry operation-specific evidence. A kernel theorem carries a proof term and formal dependencies. The ledger stores these routes in one schema without claiming that they share one trust boundary.

Status also matters. Proposed, checked, admitted, and rejected records answer different questions. A searchable catalog should let the reader filter by route, status, concepts, dependencies, and dependents.

9.4

Axeyum and mathlib serve different current scales

mathlib is the large formal mathematics library for Lean. It includes broad definitions, theorems, tactics, notation, and community-maintained interfaces. The Axeyum Library is much smaller and gives special attention to cross-route evidence and explicit axiom footprints.

Selected mathlib statements and exports can enter comparison or import work. mathlib is not a hidden runtime component of the Axeyum Library.

Worked example

Read a three-fact dependency chain

Fact A defines matrix multiplication. Fact B proves that the identity matrix is a left identity. Fact C uses B to simplify a verified linear transformation.

Record direct edges
B depends on A. C depends on B and may also depend directly on A's definitions.
Compute dependents
B is a dependent of A, and C is a dependent of B.
Follow assumptions
The axiom footprint of C includes every trusted declaration reached through B and its other dependencies.
Use the graph
If B changes, the library can identify C for rechecking. If another target needs a left-identity result, B is already available.

Result. The graph turns accepted facts into reusable inputs and makes their inherited assumptions visible.

9.5

Check your understanding

Answer each question before opening the explanation.

1 Why does storing two proof routes in one ledger not make them equally trusted?

Each route has its own checker, evidence, and trusted computing base, which the record must preserve.

2 If B depends on A, which fact is the dependent?

B is the dependent of A; A is the dependency of B.

Concept wiki

Terms in this lesson

All concepts