BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Serre finiteness theorem in Cubical Agda - Axel Ljungström (U
 niversity of Nottingham)
DTSTART:20260226T170000Z
DTEND:20260226T180000Z
UID:TALK244150@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:In this talk\, I will present a recently finished computer for
 malisation project of a cornerstone result from homotopy theory: the Serre
  finiteness theorem. This theorem\, which in its simplest form states that
  homotopy groups of spheres are finitely presented\, was recently given a 
 proof entirely in the language of homotopy type theory (HoTT) by Barton a
 nd Campion. We have formalised this proof in the HoTT-based proof assistan
 t Cubical Agda. Because HoTT is a constructive language and Cubical Agda i
 s fully computational\, our formalised proof of the Serre finiteness theor
 em can be viewed as an (executable) algorithm which takes as input any hom
 otopy group of any sphere and returns a finite presentation of it. I plan 
 on giving a rough outline of the proof and its formalisation. I will also 
 discuss what problems we run into when actually trying to run our proof/al
 gorithm on a computer. Before doing any of this\, however\, I will give a 
 quick recap of the very basics of (homotopy) type theory and (Cubical) Agd
 a. This talk is based on joint work with Reid Barton\, Owen Milner\, Ander
 s Mörtberg\, and Loïc Pujet.\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting
  https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8Hb
 Y.1\n\nMeeting ID: 898 5609 1954 Passcode: ITPtalk\n\n
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR