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 the sandwich theorem.

That last link is a link to a proof of the theorem that says that if three real-valued sequences (a_n), (b_n), (c_n) with a_n\leq b_n\leq c_n satisfy a_n\to\ell and c_n\to\ell, then b_n\to\ell. 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.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College (and beyond) trained in the art of formalising mathematics on a computer.
This entry was posted in Imperial, undergrad maths and tagged , . Bookmark the permalink.

2 Responses to Lean in LaTeX

  1. Dan Christensen says:

    I like the interactive html a lot. I guess this is the place to get it:

    https://github.com/leanprover-community/format_lean

    Like

    • xenaproject says:

      Yes! At Imperial in the maths department there are three kinds of student. (1) Those who have learnt enough about the software to actually write their own code in Lean, (2) those who aren’t interested, (3) those for whom the Lean learning curve is too steep but they don’t mind showing up and watching me write Lean. Patrick’s formatter (which he only wrote a few days ago and your link is correct) is in my mind a way to perhaps get people from type (2) into type (3), because all the first years know that they are going to have to pass an exam in analysis in May, and I think that this is an appealing way of looking at the material — at any stage in the proof you can see what you’ve proved and what you’re trying to do, in a way which I hope many mathematicians will be able to make sense of.

      Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s