For example, let us step through the process of proving associativity for

`a o b = (a x b) x 1`

, given the abelian group `x`

. The `| x`

in the following denotes applying the rule `x`

at the emboldened position in the equation (why yes, it *is*an AST internally):

ao(b o c) = (a o b) o c | a o b = (a x b) x 1

(a x (boc)) x 1 = (a o b) o c | a o b = (a x b) x 1

(a x ((b x c)x1)) x 1 = (a o b) o c | (a x b) x c = a x (b x c)

(ax(b x (c x 1))) x 1 = (a o b) o c | (a x b) x c = a x (b x c)

((a x b) x (cx1)) x 1 = (a o b) o c | a x b = b x a

((a x b)x(1 x c)) x 1 = (a o b) o c | (a x b) x c = a x (b x c)

(((a x b)x1) x c) x 1 = (a o b) o c | a o b = (a x b) x 1

((a o b) x c)x1 = (a o b) o c | a o b = (a x b) x 1

(a o b) o c = (a o b) o c

Oh, have the neutral element as well:

aoe(o) = a | a o b = a x b x 1

(a x e(o)) x 1=a | (a = b) = ((a x inv(x,1)) = (b x inv(x,1)))

((a x e(o)) x 1)xinv(x,1) = a x inv(x,1) | (a x b) x c = a x (b x c)

(a x e(o)) x (1xinv(x,1)) = a x inv(x,1) | a x inv(x,a) = e(x)

(a x e(o))xe(x) = a x inv(x,1) | a x e(x) = a

a x e(o)=a x inv(x,1) | (a = b) = ((inv(x,c) x a) = (inv(x,c) x a))

inv(x,a)x(a x e(o)) = inv(x,a) x (a x inv(x,1)) | (a x b) x c = a x (b x c)

(inv(x,a)xa) x e(o) = inv(x,a) x (a x inv(x,1)) | inv(x,a) x a = e(x)

e(x) x e(o) = inv(x,a)x(a x inv(x,1)) | (a x b) x c = a x (b x c)

e(x) x e(o) = (inv(x,a)xa) x inv(x,1) | inv(x,a) x a = e(x)

e(x) x e(o) = e(x)xinv(x,1) | e(x) x a = a

e(x)xe(o) = inv(x,1) | e(x) x a = a

e(o) = inv(x,1)

As you might imagine, it is not a very exciting game in its current form. One might imagine replacing the typographical symbols with mushrooms and small furry animals, and the addition of fireworks and showers of colourful jewels on the successful completion of one's proof obligations. Maybe even a fountain of

*money*.

Roam the countryside and befriend local wildlife with your awesome powers of axiomatic rigor! Bring down the castle drawbridge with a well-placed induction! Banish ghosts with the radiant aura of reductio ad absurdum!

Reducing the rest of mathematics to gameplay mechanics remains an open question.

Codewise, what I'm doing looks like this (leaving out all the hairy bits):

type Op = String

data Expr = Expr (Op, Expr, Expr)

| A | B | C

| Inv (Op, Expr)

| Neutral Op

| Literal Int

type Pattern = Expr

type Substitution = Expr

data Rule = Rule (Pattern, Substitution)

type CheckableRule = ((Rule -> Bool), Rule)

isTrue :: Rule -> Bool

isTrue (Rule (a,b)) = a == b

isBinding :: Expr -> Rule -> Bool

isBinding e (Rule (a,b)) = e == a || e == b

opf :: Op -> Expr -> Expr -> Expr

opf op a b = Expr (op, a, b)

{-

Group axioms main stage:

Stability: a o b exists in G for all a, b in G

Magma!

Associativity: a o (b o c) = (a o b) o c

Semigroup!

Neutral element: a o 0 = 0 o a = a

Monoid!

Inverse element: a o a_inv = a_inv o a = 0

Group! Enter Abelian bonus stage!

-}

type CheckableRule = ((Rule -> Bool), Rule)

checkCheckableRule :: CheckableRule -> Bool

checkCheckableRule (p, rule) = p rule

associativity :: Op -> CheckableRule

associativity op = (isTrue, (A `o` (B `o` C)) `eq` ((A `o` B) `o` C))

where o = opf op

rightNeutral :: Op -> CheckableRule

rightNeutral op = (isBinding (Neutral op), (A `o` Neutral op) `eq` A)

where o = opf op

leftNeutral :: Op -> CheckableRule

leftNeutral op = (isBinding (Neutral op), (Neutral op `o` A) `eq` A)

where o = opf op

rightInverse :: Op -> CheckableRule

rightInverse op = (isBinding (Inv (op, A)), (A `o` Inv (op, A)) `eq` Neutral op)

where o = opf op

leftInverse :: Op -> CheckableRule

leftInverse op = (isBinding (Inv (op, A)), (Inv (op, A) `o` A) `eq` Neutral op)

where o = opf op

{-

Abelian bonus stage:

Commutativity: a o b = b o a

Abelian group! Enter ring bonus stage!

-}

commutativity :: Op -> CheckableRule

commutativity op = (isTrue, (A `o` B) `eq` (B `o` A))

where o = opf op

magma op = [] -- FIXME?

semiGroup op = magma op ++ [associativity op]

monoid op = semiGroup op ++ [rightNeutral op, leftNeutral op]

group op = monoid op ++ [rightInverse op, leftInverse op]

abelianGroup op = group op ++ [commutativity op]

{-

Ring bonus stage:

Show bonus function to be a semigroup!

Distributivity of x over o:

a x (b o c) = (a x b) o (a x c)

(a o b) x c = (a x c) o (b x c)

Pseudo-ring!

-}

leftDistributivity :: Op -> Op -> CheckableRule

leftDistributivity opO opX = (isTrue, (A `x` (B `o` C)) `eq` ((A `x` B) `o` (B `x` C)))

where o = opf opO

x = opf opX

rightDistributivity :: Op -> Op -> CheckableRule

rightDistributivity opO opX = (isTrue, (A `x` (B `o` C)) `eq` ((A `x` B) `o` (B `x` C)))

where o = opf opO

x = opf opX

{-

Neutral element for x: a x 1 = 1 x a = a

Ring!

Commutativity for x: a x b = b x a

Commutative ring! Enter field bonus stage!

Field bonus stage:

Inverse element for x in G: a x a_inv = a_inv x a = 1

Field! Superior! Shower of jewels!

-}

pseudoRing o x = abelianGroup o ++ semiGroup x ++

[leftDistributivity o x, rightDistributivity o x]

ring o x = pseudoRing o x ++ [rightNeutral x, leftNeutral x]

commutativeRing o x = ring o x ++ [commutativity x]

field o x = commutativeRing o x ++ [rightInverse x, leftInverse x]