Mathematics
Exact symbolic computation, formal definitions, checked theorems, and dependency-aware library construction.
Vision
A system that can extend checked knowledge
Axeyum is a system for constrained reasoning. It is designed for mathematics, software, and other domains where people formalize rules, test claims, and extend knowledge through checked results.
Objective
Solving and proving in one system
Automated solvers, computer algebra systems, proof kernels, and formal libraries usually expose different terms, evidence formats, and notions of acceptance. Axeyum implements these functions in one Rust workspace so a result can move from search or computation to a recorded, checked fact.
The long-term objective is repeated knowledge development. Axeyum should select a useful open statement, find or compute a result, check the relevant evidence, record the accepted fact and its assumptions, then use the changed dependency graph when selecting later work.
Applications
One reasoning substrate across several domains
The typed terms, solvers, evidence routes, kernel, and library support applications beyond formal mathematics. Each application retains its own semantics and checker requirements.
Software and systems verification
Constraint solving, symbolic execution, bounded model checking, transition systems, and replayed counterexamples.
Security and smart contracts
Typed path obligations for binary analysis and bounded symbolic execution of EVM bytecode.
Rules, policy, and compliance
Bounded checks for consistency, coverage, thresholds, allocation, authorization, and workflow reachability in human-authored formal models.
Property checking and test generation
Typed prove-or-counterexample interfaces with minimized models and deterministic regression tests.
Checked agent workflows
Models can propose rules, invariants, encodings, formalizations, or proof steps; Axeyum accepts results through the applicable checker.
System
Five native components
Each component is Axeyum's own implementation. External systems appear in benchmarks, differential tests, imports, and technical comparisons.
- Axeyum SAT Solver A native CDCL solver with AIG and CNF lowering and certificate support.
- Axeyum SMT Solver A typed SMT implementation with rewriting, theory solving, bit-blasting, models, and certificates.
- Axeyum CAS A proof-carrying computer algebra system for exact symbolic operations.
- Axeyum Kernel An independent Rust checker for a selected Lean-core term language.
- Axeyum Library A dependency-aware library of checked facts with explicit evidence and assumptions.
Knowledge development
Checked results change later work
A recorded fact matters when it supplies a dependency, a procedure, or evidence that later work can use. The library therefore stores dependency edges, proof routes, axiom footprints, and provenance with the proposition.
Foundations
Assumptions remain attached to each result
Axeyum includes a constructive mathematical base whose kernel-checked declarations can have an empty axiom footprint. Classical material remains useful, but its uses of choice, propositional extensionality, quotient soundness, or other axioms stay visible in the fact record.
The distinction applies per declaration. It does not classify mathlib as wholly classical, and an empty footprint does not make two statements equivalent when their carriers or hypotheses differ.
Compare the foundationsNext work
Broader coverage and more reusable results
Current development expands solver coverage, certificate production, kernel reconstruction, formal-library depth, and the procedures that select and reuse facts. The status reports measure those areas separately because progress in one does not establish progress in another.