Computer algebra is a diffuse branch of mathematics done with computers that encompasses
both computational algebra and analysis.
Computer algebra includes exact symbolic manipulation of mathematical expressions, such as polynomialcomputation,
symbolic integration, symbolic summation,
and equation solving. Practical symbolic
integration systems combine decision procedures such as the Risch
algorithm with heuristic, table-based, and rule-based methods; even when an elementary
antiderivative exists, implementations may miss
it (Desmond 2026).
Computer algebra can also supply exact checks for results proposed by artificial intelligence systems. For example, a claimed antiderivative
can be tested by differentiation and simplification
to determine whether it reproduces the integrand. Such
a check verifies the resulting identity, not the correctness
or significance of the process that produced the candidate (Wolfram 2026).
Checking a formal proof has a broader purpose than checking a symbolic identity. The Lean formalizations accompanying
OpenAI's (2026) mathematical release provide derivations of formal statements whose
inference steps can be checked by a computer. Symbolic calculation can support such
an argument, but checking the complete derivation and its assumptions is distinct
from simplifying an expression or testing a numerical example.
