# Category Archives: Learning Lean

## Summer projects 2020

Undergraduate mathematician? Not much to do in July and August? Come and work with me! Continue reading

## No errors.

Does your Lean file contain errors? Try and cut down. 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

## Prove a theorem. Write a function.

New maths PhD students Lambert A’Campo and Ashvni Narayanan have proved that a normed real vector space with compact unit ball is finite-dimensional in Lean! [update added a few days later: ROFL Sébastien Gouëzel on the Lean chat complained that … 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

## The inverse of a bijection.

Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading

## Equality part 2: syntactic equality

Syntactic equality is yet another kind of equality. I am beginning to learn why it matters. Continue reading

## Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until … Continue reading