Tag Archives: M1P1

Lean in LaTeX

Patrick Massot wrote a formatter, which can turn Lean code into beautiful LaTeXxy html. The undergraduates and I have been formalising Imperial’s first real analysis course M1P1 in Lean. Put them together and you get a 21st century proof of … Continue reading

Posted in Imperial, undergrad maths | Tagged , | 2 Comments