Computer algebra
Checked computer algebra
Axeyum implements its own computer algebra system with explicit checks and ledger records for supported operations. Mathematica and SymPy provide reference points for broader symbolic mathematics systems.
Components
Current CAS routes
- 60
- facts on a CAS certificate route
- 14
- CAS results reconstructed in the proof kernel
- 46
- CAS-internal facts python3 scripts/validate-facts.py @ a103b3db3, 2026-09-03
What the comparison means
SymPy is an open-source Python computer algebra system. Mathematica is a broad commercial computation system and language. Both cover far more operations and user workflows than Axeyum.
Axeyum's focus is the boundary after a computation. A supported operation can return structured evidence, an independent checker can validate it, and the accepted proposition can enter the same dependency graph as a kernel-checked theorem or solver result.
Snapshot a103b3db3 · 2026-09-03. Source: python3 scripts/validate-facts.py @ a103b3db3, 2026-09-03.