Forgotten Computer Proofs

When I was working on my masters thesis I got really interested in using computers to prove things.

An important part of my thesis hinged on discovering a super-commutative ring that did not have a super divided power structure. In my thesis I present a whole class of rings that have that property, one ring for each prime number. However, before I figured out the proof that it worked for every prime, I used a computer to prove that it worked for the number 3. That work has never been published. Until today.

Super Duper Example

In order to do that, I built a mini-algebra system using the Miranda programming language.

p = 3
monomial ::= Mon (num,[char]) ||A monomial is a number followed by a (possibly empty) list of variables represented by characters
 ||A polynomial is just a list of monomials

highcount :: [*] -> num ||finds the number of the most plentiful element in a list
highcount [] = 0
highcount (a:x) = (1 + #[b | b <- x; b = a]), if ((1 + #[b | b <- x; b = a]) >= highcount (x -- [b | b <- x; b = a]))
 = highcount (x -- [b | b <- x; b = a]), otherwise

fact :: num -> num ||input n -> output n factorial
fact 0 = 1
fact (n+1) = ((n+1)*(fact n))

clt :: [monomial] -> [monomial] ||takes a sorted polynomial and "collects like terms"
clt [] = [] ||If polynomial is 0 (an empty list), return 0
clt (a:[]) = (a:[]) ||If polynomial is a monomial return it
clt ((Mon(a, astr)):(Mon(b, astr)):x) = clt ((Mon((a+b) mod p, astr)):clt (x))
 ||If the first two monomials in the polynomial have the same variables
 ||add them together by adding their coefficiants. (You see why "sorted" is important)
clt (a:x) = a:(clt x) ||If they don't have the same variables then move on to the rest of the list

remo :: [monomial] -> [monomial] ||removes zeros to clean up polynomials
remo [] = []
remo (Mon(a, astr):x) = remo x, if ((a=0) \/ ((highcount astr) >= p)) || KILL ALL POWERS OF P! (powers of p are zero)
remo (Mon(a, astr):x) = (Mon(a, astr)):(remo x), otherwise

monsort :: [monomial] -> [monomial] ||puts polynomials in alphabetical order, so collecting like terms is easier.
monsort [] = []
monsort (Mon(a,astr):x) = monsort [ Mon(b,bstr) | Mon(b,bstr) <- x; bstr <= astr ]
 ++ [Mon(a,astr)] ++
 monsort [ Mon(b,bstr) | Mon(b,bstr) <- x; bstr > astr ]

polysan :: [monomial] -> [monomial] ||sanitises polynomials
polysan x = remo(clt(monsort(x)))

mult :: monomial -> monomial -> monomial ||multiplies monomials
mult (Mon (a, astr)) (Mon (b, bstr)) = (Mon ( (a*b) mod p, (sort(astr++bstr))))

scalmult :: num -> monomial -> monomial ||multiplies monomials and scalars
scalmult n (Mon(a, astr)) = (Mon((n*a) mod p, astr))

polyscalmult :: num -> [monomial] -> [monomial] ||multiply polynomials by scalars
polyscalmult n x = (map (scalmult n) x)

polyadd :: [monomial] -> [monomial] -> [monomial] ||adds polynomials. note: 0 = []
polyadd x y = polysan (x++y)

polymul :: [monomial] -> [monomial] -> [monomial] ||multiply polynomials. note 1 = Mon (1,[])
polymul x [] = []
polymul [] y = []
polymul (a:x) y = (polyadd (map (mult a) y) (polymul x y))

power :: ([monomial], num) -> [monomial] ||exponetiates polynomials
power (x,0) = [Mon (1,[])]
power (x,1) = x
power (x,n+1) = (polymul x (power (x, n)))

repeater :: num -> * -> [*] ||outputs a list of the input repeated a bunch of times
repeater 0 x = []
repeater 1 x = [x]
repeater k x = (x:(repeater (k-1) (x)))

gammamon :: num -> monomial -> monomial ||gamma on a monomial
gammamon 0 x = Mon (1, []) ||Rule 1
gammamon 1 x = x ||Rule 1
gammamon k (Mon (l, a:[])) = Mon (l^k * ((fact k)^(p-2) mod p) mod p, repeater k a) ||What gamma does on the generators.
gammamon k (Mon (l, a:x)) = mult (Mon (1,repeater k a)) (gammamon k (Mon (l, x))) ||Rule 3

sigma :: (num, num) -> ( num -> [monomial]) -> [monomial] ||adds incremental functions (used to implement rule 2.)
sigma (i, k) func = [Mon(0,[])] , if i > k
sigma (i, k) func = polysan ((func i) ++ (sigma (i+1,k) func)) 

gamma :: num -> [monomial] -> [monomial]
gamma 0 x = [Mon (1,[])] ||Rule 1
gamma 1 x = x ||Rule 1
gamma k [] = [] ||gamma(0) is 0
gamma k (x:[]) = polysan [gammamon k x] ||gamma of a monomial goes to gammamon
gamma k (x:y) = polysan (sigma (0, k) (gammaprod [x] y k)) ||Rule 2

||Things to test.

|| Rule 4
test1 i j x = (polysan (polymul (gamma i x) (gamma j x)) = polysan (polyscalmult (((fact (i+j)) div ((fact i)*(fact j))) mod p) (gamma (i+j) x)))

|| Rule 5
test2 i q x = (polysan (gamma i (gamma q x)) = polysan (polyscalmult (((fact (i*q)) div ((fact i)*(fact q)^i)) mod p) (gamma (i*q) x)))

test i j x = (test1 i j x) & (test2 i j x)

gammaprod :: [monomial] -> [monomial] -> num -> num -> [monomial] || used to implement rule 2.
gammaprod x y k 0 = gamma k y ||gamma 0 x = 1
gammaprod x y k k = gamma k x ||gamma 0 y = 1
gammaprod [] y k i = [] ||0*stuff = 0
gammaprod x [] k i = [] ||stuff*0 = 0
gammaprod x y k i = polymul (gamma i x) (gamma (k-i) y)

write :: [monomial] -> [char] ||outputs polynomials so they can be read by other programs
write [] = "0\n"
write (Mon(a,astr):[]) = (show a) ++ "*" ++ (condence(astr)) ++ ['\n']
write (Mon(a,astr):rest) = (show a) ++ "*" ++ (condence(astr)) ++ " + " ++ (write rest)

stars :: [char] -> [char]
stars [] = []
stars (a:[]) = (a:[])
stars (a:rest) = [a] ++ "*" ++ (stars(rest))

condence :: [char] -> [char] ||takes a string and writes it in exponent form, ex: "aaabb"-> "a^3*b^2"
condence [] = []
condence (a:[]) = (a:[])
condence (a:rest) = a:'*':(condence rest), if ([ b | b <- rest; b=a] = [])
 = [a] ++ "^" ++ (show (1 + #[ b | b <- rest; b=a])) ++ "*" ++ (condence (rest -- [ b | b <- (rest); b=a])), 
 if ~((rest -- [ b | b <- (rest); b=a])= [])
 = [a] ++ "^" ++ (show (1 + #[ b | b <- rest; b=a])), otherwise

||some variables

a = [Mon (1, "a")]
b = [Mon (1, "b")]
c = [Mon (1, "c")]
d = [Mon (1, "d")]
f = [Mon (1, "f")]
g = [Mon (1, "g")]
rel = [Mon (1,"ab"),Mon (1, "cd"),Mon (1, "ef")]
rel1 = [Mon (-1,"ab")]
rel2 = [Mon (1, "cd"),Mon (1, "ef")]
rel3 = [Mon (1, "cd"),Mon (1, "ef"), Mon (1, "gh")]

When I tried to run the problem for the number 5 it crashed my laptop.



The Story of ‘X’

One of my favourite anecdotes from my days teaching in an English secondary school involves the variable x. I was introducing the concept of a linear equation. Specifically the y=mx+b that kids in Ontario learn all about in Grade 9.
I was explaining how you plot the line on a graph when a young boy got out of his chair threw his hand up and toward the board, palm open, indicating with a wild gesture the third last letter of the alphabet written plainly in the equation. “But Sir!” he exclaimed, “What Is X!”
For my students, up until this point a letter had represented some unknown quantity, and it was their responsibility to divine its value. To Solve For X! But this was a new concept. In y = 2x + 1, x isn’t a quantity to solve; it’s a variable, a symbol of all the possible numbers to which we could multiply by 2 and add 1. I was amused and did my best to explain the nuanced differences of this new concept masquerading as an old familiar one.
But how did X become the symbol of anything in the first place? Who was the mystery person who decided that we needed to use letters to represent numbers?
His name was François Viète.

François Viète

Continue reading

The History of X


Al-Khwārizmī on a 1983 Soviet Union postage stamp celebrating his 1200th birthday. 

When al-Khwārizmī codified algebra he made a bunch of algorithms to find unknown quantities. The problems were expressed in everyday language as you can see in this example taken from an 1831 translation of his work.

“two squares and ten roots are equal to forty-eight dirhems; that is to say, what must be the amount of two squares which, when summed up and added to ten times the root of one of them, make up a sum of forty-eight dirhems? You must at first reduce the two squares to one; and you know that one square of the two is the moiety of both. Then reduce every thing mentioned in the statement to its half, and it will be the same as if the question had been, a square and five roots of the same are equal to twenty-four dirhems; or, what must be the amount of a square which, when added to five times its root, is equal to twenty-four dirhems? Now halve the number of the roots; the moiety is two and a half. Multiply that by itself; the product is six and a quarter. Add this to twenty-four; the sum is thirty dirhems and a quarter. Take the root of this; it is five and a half. Subtract from this the moiety of the number of the roots, that is two and a half; the remainder is three. This is the root of the square, and the square itself is nine.”

As I’m sure you see from the above paragraph, using common language to explain math problems could be tedious and time consuming.
To compare, here is a translation into our modern symbolic algebra.


Look how far we’ve come.

900 factor lattice


900 factor lattice

I’ve been experimenting with the representations of factor lattices. Factor lattices are great for demonstrating a deep understanding of the multiplicative relationships between whole numbers.
Pick a number in the lattice above. If you travel anywhere in a northern or eastern direction you will find the multiples of your number, all the way to 900. If you travel in a southern or western direction you will find the factors of your number, all the way down to 1.
The real trick is designing them so that each row of numbers is increasing from the top left to the bottom right. It isn’t always easy to do.


H OM E OMOR PH ISM Dome A/V Performance

Topology is the mathematics of the shapes of bendy spaces. In topology two spaces are said to be homeomorphic if there is a continuous smooth transformation of one space to the other. However, “space” doesn’t need to follow your intuitive notions of space. A computer can take a space made up of zeros and ones and transform it into this performance by Ouchhh. (In fact that is what yours is doing when you watch this video.)