Category Archives: Learning Lean
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
A word on BIDMAS
Maybe it’s not called that in other countries, but in the UK BIDMAS (which I swear was “BODMAS” when I was at school, or maybe I just went to a weird school) was the rule that was used to figure … Continue reading
Column addition
Lean has two copies of basic number types such as the naturals or integers. The reason is that Lean users might want to do two completely different things with numbers such as these. Some people might want to prove theorems … Continue reading
Learning Lean by example
I am interested in Lean for lots of reasons, and one of these reasons is that I am convinced that somehow it can be used to teach university mathematics students about proof in a new way. However I have run … Continue reading
