Tue 18 Jan 2022 17:45 - 18:10 at Salon III - Category Theory, HoTT, Number Theory Chair(s): Kuen-Bang Hou (Favonia)

The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence ``proof from the Book''. Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.

Talk slides (windmills_slides.pdf)827KiB

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:30 - 18:10
Category Theory, HoTT, Number TheoryCPP at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
16:30
25m
Talk
Implementing a category-theoretic framework for typed abstract syntaxRemote
CPP
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University
DOI Pre-print Media Attached
16:55
25m
Talk
(Deep) Induction Rules for GADTsRemote
CPP
Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of Technology
Pre-print Media Attached
17:20
25m
Talk
On homotopy of walks and spherical maps in homotopy type theoryRemote
CPP
Jonathan Prieto-Cubides University of Bergen
Pre-print Media Attached
17:45
25m
Talk
Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote
CPP
Hing Lun Chan Australian National University
DOI Pre-print Media Attached File Attached