NASC Seminar: LeanFun: formalised, verified spectral methods and the trouble with numerics in Lean

About

Speaker: Timon Gutleb (Leeds) Abstract: LeanFun is an experimental project to formalise orthogonal polynomials, special functions and the mathematics underlying spectral methods in Lean. Its goal is to develop a reusable foundation for methods found in software such as Chebfun and ApproxFun, alongside a readable mathematical reference connecting familiar formulas to machine-checked statements and proofs. This talk introduces the project and its background, including a brief overview of Lean and its mathematical library, Mathlib. I will discuss the mathematical and practical challenges of translating numerical analysis into formal mathematics: choosing definitions, preserving classical meaning, organising interconnected theories, and making the results actually useful to mathematicians and students. Examples from special functions and orthogonal polynomials will illustrate both the progress so far and the work ahead.