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.
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.
February 4
“Getting L∃∀N”, Nathan Albin
Continuing with the Lean theme, I'll start from an empty Lean file and show how to use inductive types to construct the natural numbers from scratch and how to prove theorems about them. It's also a good time to talk about the Curry–Howard isomorphism, which establishes the link between logic and computation. You'll often see this summarized as “propositions are types, proofs are programs.” This means proof-checking is really just type-checking in disguise. I find this dual view incredibly helpful; if I get stuck thinking about a logical implication, I can switch to thinking about writing a function with a specific type signature.