Return to Colloquia & Seminar listing
Predicate logic in dependent type theory
Student-Run Research Seminar| Speaker: | Colby Brown, UC Davis |
| Location: | 2112 MSB |
| Start time: | Wed, Apr 23 2025, 12:10PM |
Proof formalization and assistive proof writing software are in vogue. Lean, rapidly gaining widespread adoption as the defacto standard, is based on the theory of dependently typed lambda calculi. In this talk, we will introduce the type system used in Lean, derive a model for predicate logic, and showcase what it really means to "prove" a mathematical statement in Lean. No previous background in type theory, Lean, or programming needed.