StockholmGoteborgMeeting251029

(previous meetings)

Venue

Room Analysen, EDIT building, Chalmers campus, Göteborg

Schedule

11:40 - 12:10Anders Mörtberg
 Lunch
13:20 - 13:50TBA
14:00 - 14:30Sina Hazratpour
14:40 - 15:10Andreas Abel
 Coffee
15:50 - 17:00Discussion: what are the most important research directions and open problems in type theory? Please add your suggestions here.
18:00Dinner Andrum (map)

Anders Mörtberg: The Serre finiteness theorem formalized in Cubical Agda

Abstract:In the early 1950s Jean Pierre Serre proved a remarkable result establishing that the homotopy groups of spheres are finite, except for a few special cases. A synthetic proof in HoTT of this landmark result in algebraic topology was announced by Barton and Campion in 2022. This quickly inspired Ljungström and myself to team up with Barton and Milner at CMU to embark on an extensive project to formalize the proof in Cubical Agda. About a month ago, this formalization was finally completed.

The proof of Barton and Campion is very interesting not only as it establishes that Serre's classical result can be proved synthetically in HoTT, but also because it is fully constructive. The statement of their theorem is that all homotopy groups of spheres are finitely presented, which means that we can (in principle) compute all of them by normalizing the proof terms in Cubical Agda. The proof is also quite elementary compared to Serre's proof and its formalization was fun because it involved not only the formalization of lots of synthetic algebraic topology, but also linear algebra and diagonalization of integer matrices. In the talk I will outline the proof and discuss various simplifications that we found when formalizing it.

Sina Hazratpour: Towards a Lean4 Formalization of Gödel's Incompleteness Theorems in Arithmetic Universes

Abstract: In 1973, André Joyal gave a lecture outlining a category-theoretic proof of Gödel’s incompleteness theorems. This significant contribution was never formally published, however some lecture notes circulated informally among a very small group of category theorists. In these notes, Joyal sketched a proof of incompleteness by emulating Cantor’s diagonal argument within the initial arithmetic universe (AU). However, a precise formulation of the concept of arithmetic universe remained implicit at the time.

Years later, Maietti provided a precise formulation of AUs as list-arithmetic pretoposes and proved several important theorems about AUs using their internal language. Subsequent developments by Maietti, Vickers, and others established AUs as a suitable setting for predicative topos theory. Yet, despite these advances, Joyal’s original categorified proof of Gödel’s incompleteness theorems remained unpublished and largely inaccessible.

In this talk, I report on an ongoing project, joint with Peter Lumsdaine, to formalize Joyal’s proof using the Lean4 interactive theorem prover. Our aim is to render Joyal’s argument both explicit and formally verified, while also bringing together the scattered literature on locoses and arithmetic universes into a single, coherent digital resource.