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 Mar 3rd: Don't forget stuff we already know :) And just continue going through the book at our own pace. Ch2 of Mathematics in Lean.

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.

Tactics/Syntax Covered

Here's a list of the tactics & syntax that has been covered so far (or at least, as far as I've managed to type up---I'm behind!!) You can also use this as a guide to help you know what to skim/skip if you've fallen behind---if you feel comfortable with all the tactics/syntax on this list, then you can jump ahead! Things ordered roughly by when they appear

• #check: Checks the type of the input. Examples:
  #check 2+2   outputs ℕ
  #check 2+2=4   outputs Prop
• #eval compiles & evaluates the input (gets mad about sorry though). Examples:
  #eval 2+2   outputs 4
  #eval 2+2=4   outputs true
• example / theorem: An example is a theorem but unnamed & forgotten (so, once you're done with it Lean forgets all about it). A theorem gets a name and can be used inside of proofs of later results.
• by: Tells lean we're about to start a proof using tactics. Indents matter! (like python). If you don't want indents to matter, you need to use braces ({ and }) around everything after by and separate tactics by semicolons (;).
• rw: Finds the 1st instance thing that matches the desired pattern. Then rewrites ALL instances that look exactly like this first one (where first is measured in an out-to-in way?) Examples:
  rw [mul_comm]
  rw [sub_self, ← add_mul]
  rw [mul_comm a b]
If the current goal is trying to prove that a*b*c*d=a*b*c*e then rw [mul_assoc] makes the new goal into a*b*(c*d) = a*b*c*e. However, rw [mul_assoc a] makes the new goal into a*(b*c)*d=a*(b*c)*e
• nth_rw: Rewrites the nth instance. Use like rw 2 [mul_comm]
• section ... end & variable: section creates a new section. Might be useful to do this so you can also declare some variables used throughout the section, and not need to re-declare their types in each example or theorem.
• calc
• exact e and apply e: apply sees if the conclusion of e would prove our thing, then gives us the hypotheses as new subgoals. exact is the special case where we already know that e is true.
• namespace: Similar to section but need to pass in a name as input (and the same name to end it). Also, theorems named in the namespace won't exist outside it.
• variable (R : Type*) [Ring R] creates a type called R and gives it a ring structure.
• ring: Use by ring and Lean will attempt to auto-prove using the ring axioms!.
• rfl: Means "reflexive". If the proof is by definition, this will solve it! So, something like example (a b : \R) : a-b = a + -b := by refl works.
• norm_num is a tactic. I'm still kind of confused on what it's good for?
• linarith is a tactic for autosolving linear arithmetic?

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).

Feb 3rd

We started working through 2.1 and 2.2 exercises. We looked at the syntax of "have".

Feb 10th

We continued working through Ch 2 exercises.

Feb 17th

More Ch 2! We learned some subtleties about how rw works/how it chooses which instances to rewrite. Noah taught us about apply_fun, as a way to do the same thing to both sides of an equation. Here's an example that takes hypothesis h and multiplies both sides of the equation by 2:

apply_fun (fun x\mapsto 2*x) at h

Feb 24th

We learned to be careful of type signatures! lt_of_le_of_lt doesn't take any parameters, so it's illegal to try to write something like rw [lt_of_le_of_lt g h]. We can tell this because when this Theorem was originally defined, there was no forall or any parameters in the definition. It HAS to be inferred from context.