This is an old revision of the document!
Table of Contents
Spring 2026 Meeting Schedule
All meetings take place on Wednesdays, 2:30 - 3:30 pm in Burt Hall 204 unless otherwise noted.
| Date | Meeting Title | Speaker | Abstract |
|---|---|---|---|
| February 4 | Getting L∃∀N | Nathan Albin | Abstract |
| February 11 | |||
| February 18 | |||
| February 25 | |||
| March 4 | |||
| March 11 | |||
| March 18 | NO MEETING | Spring Break | |
| March 25 | |||
| April 1 | |||
| April 8 | |||
| April 15 | |||
| April 22 | |||
| April 29 | |||
| May 6 |
Abstracts
February 4
“Getting L∃∀N”, Nathan Albin
This semester, I've decided it's time to learn to use the programming language (and interactive theorem prover) Lean (lean-lang.org). To support this goal, I'm planning to lead informal demonstrations and discussions at a few NODE meetings. This will be the first of those. I'm about as far from being an expert as one can get, but I'll show you the ε > 0 that I've learned thus far. In keeping with the unofficial acronym NODE = Nathan Often Does Examples, I'll work through some constructions and proofs using “easy” structures like the natural numbers, and we can explore questions as they arise. I may get to the point of proving the handshaking lemma in graph theory. If not, that will be for a future installment. Eventually, I'll be proving things about p-modulus with an AI assistant.