Lean for the not very curious mathematician

Stream: new members

[Martin C. Martin]

I met an old friend recently, who is a Math professor at a teaching college. He had heard of theorem proving computer programs, but not of Lean. What can I point him to, to show him some of the flavor of ITPs in general, or Lean in particular? "Lean for the curious mathematician" is a conference, and I assume he doesn't want to invest that much time. The natural numbers game comes to mind, but he's not a gamer so terminology like "boss level" might turn him off. Also, it makes it seem like ITPs are for foundations of mathematics level stuff, not even high school or early undergrad level math.

Is there something else I can point him to? There are some Quanta magazine articles, but those are very high level and vague to a mathematician, I would assume.

[Shreyas Srinivas]

You could show him the mathematics in lean book

[Jireh Loreaux]

#mil is great. I think for a nice video that showcases some nontrivial things happening in Lean in a demo, Heather Macbeth's 2022 LftCM ICERM talk is excellent: https://icerm.brown.edu/video_archive/?play=2896, with the only downside in my mind being that it happened in Lean 3.