Let's Learn Lean!

Meetings will be Tuesdays 2:30-3:30pm in Avery 351. We will have a hybrid option for those who are interested but unable to attend in person. The zoom link is the same every week and will be sent in the mailing list. Ask me or Zach Norwood to be added to the mailing list; or seach for lean-learning-league on mailman and add yourself!

Find this page again easily via http://go.unl.edu/LLLs26

Upcoming

Homework for Feb 3rd: Read sections 2.1-2.3 in Ch2 of Mathematics in Lean. The meeting will going through the exercises in these sections, both answering questions and trying to do more of them. So you will probably want to do some exercises as you read, but don't feel the need to do all of them!

Additional Resources

There is supposedly a web version of lean available at https://live.lean-lang.org/. I haven't looked into it too much myself, but if anyone is interested and gets it working then we'd love for you to help people troubleshoot. (In particular, the stumbling block at which I gave up was figuring out how to get the MIL imports to work in order to get exercise S02 to be error-free).

Ayden discovered even more lean games on the same server. So you can keep playing the natural number game, or try out real analysis, set theory, or linear algebra.

Past Meetings

Jan 20th
We played the natural number game to start to get familiar with the syntax and key ideas. You can set rules to "relaxed" to skip ahead to later levels, but the goal was really just to do Tutorial World and Addition World (in particular, to mess around with induction!). We saw a mini-preview of what actual lean code would look like. We also discussed our goals for the semester: have fun, and see what doing lean "in practice" would look like! How could we code an actual small theorem? How could we contribute to the open source project? Finally, here are 17 theorems not yet formalized in lean.
Jan 27th
We made sure (almost) everyone's Lean installation is working! Troubleshooting: Make sure VSCode is up to date; Windows users it seems like it just legit takes a REALLY long time in the last "restarting the file step".Remember, a successful installation = following the instructions in Ch1 of Mathematics in Lean, namely
  • Install Lean4 itself.
  • Install VSCode (the recommended editor).
  • Clone the MIL (Math in Lean) repository to get copies of all of the exercises/demos that go along with the book.
  • Check that everything is working correctly by actually opening the S01 and S02 files in VSCode, and making sure the output in the righthand sidebar looks correct/no errors. (I had to "restart" my files by clicking the ∀ symbol above the code window and using the dropdown menu).