You are here

Generating Functions in Lean

Herman Chau, University of Washington
Monday, May 20, 2024 - 1:00pm to 2:20pm
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.

People Involved: 
Event Subcalendar: