Formal mathematics
Axeyum Library
A dependency-aware library of checked facts with explicit evidence and assumptions.
New to Library?
What must a library retain so that one checked result can support another?
Lesson 9 explains facts, dependencies, assumptions, and provenance. Lesson 10 compares constructive and classical axiom footprints.
Implementation
Axeyum implements its formal library as a typed fact ledger. Each fact records its statement, proof route, evidence, assumptions, provenance, and dependency edges.
The library includes a constructive base whose kernel-checked declarations have an empty axiom footprint. The mathlib comparison identifies where imported classical analysis uses choice, propositional extensionality, or quotient soundness.
- Typed fact records and semantic validation
- Direct dependency and dependent edges
- Proof-route and evidence metadata
- Axiom-footprint reporting
Rust crates
These crates implement the component or connect its results to another Axeyum checker. Each link opens the crate's source directory.
Reference systems and results
mathlib is the principal reference library and a source of selected statements and exports.
Read the mathlib comparisonProblems studied with this component
- Primality of 2^89 - 1 Number theory
- Two four-color Rado numbers Combinatorics
- Optimal sorting networks on three to six channels Computer science
- A BCNF decomposition counterexample Database theory
- The cause of an infeasible ICU roster Operations research
- The cause of an impossible project deadline Operations research