Formal proof and synthetic mathematics

Heidelberg University, 24-25-26 June 2026

An illustration of the elimination rule for the existential quantifier, where the space of witnesses and evidence is represented as a bundle with contractible fibres.

Goal

Martin-Löf Type Theory provides a powerful syntax in which to express mathematical concepts and formalise them in a programming language. Combined with homotopy theory, it also provides a geometric framework for proof theory that is both intuitive and helpful. The goal of this workshop is to present an introduction to these topics for mathematicians, emphasising the type-theoretic aspects and the synthetic approach.

Registration deadline: 24 May 2026 (Registration form).

Lecturers

Speakers

Schedule

The workshop will consist of two lecture series (3 x 1h) and six research talks (1h).

Outline
Wednesday 24.06 Thursday 25.06 Friday 26.06
09:30-10:30 Paige North (1) Paige North (2) Felix Cherubini (3)
Coffee break Coffee break Coffee break
11:00-12:00 Milly Maietti Felix Cherubini (2) Paige North (3)
Lunch break Lunch break
13:30-14:30 Felix Cherubini (1) Hugo Moeneclaey
Coffee break Free afternoon Coffee break
15:00-16:00 Tom de Jong Meven Lennon-Bertrand
16:15-17:15 Gabriella Clemente Fernando Chu

Rooms

All talks will take place in the Mathematikon (Building 205 of the Neuenheimer Feld Campus).

  • Wednesday 24.06 (09:30-12:00): Conference Room 5/104 (5th floor).
  • Wednesday 24.06 (13:30-17:15) : Lecture Hall (Hörsaal, ground floor).
  • Thursday 25.06: Seminar Room A (ground floor).
  • Friday 26.06: Conference Room 5/104 (5th floor).

Program

Lectures

The definition of the basic objects of algebraic geometry, schemes, requires a stack of notions that has to be unfolded and reconstructed a lot. In Synthetic Algebraic Geometry (SAG), a scheme is just a set with a property and morphisms of scheme are just functions of sets.

To make this work, we introduce three axioms, which are incompatible with the axiom of choice. One of the axioms, called Zariski-local choice (ZLC), introduces a new choice principle related to the Zariski-topology, which relates affine schemes to objects which are not sets, but higher types. We have access to the latter by reasoning in homotopy type theory.

We will give an introduction to the constructive algebra needed in SAG and present the axioms of SAG. With the axioms, we will define schemes and construct basic examples. We will show the role of ZLC in making basic topological properties of schemes work and finally show the original motivation behind ZLC: Higher types can be used to define cohomology groups of schemes and with ZLC it is possible to recompute classical results without the usual technicalities.

The Equivalence Principle is an informal principle asserting that equivalent mathematical objects have the same properties. For example, group theory has been developed so that isomorphic groups have the same group-theoretic properties, and category theory has been developed so that equivalent categories have the same category-theoretic properties (though sometimes other, ‘evil’ properties are considered). Vladimir Voevodsky established Univalent Foundations (also known as homotopy type theory) as a foundation of mathematics (based on dependent type theory) in which the Univalence Principle, and thus the Equivalence Principle, for types (the basic objects of type theory) is a theorem. Later, versions of the Equivalence Principle for set-based structures such as groups and categories were shown to be theorems in Univalent Foundations.

In joint work with Ahrens, Shulman, and Tsementzis, we formulate and prove versions of the Equivalence Principle for a large class of categorical and higher categorical structures in Univalent Foundations. Our work encompasses (higher) categorical structures such as bicategories, dagger categories, opetopic categories, and more.

The Equivalence Principle in Univalent Foundations rely on the fact that the basic objects – the types – can be regarded as spaces. That is, Univalent Foundations can be viewed as an axiomatization of homotopy theory and as such is closely related to Quillen model category theory. Univalent Foundations can also be viewed as a foundation of mathematics based not on sets, but on spaces. It is the homotopical content of this foundation of mathematics that allows us to prove something like the Equivalence Principle, something which is not possible in set-based foundations of mathematics, such as ZFC.

I will begin the lecture series with a whirlwind introduction to Univalent Foundations, and then continue on to explain how we can prove the equivalence principle in it for various structures. If time allows, I will also talk about work to develop an extension of Univalent Foundations in which the basic objects are not spaces but higher categories.

Talks

