Lean 4 talk of a ten minute duration?

Stream: new members

[Yan Yablonovskiy 🇺🇦]

Hey all,

I will be amongst people doing a 10 min student talk at the Australian Mathematical Sciences Institute summer school , https://ss.amsi.org.au/participant-talks-abstracts/ .

The abstract is very minimal and the title could be a bit problematic from a pedantic point of view given lean is only one potential aspect of the 'univalent foundation' of mathematics.

My goal is to proselytise about lean to larger and wider audience than just at my school, to help that ITPs are not commonly used in Australia.

10 minutes is a very short time though, any advice of the most effective way to intrigue an audience in that tiny time frame?

Currently abstract and title can be changed, and I figured this aspect of the recent Erdos problem hype would be a good way to market it.

[Michael Rothgang]

Is talking about univalent foundations something you must do? My impression is that univalence and HoTT are quite far from mathematical mainstream, and that Lean and mathlib offer enough to talk about without including them.

[Michael Rothgang]

I don't have a 10 minutes introduction to Lean in my drawer, but I can share what I do in 30 minutes' time: the first half https://www.math.uni-bonn.de/people/rothgang/slides_Potsdam2025.pdf is an intro to Lean.

[Michael Rothgang]

My selection of examples is certainly biased (to a more advanced audience), but worked well so far.

[Yan Yablonovskiy 🇺🇦]

Michael Rothgang said:

I don't have a 10 minutes introduction to Lean in my drawer, but I can share what I do in 30 minutes' time: the first half https://www.math.uni-bonn.de/people/rothgang/slides_Potsdam2025.pdf is an intro to Lean.

Thanks so much for this! And fair point on univalent foundations, I will probably deemphasize it and make it a small point as a part of an obligatory disclaimer that Lean 4 is not the only way to do ITP .

[suhr]

Lean is incompatible with HoTT. So if you really want to talk about HoTT, you need a different proof assistant.

[Chris Henson]

suhr said:

Lean is incompatible with HoTT. So if you really want to talk about HoTT, you need a different proof assistant.

It is true that there are incompatible foundations, but there are still interesting projects at the intersection of Lean and HoTT! Off the top of my head, there is HoTTLean that is aiming to make an embedded proof mode that interprets into the natural model in Lean, and Jon Sterling currently implementing a new proof assistant for HoTT in Lean.

So while it is true that directly doing HoTT in Lean is problematic, I think there is a pretty interesting story about the power of Lean in terms of metaprogramming and as a programming language and how this can interact with type theories that would normally be considered out of scope, especially given the previous support for HoTT.

All that said, given the apparent audience and time constraints, I agree with Michael that this is likely not a great fit for this particular talk.