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 the sandwich theorem.
That last link is a link to a proof of the theorem that says that if three real-valued sequences with satisfy and , then . If you click on a line in the proof then it opens up the Lean code (which is probably incomprehensible if you don’t know any Lean) but the beauty is that if you then click on one of the grey rectangles either side of that line of Lean code then you get to see the tactic state, which a mathematician might well find easy to understand because it is written in standard mathematical language. This way a mathematician who does not know any Lean can still step through the formal proof, and can figure out how to get from each line to the next themselves, because each individual step is typically very short.
Ultimately this means that we can write formally-verified course notes for the Imperial analysis course which the first year undergraduates are currently attending, and the notes could be of use even to students who do not know the technicalities of how to use Lean and do not have Lean installed on the computers they have access to.