BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Salvatore Mercuri (Imperial College London)
DTSTART:20260122T170000Z
DTEND:20260122T173000Z
DTSTAMP:20260420T025841Z
UID:LT2026/35
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/35/">
 A bottom-up approach to formalisation in the FLT project</a>\nby Salvatore
  Mercuri (Imperial College London) as part of Lean Together 2026\n\n\nAbst
 ract\nThis talk will describe a collaborative multi-author project to deve
 lop foundational material required for the formalisation of the proof of F
 ermat’s Last Theorem. The culmination of this project is a sorry-free pr
 oof that a certain space of automorphic cusp forms is finite-dimensional. 
 We will report on the overall status of this project\, with a particular f
 ocus on the adele ring sub-project\, as well as the ongoing efforts to ups
 tream our results to mathlib.\n
LOCATION:https://researchseminars.org/talk/LT2026/35/
END:VEVENT
END:VCALENDAR