Fun with infinite time Turing machines: A bizzare world with fewer reals than naturals

There are more real numbers than natural numbers. Or are there? Meet the bizarre world of infinite time Turing machines, where two plus two is still four and still infinitely many prime numbers exist, but where the axiom of choice fails, not every mathematical assertion is true or false—and where there is an injection from ℝ to ℕ.

This alternative mathematical universe is an example for a so-called "topos". Originally created for Grothendieck's revolution of algebraic geometry to overcome severe mathematical obstacles, gradually a rich and colorful landscape of such toposes emerged. Nowadays they have found applications in diverse subjects such as combinatorics, differential geometry, computability theory and even quantum mechanics.

Just as the shortest and best way between two truths of the real domain often passes through the imaginary one, sometimes a short and conceptual proof about objects of the standard topos passes through an alternative one. This talk presents a first a introduction to this circle of ideas. No prerequisites are required, everyone is welcome to join the seminar.


Secrets of the Internet: From how it works to why it's unsafe. A primer for everyone who does not know what an IP address is

Invisible to the casual user, computers communicate and work together in the background to deliver the mathematics videos you're craving. In this tutorial, we will use a special hacking tool to render this communication visible. With live demos we will learn that the domain names like uantwerpen.be we're familiar with are a thin layer around so-called IP addresses, which are the real addresses computers use to identify themselves. We will uncover hidden information your browser sends along each request, and we'll see how easy it is to intercept traffic.

One of the audience members may volunteer to log into a website with their phone or laptop, and I'll display the password on the projector.

In the second half of the talk, we will focus on several mathematical breakthroughs which are contributing every day to Internet communication protection, including the wonder of asymmetric cryptography, the mystery of safe key exchange in the open, the amazing role of elliptic cuves and the importance of formal proofs for verifying cryptographic protocols.

This workshop is for everybody who is interested in knowing how the Internet works and wants to learn in which form computers talk to each other. Absolutely no prerequisites are required. People who are familiar with network stacks will be bored to hell.


Provable unprovability: A primer to the multiverse philosophy

Many conjectures in mathematics have turned out to be provable. Others were refuted. Some we don't know yet. And then there are those conjectures which—provably so!—will never be settled: There are statements for which we can prove that they don't have a proof, and for which we can also prove that they don't have a refutation.

Hence a mathematical multiverse emerges, as for those undecided statements we can just arbitrarily declare whether to adopt or reject them.

The lecture gives a first introduction to this circle of ideas, with examples for provably unprovable assertions from several subjects. No prior knowledge is required—everyone is welcome to join the seminar!


Introduction to Agda, a collaborative proof assistant

Agda is a computer program for assisting us in composing mathematical proofs: Agda meticulously verifies every proof step, perspicuously summarizes the current proof state, systematically generates case distinctions and, in some special cases, automatically fills in proofs.

Originally conceived at the end of the 1990s, Agda and other proof assistants have gained traction by a series of recent developments. In view of several "Lemma 1.1 breakdown catastrophes", they are increasingly used to secure mathematical works; but more importantly, the late Fields medalist Voevodsky pursued the vision for proof assistants to unlock new realms of mathematics, complex theories so advanced that they require computer support for their construction. The successful liquid tensor experiment, in which a proof assistant facilitated a collaborative effort to verifying cutting-edge research in algebra and topology, is a remarkable example. Others use proof assistants for the more modest reasons to help them understand or find the most elegant presentations of mathematical theories, verify the correctness of programs or extract algorithms from proofs.

One of the most intriguing features of proof assistants might not be technical, but social in nature: Agda and similar tools enable new forms of mathematical collaboration on an unprecedented scale—and using them can be an incredibly enjoyable and deeply rewarding experience.

The lecture gives a first introduction to Agda. No prior knowledge is required—everyone is welcome to join the seminar!


The axiom of choice: fractal monsters, sandboxes and an unexpected conclusion

Initially arising from a simple observation about finite sets, the axiom of choice has become a cornerstone of the logical framework underlying modern mathematics. Despite its widespread use, the axiom of choice remains one of the most controversial principles in mathematics; proofs using the axiom of choice are sometimes flagged, and some mathematicians try to avoid choice at all. Are these concerns justified?

The talk will begin with a careful explanation what the axiom of choice is about and what it's not. We then put it under logical scrutiny, in the process learning to judge potential axioms by more dimensions than their apparent truth. We will weigh on consequences of the axiom of choice, explore how it can be contained and discuss how a fantasy world containing a counterexample might look like.

No prior knowledge is required—everyone is welcome to join the seminar!