BEGIN:VCALENDAR
PRODID:-//Columba Systems Ltd//NONSGML CPNG/SpringViewer/ICal Output/3.3-
 M3//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VEVENT
DTSTAMP:20261019T081853Z
DTSTART:20261023T110000Z
DTEND:20261023T120000Z
SUMMARY:NASC Seminar: LeanFun: formalised\, verified spectral methods and
  the trouble with numerics in Lean
UID:{http://www.columbasystems.com/customers/uom/gpp/eventid/}ed2-mvezfv7
 9-n8psa3
DESCRIPTION:Speaker: Timon Gutleb (Leeds)\n\nAbstract: LeanFun is an expe
 rimental 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 Che
 bfun and ApproxFun\, alongside a readable mathematical reference connect
 ing familiar formulas to machine-checked statements and proofs.\nThis ta
 lk introduces the project and its background\, including a brief overvie
 w of Lean and its mathematical library\, Mathlib. I will discuss the mat
 hematical and practical challenges of translating numerical analysis int
 o formal mathematics: choosing definitions\, preserving classical meanin
 g\, 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.\n
STATUS:TENTATIVE
TRANSP:TRANSPARENT
CLASS:PUBLIC
LOCATION:Frank Adams Room 1\, Alan Turing Building\, Manchester
END:VEVENT
END:VCALENDAR