In the first part of this talk, I will present the 1-groupoid model of MLTT. This model validates a restricted version of the univalence axiom, which can be used to develop 1-groupoid theory synthetically. The relation to the ∞-groupoid model of HoTT will be briefly sketched. In the second part of the talk, I will motivate Directed Type Theory as a language for developing category theory synthetically and sketch some work in progress (joint work with Paige R. North) in this direction https://arxiv.org/abs/2602.17480.

Synthetic differential geometry (SDG) is an axiomatic version of differential geometry, whose context is a smooth topos instead of the category of smooth manifolds. After covering the basics of SDG, I will talk about recent developments in synthetic differential calculus from the joint work https://hal.science/hal-05555752/document. I will then discuss smooth toposes through examples of well-adapted models, as well as work in progress in the area that is a collaboration with Riccardo Brasca and Joël Riou. Time permitting, I will explain some of the peculiarities of formalizing SDG in Lean.

I will explain how we can develop homotopy theory synthetically in homotopy type theory (HoTT). As a particular example, I will focus on epimorphisms, characterizing these via suspensions, and present examples and applications in group theory via the identification of groups with certain higher types.

This is based on a paper with Ulrik Buchholtz and Egbert Rijke: Epimorphisms and Acyclic Types in Univalent Foundations. In: The Journal of Symbolic Logic (2025), pp. 1–36. doi: 10.1017/jsl.2024.76.

In the synthetic viewpoint on type theory, one works inside a particular type theory, whose rules capture the features of the mathematical objects of interest. However, type theory itself can be studied as a mathematical object in its own right. This is necessary to formally explain how the synthetic language relates to the objects it is intended to capture, but is more generally a rich field of mathematical investigations. My talk will be an introduction to these investigations.

I will present Generalised Algebraic Theories, one of the most popular formal definition of what a type theory is; introduce the closely related notions of Categories with Families and Natural Models, two standard ways of capturing when a given structure can interpret a type theory; and explain how one can think of syntax formally in this setting. Time allowing, I might also talk a bit about how all of this relates to proof assistant implementation.

Dependent type theories, such as Martin-Löf Type Theory and Homotopy Type Theory, have provided a solid basis for the development of formal mathematics, that is, mathematics formalized within proof assistants.

In this talk, based on recent results in [1,4], we describe some principles that distinguish Martin-Löf Type Theory and Homotopy Type Theory within the landscape of foundations of mathematics, and in particular within constructive mathematics. Our analysis is carried out by referring to a third foundation, called the Minimalist Foundation, developed in [2,3] as a common core underlying the main foundational systems for mathematics.

These distinguishing principles include certain forms of choice axioms, as well as computability and continuity principles.

[1] Contente, M. and Maietti, M. E. , “The Compatibility of the Minimalist Foundation with Homotopy Type theory.” , Theoretical Computer Science, vol. 991, p. 114421, 2024

[2] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides, p. 91-114. OUP (2005)

[3] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319{354 (2009)

[4] M. E. Maietti, P. Sabelli, and D. Trotta. Effectiveness and continuity in intuitionistic quasi-toposes of assemblies. Mathematical Structures in Computer Science, vol 36, 2026

In this talk we will give an overview of the machinery which was developed during the quest for constructive models of synthetic algebraic geometry. We will avoid technical semantic considerations, and focus on what this machinery can give us, i.e. models of HoTT satisfying various additional axioms, enabling us to work synthetically in various sheaf topoi.

The main applications so far are to build constructive models for synthetic algebraic geometry and synthetic Stone duality, enabling us to work synthetically in the topoi of Zariski sheaves and of light condensed sets. We expect more applications in the future, leading to synthetic work in other sheaf topoi.

In more details, we will first explain how one can work synthetically in any classifying higher presheaf topoi by adding three axioms to HoTT, following the work of Thierry Coquand, Jonas Höfer and Christian Sattler. We will then define topologies and their associated sheaves internally to these presheaf topoi. We will show how to use such a topology to work synthetically in the associated sheaf model of HoTT, using a variant of the presheaf axioms.

As an application we will give models for synthetic algebraic geometry and 3 closely related variants, based on the presheaf topos classifying rings, the Zariski topos, the étale topos and the fppf topos. We will contrast the additional axioms satisfied by each of these models, giving an interesting perspective on the ubiquitous use of these topologies in algebraic geometry.

As a conclusion we will explain how synthetic Stone duality and the topos of light condensed sets fit in this picture, as well as possible future applications and extensions for this framework.

Organisers