Skip to content

1 · Proving Identities

Prerequisites: a built zelph binary — see the Quick Start Guide. Nothing else. This page assumes no zelph knowledge.

Three lines

Start the REPL and type:

zelph> .import math
zelph+> <x> ~ polyring
(:needsring <x>) ⇐ (<x> ~ polyring)
zelph+> ? $( (1+x)*(1-x) ) ≡ $( 1 - x^2 )
Answer: (((&1 + x) * (&1 - x)) ≡ $( &1 - x ^ &2 )) = proven

That is a complete session. Three lines, and the last one is the theorem.

Take the lines in turn.

.import math pulls in the whole mathematical standard library — an arithmetic substrate, signed integers, polynomial normal forms, a symbolic term layer, differentiation, and the infix notation used below. It is a convenience: every module can also be imported on its own, and the reference lists what each contributes.

<x> ~ polyring declares the indeterminates. <…> is zelph's list syntax and ~ reads is an instance of, so this is a plain fact: the list <x> is an instance of polyring. It is not a directive to the parser — it is knowledge, and the deduction displayed beneath it shows a rule already reacting to it. With several indeterminates you write them in one list, outermost first:

zelph+> <x y z> ~ polyring
(:needsring <x y z>) ⇐ (<x y z> ~ polyring)

? … is the result-query prefix. It materialises the statement, runs inference to the fixpoint quietly, and then reports what the graph now knows about it. Without the ? you would enter the statement, watch the deductions scroll past, and query the result separately; ? is the one-line form.

≡ asks whether two terms are the same polynomial. Not "equal at the points I tried" and not "textually equal after expansion" — the same element of ℤ[x].

The notation

$( … ) is a term island: conventional infix notation with the usual precedence, spelled inside a statement that is otherwise ordinary zelph. Inside an island you may write + - * / ^, function application f(u), unary minus, integer literals, and parentheses.

Islands are pure surface. The expression $( 1 - x^2 ) generates precisely the same graph structure as the verbose form (&1 - (x ^ &2)), and due to zelph’s use of hash-consing for every term, both spellings meet at the identical node. You can combine them freely – the answer line above exemplifies this, displaying one side in verbose form and the other as an island, since zelph employs island notation exclusively when precedence permits omitting parentheses.

The & in &1 marks a numeral. It is not decoration: it distinguishes the number 1 from a node that happens to be called 1. You do not type it inside islands, but you will see it in output.

Everything below is a complete session after .import math.

Sophie Germain's identity — the classic factorisation that shows x⁴ + 4y⁴ is composite for every y > 1:

zelph+> <x y> ~ polyring
(:needsring <x y>) ⇐ (<x y> ~ polyring)
zelph+> ? $( x^4 + 4*y^4 ) ≡ $( (x^2 + 2*y^2 - 2*x*y) * (x^2 + 2*y^2 + 2*x*y) )
Answer: ($( x ^ &4 + &4 * y ^ &4 ) ≡ $( (x ^ &2 + &2 * y ^ &2 - &2 * x * y) * (x ^ &2 + &2 * y ^ &2 + &2 * x * y) )) = proven

The Brahmagupta–Fibonacci identity — the product of two sums of two squares is a sum of two squares, which is why the Gaussian integers are multiplicative:

zelph+> <a b c d> ~ polyring
(:needsring <a b c d>) ⇐ (<a b c d> ~ polyring)
zelph+> ? $( (a^2 + b^2) * (c^2 + d^2) ) ≡ $( (a*c - b*d)^2 + (a*d + b*c)^2 )
Answer: … = proven

Euler's four-square identity — the quaternionic analogue, eight indeterminates:

zelph+> <a1 a2 a3 a4 b1 b2 b3 b4> ~ polyring
(:needsring <a1 a2 a3 a4 b1 b2 b3 b4>) ⇐ (<a1 a2 a3 a4 b1 b2 b3 b4> ~ polyring)
zelph+> ? $( (a1^2+a2^2+a3^2+a4^2) * (b1^2+b2^2+b3^2+b4^2) ) ≡ $( (a1*b1-a2*b2-a3*b3-a4*b4)^2 + (a1*b2+a2*b1+a3*b4-a4*b3)^2 + (a1*b3-a2*b4+a3*b1+a4*b2)^2 + (a1*b4+a2*b3-a3*b2+a4*b1)^2 )
Answer: … = proven

A cyclotomic factorisation:

zelph+> <x> ~ polyring
(:needsring <x>) ⇐ (<x> ~ polyring)
zelph+> ? $( x^6 - 1 ) ≡ $( (x-1)*(x+1)*(x^2+x+1)*(x^2-x+1) )
Answer: … = proven

The binomial theorem, instantiated:

zelph+> <x y> ~ polyring
(:needsring <x y>) ⇐ (<x y> ~ polyring)
zelph+> ? $( (x+y)^5 ) ≡ $( x^5 + 5*x^4*y + 10*x^3*y^2 + 10*x^2*y^3 + 5*x*y^4 + y^5 )
Answer: … = proven

What "proven" means here

It is worth being precise, because the mechanism is unusually simple.

Each side is compiled to a canonical normal form: a recursive, dense, variable-tagged structure representing a multivariate polynomial over ℤ. Two polynomials are equal exactly when their normal forms match. Furthermore, because every term in zelph is hash-consed, equal normal forms are the same node.

So the whole proof rule is:

(A ≡ B, (:topoly A) = P, (:topoly B) = P) => ((A ≡ B) = proven)

Read it as: if A compiles to P, and B compiles to the same P — the same variable, so unification demands the identical node — then the identity holds. There is no equality checker to trust. The normal-form tutorial opens the representation up; here it is enough that it is canonical.

