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
- 69
- facts on a CAS certificate route
- 16
- CAS results reconstructed in the proof kernel
- 53
- CAS-internal facts python3 scripts/validate-facts.py @ 03ae4a3c9, 2026-10-05
1 of the 16 kernel reconstructions is non-discriminating: its kernel obligation holds for every polynomial in place of the certificate's, so it does not test the certificate.
Public functions in axeyum-cas
- 151
- return a certificate
- 110
- check a certificate
- 1,019
- return a result with no certificate python3 scripts/check-cas-trust-registry.py @ 03ae4a3c9, 2026-10-05
The trust registry classifies all 1,280 public functions of the crate. The certified count is a floor the registry check enforces.
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 03ae4a3c9 · 2026-10-05. Sources: python3 scripts/validate-facts.py @ 03ae4a3c9, 2026-10-05; python3 scripts/check-cas-trust-registry.py @ 03ae4a3c9, 2026-10-05.