Let's Learn Lean with the UNLLLL!

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

In Fall 2026, meetings will be Mondays 2-3pm in Avery 117. Meetings are hybrid using the same zoom link every week (check 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!

The "All Levels" Lean League (aka AL aka UNLLLLAL) is open to everyone regardless of experience levels. We will do a combination of tutorials and reading through the textbook Mathematics in Lean. If you have a request for something you want to hear about in a tutorial, ask during a meeting and someone might be able to run one (or, maybe you can learn more about it and teach it to the rest of us?!).

There is also the "Leaders" Lean League (aka UNLLLLL) that meets weekly and is time for people to work on ongoing projects. Come ask about it if you are interested in joining.

Fall 2026 Schedule

No meeting on labor day!

Homework for 9/14: Install Lean! Use the instructions below. We will (hopefully) do a tutorial on "My First Proof" where we follow along with someone presenting to build a lean file with our very first proof (maybe roughly following some ideas from Ch 1 and the beginning of Ch 2 of the textbook).

Installation Instructions

Instructions to get the Mathematics in Lean project:

1. Install Lean and VS Code using the instructions here: https://lean-lang.org/install/
2. Fetch the repository by clicking on the forall symbol in the upper right corner of VS Code, and choose "Open Project", then "Download Project", and then "Mathematics in Lean".
3. Click the forall symbol in VS Code, then "Project Actions...", then "Fetch Mathlib Build Cache".
4. Click the "Restart File" button in the bottom right corner.

If you are running Windows and have antivirus software installed, then excluding the directory where the lean project is placed from scanning can speed up things a lot. As always, messing with your antivirus is something you are doing at your own risk.

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 in Spring 2026

Here's a list of SOME of the tactics & syntax covered last Spring (or at least, as far as I managed to type up!!). We will be starting back from the basics for Fall 2026, but I'll leave this list in case it is helpful to anyone. 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?

Meeting summaries from Spring 2026