NASC Seminar: LeanFun: formalised, verified spectral methods and the trouble with numerics in Lean
| Dates: | 23 October 2026 |
|---|
| Times: | 12:00 - 13:00 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Mathematics |
|---|
| Who is it for: | University staff, Current University students |
|---|
| Speaker: | Timon Gutleb |
|---|
|
|
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.
Speaker
Timon Gutleb
Organisation: University of Leeds
Travel and Contact Information
Find event
Frank Adams Room 1
Alan Turing Building
Manchester
