Category Archives: Learning Lean

Quadratic Reciprocity and (p^2-1)/8

The law of quadratic reciprocity. The jewel in the crown of mathematics! Still not proved in Lean! Clara List and Sangwoo Jo were thinking about this today. They formalised the statement. There are two “supplements” to the law, describing when … Continue reading

Posted in Learning Lean, number theory | 1 Comment


The problem This post is about the equation . This special case of the binomial theorem is the sort of thing that we would expect incoming students at my university to know, or at least to be able to compute … Continue reading

Posted in General, Learning Lean, tactics | Leave a comment

Group Theory revision

To all Imperial students — welcome back and good luck in your exams. I was looking at the axioms for a group in Lean today. If you fire up Lean and type #print group (e.g. by clicking here and then … Continue reading

Posted in Learning Lean | Leave a comment

Mini-tutorial : Currying.

A couple of mathematics undergraduates have asked me about this recently. Currying is something which is important in computer science, but is based on a fact which is trivial mathematically. As it’s not hard to see, → is not associative. … Continue reading

Posted in Learning Lean | Leave a comment

Working with integers

The integers. Lean has integers inbuilt as part of the core library. You can call them int if you want to be old skool, but if you type \Z (and then hit the space bar) in VS Code or emacs … Continue reading

Posted in Learning Lean | 1 Comment

Building the non-negative integers from scratch

It’s not actually that hard to build the non-negative integers from scratch in Lean. Let’s call them xnat, because Lean already has an inbuilt nat. The code just looks like this: inductive xnat | zero : xnat | succ : … Continue reading

Posted in Learning Lean | 3 Comments

Rational powers

Lean’s core library has no support for rational or real numbers 😦 They are however in the maths library — or we can just make some fake real numbers and use them instead. — let’s define the real numbers to … Continue reading

Posted in Learning Lean, M1F | Leave a comment