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
Xena 