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 b . . . Read more