# 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