C++17 · ANTLR4 · Math Verification
pearl‑proof
A math-checker language that verifies algebraic equations by converting both sides to canonical polynomial form and checking their difference is zero.
Try it
The language in action
check
1 + 1 = 2
OK
check
x + x = 2 * x
OK
check
(a + b)^2 = a^2 + 2*a*b + b^2
OK
check
(x + y) * (x - y) = x^2 - y^2
OK
check
x^3 = x * x * x
OK
check
(x + 1)^2 = x^2 + 1
ERROR
check
2 + 2 = 5
ERROR
How it works
01
Parse
ANTLR4 grammar tokenises and parses the .proof file into a parse tree
02
AST
Visitor pattern walks the tree and builds a typed expression AST
03
Expand
Both sides are converted to canonical polynomial form — a map of monomials to coefficients
04
Verify
poly(A) − poly(B) is computed. If the result is the zero polynomial: OK. Otherwise: ERROR
What it supports
Operators
Addition, subtraction, multiplication, integer division, and right-associative exponentiation
Expressions
Integer constants, named variables, parenthesised grouping, and unary negation
Polynomial engine
Full symbolic arithmetic — add, subtract, multiply, power — over multivariate polynomials with integer coefficients
Batch checking
Checks every line in a .proof file and reports the line number of each OK or ERROR independently
Build & run
# Prerequisites: CMake 3.10+, C++17 compiler, ANTLR4 C++ runtime, JRE
mkdir build && cd build
cmake ..
make
# Run against a .proof file
./pearlproof test.proof
Stack
C++17
ANTLR4
CMake
Visitor Pattern
Polynomial Arithmetic
GitHub Actions CI
Node.js · Express