vid_script.txt

How I made the natural number game.

Peter Johnstone taught me that 0 was {}, 1 was {{}}, 2 was {{},{{}}} and so on. But what about all the people who didn't go to that class?

Set theory is *one way of doing mathematics*.

Type theory is *another way of doing mathematics*

Naturals, integers, rationals, reals. Diophantus actually worked with positive rationals, which have a beautiful multiplicative structure: they are the free multiplicative abelian group on the primes. Similarly the positive naturals {1,2,3,4,...} (the British Natural Numbers, as I was taught at the University of Cambridge) as Patrick teaches the French in Saclay.

But when you look at a natural number in type theory b;ah blah


In mathematics, when you say "let G be a group" what you mean is that G is a set, and G has elements, and the elements are all individual "atoms", and that it is impossible to split the atom.

Building the natural number game

Think of some good targets.
2+2=4
x+y=y+x
all axioms of a commutative semiring
(e.g. x*(y+z)=x*y+x*z etc) and maybe several other natural statements (0*x=0 etc)
All axioms of a total ordering <= 
Later:
Archie Browne divisibility world all by himself
Ivan ... even_odd world

Solving 3*x+4*y=7 and 5*x+6*y=11.
Diophantus would have understood that
question and he hadn't even invented 0 yet.

We prove cancellation.

add_comm and add_assoc and then we use simp to make one tactic which can solve this. We make a term called decidable_eq and then all of a sudden we 


A theorem
Load of old nonsense.

IDeas: geometry game,