Category Archives: undergrad maths
Mathematics in type theory.
An explanation of how to set up mathematics using universes, types, and terms Continue reading
The complex number game
The complex number game, and the Xena Project’s first steps into Twitch and Discord. Continue reading
Xena Project Thursday meetings start with talk tomorrow 21st May
The Complex Number Game — proving basic stuff about the complexes in Lean Continue reading
Summer projects 2020
Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading
The invisible map
Is a subgroup of a group a group? Is 3 a topology on 2? Is a natural number a real number? Decisions like this have consequences. Continue reading
Where is the fashionable mathematics?
A challenge to the users of all the computer proof systems to do some modern mathematics. Continue reading
My algebraic geometry course
The union of two affine algebraic sets is an affine algebraic set. Continue reading
Lean has real manifolds!
Lean has real manifolds — and tangent bundles too! Continue reading
The natural number game — an update
I just pushed an update to the natural number game. I’m rather pleased with how this has all worked out. I started off thinking it was kind of a game, but the explanations turned out so wordy and now I … Continue reading
Chalkdust, and the natural number game!
Ever wanted to prove x+y=y+x but couldn’t be bothered to download and install a computer theorem prover? Well now you can! Continue reading
Xena 