I gave an hour long talk at the NU Math Club yesterday about Lean and theorem proving.

Things that went well

It was fun to talk about Lean and to show examples. The most fun bit was playing with the Lean Chat plugin for VS Code, which has gotten quite good now.

Things that did not go well

It was a bit tedious to talk about Type Theory. I need to find better ways to motivate and explain Type Theory, especially the significance of constructors. I could do examples from Haskell or Lean to just show the thing in action.

I could have just skipped the type theory bit completely and just spent the entire time talking about Lean and perhaps doing an example from scratch.

To Do

As I was preparing for the talk, I came across this blog post and the associated paper by FacebookAI which claims to have made improvements in AI assisted theorem proving. I need to read more about it.

I also need to find some expository texts on Type Theory, especially about the Type Theory used in Lean.

Connections:: [[2022/11/Northwestern]]