Thursday 17 November 2022, 17:00, room 3U42 and online: Lean in Practice as a Theorem Prover and Functional Programming Language, Rishikesh Vaishnav (San Diego University master student) [the speaker will be online].

Lean is a theorem prover and functional programming language whose type theory is heavily inspired by Coq and whose style follows that of Haskell. In this talk, I will describe my experience with Lean as both an interactive theorem prover for formalizing mathematics and as a tool for general-purpose functional programming, and the seamless interface it provides between these two domains. I will start by discussing the basics of Lean's type system, in particular how it handles inductive types, inductive proofs, type universes and propositions, and how it uses a few foundational axioms to implement a representation of certain undecidable propositions in classical logic. I also will discuss my foray into the formalization of the foundations of Bayesian probability theory in Lean 3 that I have done as part of my Master's thesis, and my more recent experience programming in Lean 4 for the past several months at Yatima, work that involved writing an independent typechecker for Lean based on the typed normalization-by-evaluation algorithm.