Learn · By field
Find Axeyum from your field
Each guide identifies results and system properties that matter to one field. It then states the current boundary and the work that would extend it.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation How to use these guides
Start with the mathematics you know
Each field begins from a different point in the current library. A guide starts with what the system can prove or compute. The next section explains why those results matter. The final section names work that can extend the field from its present base.
Readers who are new to SAT, SMT, computer algebra, or proof checking can begin with the getting started page before opening a field guide.
What can the constructed natural and integer libraries prove?
Axeyum contains a substantial constructive development of elementary number theory over natural numbers and integers built inside its kernel.
Open the guide → Constructive analysisWhat analysis remains computational when choice is not assumed?
Axeyum builds real numbers from regular rational sequences and carries explicit approximation data through its analysis library.
Open the guide → Classical analysisHow does a constructive library compare with familiar classical analysis?
Axeyum provides a concrete place to compare classical existence theorems with constructive algorithms and explicit assumptions.
Open the guide → AlgebraHow much abstract algebra is available over the constructed carriers?
Axeyum has a checked structure hierarchy and concrete algebraic instances, with quotient-based algebra as a clear next frontier.
Open the guide → GeometryWhat geometry has been checked over the constructed real plane?
Axeyum has a substantial coordinate-geometry library over its constructed real numbers, with both kernel proofs and computer algebra certificates.
Open the guide → TopologyWhat topological ideas are already present in the analysis library?
Axeyum currently treats continuity and compact-interval arguments through explicit real analysis rather than through a general theory of spaces.
Open the guide → CombinatoricsHow do proof, search, and symbolic computation meet in finite mathematics?
Axeyum combines a constructive finite-carrier library with proof-producing search and certificate-producing symbolic computation.
Open the guide → Probability and statisticsWhat can be proved without a measure-theory library?
Axeyum now has a finite, rational-valued probability development with expectation, variance, covariance, concentration, and a weak law of large numbers.
Open the guide → Category theoryCan a concrete-carrier library grow a useful abstraction layer?
Axeyum offers a clear experiment in adding abstraction above independently constructed carriers and measured trust boundaries.
Open the guide → Logic and foundationsWhat exactly does the kernel assume and check?
Axeyum's kernel, trust accounting, and constructive models make the foundations of each result available for direct inspection.
Open the guide → Applied and computational reasoningHow do search, symbolic computation, and proof checking cooperate?
Axeyum implements SAT, SMT, computer algebra, proof checking, and a fact ledger in one Rust system with explicit evidence between stages.
Open the guide → Project evaluationWhich claims can an external reviewer verify directly?
Axeyum publishes countable claims about proof status, trust, evidence routes, comparison coverage, and automated production.
Open the guide →