Generating Functions in Lean

Herman Chau, University of Washington
-
Denny Hall (DEN), 113

In this talk, we will walk through how to formalize some examples from Herbert Wilf's "generatingfunctionology". We'll see how to define and work with power series in Lean, and work our way towards proving the closed form formula for the Fibonacci numbers. Along the way, we will discuss ways to structure Lean code to be readable from a mathematician's point of view.

Event Subcalendar