Looking at the proof

.explain reconstructs the justification of the last answer. It is a backward search over the saturated graph — zelph records no provenance during inference, so this is genuinely reconstructed, not replayed.

zelph+> <x> ~ polyring
(:needsring <x>) ⇐ (<x> ~ polyring)
zelph+> ? $( x^2 - 1 ) ≡ $( (x-1)*(x+1) )
Answer: ($( x ^ &2 - &1 ) ≡ ((x - &1) * (x + &1))) = proven
zelph+> .explain 3
($( x ^ &2 - &1 ) ≡ ((x - &1) * (x + &1))) = proven
   ├─ $( x ^ &2 - &1 ) ≡ ((x - &1) * (x + &1))  [axiom]
   ├─ (:topoly ((x - &1) * (x + &1))) = (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>)
   │  ├─ ((x - &1) * (x + &1)) aspoly (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>)
   │  │  ├─ :needstopoly ((x - &1) * (x + &1))  … [depth limit -- use '.explain <pattern> 0' for the full proof]
   │  │  ├─ ((x poly <(neg zint &1) (pos zint &1)>) pmul (x poly <(pos zint &1) (pos zint &1)>)) = (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>)  … [depth limit …]
   │  │  ├─ (x + &1) aspoly (x poly <(pos zint &1) (pos zint &1)>)  … [depth limit …]
   │  │  └─ (x - &1) aspoly (x poly <(neg zint &1) (pos zint &1)>)  … [depth limit …]
   │  └─ :topoly ((x - &1) * (x + &1))
   │     └─ $( x ^ &2 - &1 ) ≡ ((x - &1) * (x + &1))  [axiom]
   └─ (:topoly $( x ^ &2 - &1 )) = (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>)
      ├─ $( x ^ &2 - &1 ) aspoly (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>)
      │  ├─ :needstopoly $( x ^ &2 - &1 )  … [depth limit …]
      │  ├─ (x ^ &2) aspoly (x poly <(pos zint &0) (pos zint &0) (pos zint &1)>)  … [depth limit …]
      │  ├─ &1 aspoly (pos zint &1)  … [depth limit …]
      │  └─ ((x poly <(pos zint &0) (pos zint &0) (pos zint &1)>) psub (pos zint &1)) = (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>)  … [depth limit …]
      └─ :topoly $( x ^ &2 - &1 )
         └─ $( x ^ &2 - &1 ) ≡ ((x - &1) * (x + &1))  [axiom]

Three things are worth noticing.

The only leaf marked [axiom] is the statement you typed. Everything else was derived.

Both branches end at the same normal form, (x poly <(neg zint &1) (pos zint &0) (pos zint &1)>) — a polynomial in x with coefficient list −1, 0, 1, least significant first. That is x² − 1 as the machine holds it, and it is why the proof works.

The tree is cut at depth 3. .explain <pattern> 0 prints it in full, all the way down to the digit-level arithmetic that multiplied the coefficients. Nothing is hidden below a native implementation, because there is no native implementation.

Three answers, one of them silence

A false identity is answered, not merely left out:

zelph+> <x> ~ polyring
(:needsring <x>) ⇐ (<x> ~ polyring)
zelph+> ? $( (x+1)^2 ) ≡ $( x^2 + 1 )
Answer: (((x + &1) ^ &2) ≡ $( x ^ &2 + &1 )) = disproven

disproven needs no cleverness. Both sides compiled, to ⟨1, 2, 1⟩ and ⟨1, 0, 1⟩, and those are different nodes — so the verdict follows from the same node identity that gives proven, just the other way round.

The third answer is silence, and it means something specific:

zelph> .import math
zelph+> ? $( (1+x)*(1-x) ) ≡ $( 1 - x^2 )
zelph+>

Here <x> ~ polyring is missing, so x has no sort, neither side compiles, and there is nothing to compare. zelph does not report that as disproven — "I could not compile this" is not "these differ". Throughout the standard library, partiality is expressed by absence, so that a missing premise can never turn into a wrong verdict.

When encountering silence, directly request the normal forms to see which side has failed. In the silent session above, both queries remain silent as well, since x lacks a sort; once <x> ~ polyring is declared, as in the session of the false identity, both sides provide a response:

zelph+> ? :topoly $( (x+1)^2 )
Answer: (:topoly ((x + &1) ^ &2)) = (x poly <(pos zint &1) (pos zint &2) (pos zint &1)>)
zelph> ? :topoly $( x^2 + 1 )
Answer: (:topoly $( x ^ &2 + &1 )) = (x poly <(pos zint &1) (pos zint &0) (pos zint &1)>)

:topoly T is the same request the ≡ rule makes internally. The leading colon is zelph's shorthand for a self-fact — :topoly T is (T topoly T) — which is the standard-library idiom for "please compute this".

Exercises

  1. Prove the Lagrange identity (a²+b²)(c²+d²) − (ac+bd)² ≡ (ad−bc)². You will need to state it in the form A ≡ B; ≡ takes two terms, so move the subtraction to one side.
  2. Prove that x⁵ − 1 factors as (x−1)(x⁴+x³+x²+x+1), then use ? :topoly … to read off the normal form of each factor.
  3. ? :topoly $( 2^10 ) — what comes back, and why is it not a polynomial?
  4. Declare <x y> ~ polyring and then ask for ? :topoly $( y*x ). Now try a session where you declare <y x> ~ polyring instead. The normal forms differ. What does the declaration order mean? (Answer: Polynomial Normal Forms.)

Next

2 · Numbers from Nothing goes underneath everything used here: how &1 and &512 are represented, and how addition, multiplication and comparison are derived — in one case from a single NAND axiom.