Category Archives: M1P1
Formalising mathematics : workshop 3 — sequences and limits
This week we’re going to do limits of sequences, of the kind you see in a 1st year analysis course. These are great fun to do in Lean. Because of Rob Lewis’ linarith tactic (which does the “and now this … Continue reading
Posted in formalising mathematics course, M1P1, undergrad maths
1 Comment
Xena 