Category Archives: M1P1

Formalising mathematics : workshop 3 — sequences and limits

Posted on February 4, 2021 by xenaproject

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