Learn · Number theory
Axeyum for number theorists
Axeyum contains a substantial constructive development of elementary number theory over natural numbers and integers built inside its kernel.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to number theory.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
What can the constructed natural and integer libraries prove?
The current library proves Wilson's theorem and its converse, quadratic reciprocity and its supplementary laws, Fermat's little theorem, Bezout's identity, Euler's totient formulas, and uniqueness of prime factorization. The same development includes finite sets, multisets, modular congruence, factorials, and binomial coefficients.
These results use Axeyum's constructed natural numbers and integers. Their kernel records an empty axiom footprint, so a reader can inspect the theorem statement, proof route, dependencies, and trusted declarations for each fact.
Why it matters
What the current work makes possible
- Major elementary theorems are connected through one checked dependency graph.
- The proofs do not assume excluded middle, propositional extensionality, function extensionality, choice, or Quot.sound.
- The computer algebra system also produces checkable primality, factorization, and Chinese remainder certificates.
- Open Mathlib comparison facts provide concrete targets for extending the library.
Results to inspect
Open the evidence
What comes next
Extend the present base
The next mathematical layer is modern algebraic number theory: ideals, rings of integers, field extensions, characters, and analytic estimates. That work depends on a stronger abstract algebra library and a clear policy for quotient equality.
Nearer-term work can deepen the existing constructive line through more multiplicative functions, Diophantine results, and executable bounds while reusing the current divisibility and finite-set base.
Where to begin