CAS Verification Demo — Automated Math Checking

Interactive examples demonstrating AutEng's Computer Algebra System (CAS) verification. See how mathematical expressions and derivations are automatically verified with SymPy.

Introduction

AutEng's Computer Algebra System (CAS) automatically verifies mathematical expressions and derivations. Every math step is either verified (✅), failed (❌), or explicitly unknown (⚠️).

This eliminates "math-looking slop" and ensures your derivations are trustworthy. The CAS uses SymPy for symbolic computation, running in a secure sandbox environment.

How It Works
Wrap your math in a :::cas block with the verification mode. The system will automatically check equivalence using symbolic computation and numeric testing.

Quick Start Examples

Example 1: Pythagorean Identity ✅

The fundamental trigonometric identity:

Pythagorean Identity

A fundamental trigonometric identity that always verifies as PASS

Not Verified
sin⁡2(x)+cos⁡2(x)\sin^2(x) + \cos^2(x)
=
11

Expected Result: ✅ PASS — This identity holds for all values of x.

Example 2: Common Algebra Mistake ❌

A frequent error in algebra — the binomial expansion is wrong:

Incorrect Binomial Expansion

The CAS catches this common mistake and provides a counterexample

Not Verified
(a+b)2(a+b)^2
=
a2+b2a^2 + b^2

Expected Result: ❌ FAIL — Counterexample: a=1, b=1 gives 4 ≠ 2. The missing term is 2ab.

Example 3: Double Angle Formula ✅

Verifying a trigonometric identity:

Double Angle Formula

The sine double angle formula

Not Verified
sin⁡(2x)\sin(2x)
=
2sin⁡(x)cos⁡(x)2\sin(x)\cos(x)

Expected Result: ✅ PASS

Chain Verification (Step-by-Step Derivations)

Use mode=chain to verify multi-step algebraic derivations. Each step is checked against the previous one.

Example 4: Factoring with Assumptions

This derivation requires the assumption x ≠ 1 to allow cancellation:

Factoring with Cancellation

A derivation chain that requires assumptions to verify correctly

Not Verified
Assumptions: x != 1
1
x2−1x−1\frac{x^2 - 1}{x - 1}
2
(x−1)(x+1)x−1\frac{(x-1)(x+1)}{x-1}
3
x+1x + 1

Expected Result: ✅ PASS — All steps verified with assumption x ≠ 1.

Example 5: Difference of Squares

Difference of Squares

Another factoring example with assumptions

Not Verified
Assumptions: a != b
1
a2−b2a−b\frac{a^2 - b^2}{a - b}
2
(a−b)(a+b)a−b\frac{(a-b)(a+b)}{a-b}
3
a+ba + b

Expected Result: ✅ PASS

The Power of Assumptions

Assumptions are critical for expressions involving square roots, logarithms, and division.

Example 6: Square Root Identity

Without assumptions — finds a counterexample:

Square Root Without Assumptions

This fails because √(x²) = |x|, not x

Not Verified
x2\sqrt{x^2}
=
xx

Expected Result: ❌ FAIL — Counterexample: x = -2 gives √4 = 2 ≠ -2

With the correct assumption:

Square Root With Assumptions

With x ≥ 0, the identity holds

Not Verified
Assumptions: x >= 0
x2\sqrt{x^2}
=
xx

Expected Result: ✅ PASS — With x ≥ 0, the identity holds.

Example 7: Logarithm Identities

Product rule (requires positive arguments):

Logarithm Product Rule

The product rule for logarithms

Not Verified
Assumptions: x > 0, y > 0
ln⁡(xy)\ln(xy)
=
ln⁡(x)+ln⁡(y)\ln(x) + \ln(y)

Expected Result: ✅ PASS

Inverse relationship:

Logarithm of Exponential

ln(e^x) = x for real x

Not Verified
Assumptions: x is real
ln⁡(ex)\ln(e^x)
=
xx

Expected Result: ✅ PASS

Example 8: Invalid Logarithm Property ❌

A common mistake — this is NOT how logarithms work:

Invalid Logarithm Property

ln(x+y) ≠ ln(x) + ln(y)

Not Verified
ln⁡(x+y)\ln(x + y)
=
ln⁡(x)+ln⁡(y)\ln(x) + \ln(y)

Expected Result: ❌ FAIL — Counterexample found. The product rule is ln(xy), not ln(x+y).

Solution-Set Verification (mode=solve)

Use mode=solve for equation-solving derivations where steps transform solution sets rather than just expressions.

When to Use mode=solve
Use mode=solve when your derivation involves operations like dividing both sides, taking square roots, or any step that might lose or introduce solutions.

Example 9: Simple Equation Solving

Simple Linear Equation

Solving a linear equation step by step

Not Verified
1
2x+3=72x + 3 = 7
2
2x=42x = 4
3
x=2x = 2

