Lesson 06
How Axeyum checks symbolic results
How can a large computation return evidence that smaller code can check?
A computer algebra algorithm finds a result. An operation-specific checker tests the exact property claimed by that result, and selected results can also be reconstructed for the proof kernel.
After this lesson, you should be able to
- Describe the role of a computer algebra system and name several supported operation classes.
- Design a direct checker for factorization, differentiation, or an antiderivative.
- Distinguish an operation-specific certificate from kernel proof reconstruction.
6.1
The producer and checker do different work
A factorization algorithm may search through candidate factors, choose variable orderings, and use optimized polynomial data structures. A checker can ignore that search. It expands the returned factors with exact arithmetic and compares the result with the input polynomial.
This division is useful when checking is simpler than finding. It also narrows the claim: the checker accepts a factorization equality, not the producer's speed, completeness, or choice of the most useful factorization.
6.2
Certificates follow the operation
One certificate format cannot express every symbolic result well. Matrix inversion can carry a proposed inverse that is checked by multiplication. Polynomial greatest common divisor computation can carry Bézout coefficients. Integration can carry an antiderivative and its required conditions.
The checker must reject malformed evidence and false results. Mutation tests are useful here: change one coefficient, sign, bound, or dependency and confirm that the check fails.
6.3
Kernel reconstruction gives another route
Selected computer-algebra results can be translated into proof terms for the Axeyum Kernel. The kernel then checks the formal proposition using its own type rules and recorded dependencies.
The two routes answer related but different questions. An operation checker validates one mathematical relation directly. Kernel reconstruction places the result inside the formal library and exposes its axiom footprint.
6.4
Axeyum's computer algebra component
Axeyum implements selected exact operations in algebra, calculus, linear algebra, number theory, transforms, and differential equations. Mathematica and SymPy provide reference points for the broader computer algebra category; Axeyum does not call them in its default path.
Axeyum does not match their breadth, languages, package systems, or interactive workflows. Its current distinction is the explicit boundary between a produced result, its certificate, and later admission to the fact ledger.
Worked example
Check a polynomial factorization
A producer returns x² − 5x + 6 = (x − 2)(x − 3).
- Read the claim
The result claims an exact polynomial identity over the selected coefficient domain.
- Expand
Multiply the factors to obtain x² − 3x − 2x + 6.
- Collect
Combine the middle terms to obtain x² − 5x + 6.
- Compare
Every coefficient matches the input polynomial exactly.
- Reject a mutation
Changing the second factor to x − 4 expands to x² − 6x + 8, so the same checker rejects it.
Result. Exact expansion certifies the returned factorization identity.
6.5
Check your understanding
Answer each question before opening the explanation.
1 Why can a factorization checker be smaller than a factorization algorithm?
The checker only expands and compares the proposed factors; it does not need to discover them.
2 What extra information can kernel reconstruction add to a checked CAS result?
It places the proposition in the kernel environment with formal dependencies and an axiom footprint.
Concept wiki
Terms in this lesson
- CAS A program that performs exact operations on symbolic mathematical expressions.
- Operation-specific checker A checker written for the evidence returned by one class of computation.
- Evidence Data that another procedure can use to check a result.
- TCB The code and assumptions that must be correct for a result to be valid.
- Proof kernel The small part of a proof system that checks declarations and proof terms.