Return to Colloquia & Seminar listing
A Short Proof that 0 ≠ 1
Student-Run Research Seminar| Speaker: | Colby Brown, UC Davis |
| Location: | 2112 MSB |
| Start time: | Wed, May 14 2025, 12:10PM |
Lean is a proof assistant programming language capable of encoding most of modern research mathematics. Yet, it is based on a dependently typed lambda calculus, which is generally not powerful enough to even prove that zero and one are distinct natural numbers. In this talk, we will use the construction of the natural numbers as a springboard for investigating generalized induction principles on arbitrary inductive types, culminating in a (somewhat) short proof that zero and one are distinct. This is a sequel to my previous talk, "Predicate Logic in Dependent Type Theory", but no logical dependency is assumed, so we will review all necessary material.
Free pizzas as always:)