Generating Functions in Lean

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.