Showing off mathlib in talks

Stream: mathlib4

[Kevin Buzzard]

tl;dr: what are people in the community doing in live lean coding sessions as part of talks for mathematicians about lean/mathlib?

---

I give talks about mathlib, and depending on the context I sometimes do live Lean coding in these talks (especially if they are of the form "look how easy it is to use a theorem prover nowadays"). I have a few options which I tend to fall back on.

• If I'm doing a school talk then I typically prove 2+2=4, either the long way (7 or so rewrites) or with rfl.

• If I'm talking to undergraduates, then, mindful of the fact that there might be plenty of first years in the room, I typically prove that composite of injectives is injective and/or composite of surjectives is surjective (you can prove composite of injectives is injective by composing the proofs of injectivity!)

• I'm giving a mathematics department colloquium then I often prove that the composite of two continuous functions is continuous.

None of these sound particularly exciting, but for each one I have some "patter" which goes around it: for example when doing composite of continuous is continuous I prove it the way we'd prove it to undergrads via a direct open set argument, and then I prove it with continuity, and then I prove it with exact?, and then I prove it in term mode (and the term mode proof is shorter than the statement) and then I jump to the library proof etc etc.

But things move on and I'd like to upgrade the list of 5-minute mathlib presentations I have. I know that Patrick has a metric space example which is really well-crafted, it even includes fixing a mistake in the paper proof involving choosing an element of a set which might be empty, and it has jokes in it too; I think I've seen him doing it live twice and it goes down really well (the second time I had to hold my tongue and not shout out "what if it's empty?" and ruin the punchline). But this example is quite long and also technical (he uses it as an introduction to the power of filters) so would not really be suitable for anything below colloquium level.

Now we have more powerful tactics like gcongr I'm going to work on a calc-based proof of AM-GM (I haven't started thinking about this yet because I'm in teaching hell until the end of Oct, but I'm back on tour again in Nov). But this is a question where I'd be really interested in community input. What have other people tried with live coding in Lean talks for mathematicians? Anything that worked great? Anything which nearly worked great and could be great after some tweaks?

[Rémy Degenne]

I used your routine about composition of continuous functions once, but changing "continuous" to "measurable" everywhere because I was talking to people familiar with probability. It was a nice illustration of how we can write tactics to generate obvious proofs (the measurability tactic in this case). I did not try anything more involved.

[Patrick Massot]

This week I needed a very elementary example and I wanted to show calc so I proved that a sum of convergent sequences is convergent. It used the calc widget, gcongr, positivity, Aesop...