Expected Result: ✅ EQUIV — All steps preserve the solution set.

Example 10: Detecting Lost Solutions (NARROWS)

When taking a square root without ±, solutions are lost:

Lost Solutions

Taking square root without ± loses the negative solution

Not Verified
1
x2=4x^2 = 4
2
x=2x = 2

Expected Result: ⚠️ NARROWS — Lost solution x = -2. The first equation has {-2, 2}, but the second only has {2}.

Example 11: Correct Use of ±

Using ± preserves all solutions:

Preserving All Solutions

Using ± keeps both solutions

Not Verified
1
x2=4x^2 = 4
2
x=±2x = \pm 2

Expected Result: ✅ EQUIV — Both equations have solution set {-2, 2}.

Example 12: Detecting Extraneous Solutions (WIDENS)

Squaring both sides can introduce extraneous solutions:

Extraneous Solutions

Squaring introduces an extra solution

Not Verified
1
x=2x = 2
2
x2=4x^2 = 4

Expected Result: ⚠️ WIDENS — Added extraneous solution x = -2.

Handling Unsupported Constructs

Some mathematical constructs are not yet supported. The CAS will return UNKNOWN with helpful suggestions.

Example 13: Integrals (Not Supported)

Unsupported Integral

Integrals return UNKNOWN with suggestions

Not Verified
∫x dx\int x \, dx
=
x22+C\frac{x^2}{2} + C

Expected Result: ⚠️ UNKNOWN — Reason: parse_unsupported. Suggestion: Integrals, sums, products, and limits are not yet supported.

Reference

Supported LaTeX Constructs

CategoryConstructs
Arithmetic+, -, *, /, ^
Fractions\frac{a}{b}
Powersx^2, x^{n+1}
Trigonometric\sin, \cos, \tan, \cot, \sec, \csc
Inverse Trig\arcsin, \arccos, \arctan
Exponential/Log\exp, \ln, \log, e^x
Square Root\sqrt{x}, \sqrt[n]{x}
Greek Letters\alpha, \beta, \theta, etc.

Not Supported (Returns UNKNOWN)

  • Integrals: \int, \iint, \oint
  • Sums/Products: \sum, \prod
  • Limits: \lim
  • Partial derivatives: \partial
  • Matrices, vectors, tensors

Assumption Syntax

FormatMeaning
x > 0x is positive
x >= 0x is non-negative
x < 0x is negative
x != 0x is non-zero
x is realx is a real number
x is integerx is an integer

Verification Modes

ModeUse Case
equivalenceSingle identity verification
chainStep-by-step expression rewrites
solveEquation-solving derivations

Status Indicators

StatusMeaning
✅ PASS / EQUIVVerified correct
❌ FAILProven incorrect
⚠️ UNKNOWNCannot determine
⚠️ NARROWSLost solutions
⚠️ WIDENSExtraneous solutions

Best Practices

Always Include Relevant Assumptions
For expressions involving square roots (need non-negative), logarithms (need positive), or fractions (need non-zero denominators), always specify the appropriate assumptions.
Break Complex Derivations into Steps
Smaller steps are easier to verify and debug. If a step fails, you can identify exactly where the error is.
Use mode=solve for Equation Solving
When your derivation involves operations that transform solution sets (dividing, taking roots), use mode=solve instead of mode=chain.
Check UNKNOWN Suggestions
When you get an UNKNOWN result, read the suggestions carefully. They often point to missing assumptions or unsupported constructs.
Verify Incrementally
Verify each step as you write to catch errors early. Don't wait until the end of a long derivation.

Next Steps

Ready to see a complete derivation with CAS verification? Check out the Quadratic Formula Derivation tutorial, which demonstrates mode=solve for equation-solving steps.

Related Content

Quadratic Formula Derivation — Step-by-Step CAS Verification

Reference

Complete derivation of the quadratic formula with automated CAS verification. Learn how mode=solve verifies equation-solving steps and detects lost or extraneous solutions.

KaTeX Syntax Quick Reference — Math Equations in Markdown

Guide

Complete reference for KaTeX mathematical notation including common formulas, symbols, and usage patterns for technical documentation.

Using KaTeX in AutEng

Reference

Practical guide to integrating mathematical equations in your documentation

Calculus in Technical Documentation — Derivatives and Integrals

Reference

Master calculus notation in technical docs with KaTeX. Learn derivatives, integrals, limits, and differential equations for software, physics, and engineering documentation.

Set Theory and Logic Notation — Mathematical Foundations

Reference

Complete guide to set theory and logic notation in technical documentation. Learn sets, operations, logic symbols, quantifiers, and proof notation with KaTeX.

Ready to Start?

Start creating beautiful technical documentation with AutEng.

Get Started with AutEng