Research Seminar Noncommutative and Functional Analysis

The research seminar Noncommutative and Functional Analysis is run by Roland Speicher, Michael Hartz and Moritz Weber. It consists in talks on latest research and graduation projects in Functional Analysis, Complex Analysis, Free Probability, Quantum Groups and Quantum Information. 

The seminar takes place on Mondays, from 16:15, in lecture hall IV, building E2 4, or online. Usually, the talks are 60 minutes for research talks and 45 minutes for expository talks of graduation theses („Bachelorseminarvortrag/Masterseminarvortrag“) excluding time for discussions.

List of all Talks

• Date: 28.06.2024
  Speaker: Tirthankar Bhattacharyya, Indian Institute of Science

• Date: 17.06.2024
  Speaker: Dietmar Bisch, Vanderbilt

• Date: 15.04.2024
  Speaker: Cuma Kökmen
  Time: 16:15
  Title: Das Corona-Theorem

• Due to sickness, this talk had to be cancelled. It will be postponed to Friday, 16.12.2023, 14:15.
  Date: 11.12.2023
  Speaker: Michael Skeide
  Time: 16:15
  Title: Partial Isometries Between Hilbert Modules
  Abstract: Hilbert modules are Banach spaces and share, of course, all their good properties. But geometrically they behave - as opposed with the very well-behaved Hilbert spaces - very much like pre-Hilbert spaces.
  As a common root of most problems - if not all - one may highlight the fact that Hilbert modules need not be self-dual; one of the most striking consequences of missing self-duality is the fact that not all bounded modules maps need to possess an adjoint. (Intimately related: not all closed submodules are the range of a projection.) This raises the question how to define isometries, cosisometries, and partial isometries between Hilbert modules, without requiring explicitly in the definition that these maps are adjointable.
  While the definition of isometries (as inner product preserving maps) is rather natural and well-known since long (they need not be adjointable), our definitions (proposed with Orr Shalit) of coisometries (they turn out to be adjointable) and partial isometries (they need not be adjointable) are rather recent.
  As a specific problem, we will address the question how to find a (reasonable) composition law among partial isometries (making them the morphisms of a category). It turns out that for Hilbert spaces the problem can be solved, while for Hilbert modules we have to pass to the *partially defined* isometries. The proofs of some of the intermediate statements explore typical features of proofs in Hilbert module theory: Some are like those for Hilbert spaces; some reduce the proof (by means of a well-known technical tool) to that for Hilbert spaces; and some are simply ``different''. (Of course, the latter also for work Hilbert spaces; but they are ``different'' from what you would write down with all you arsenal of Hilbert space methods at your disposal.)

• Date: 04.12.2023

  • Speaker: Dan Hill
    Time: 16:00
    Title: A functional analytic framework for radial PDEs
    Abstract: Radial partial differential equations can serve as an interesting extension from standard analytic problems in one spatial dimension into their planar counterparts. In order to further develop analytic tools---such as centre-manifold reductions---for radial PDE systems, we first need to establish the basic theory of radial function spaces. In contrast to general nonautonomous PDEs, radial PDEs possess highly structured nonautonomous terms and explicit smoothness conditions at the origin, which we exploit in our definitions.
    In this talk I will introduce a new framework for radial function spaces, considering the natural nonautonomous radial differential operators associated with radial PDEs, and show that they preserve the usual results found in the one-dimensional problem.

  • Speaker: Alberto Dayan
    Time: 17:10
    Title: A random matrices application to the study of Carleson measures for the polydisc
    Abstract: A Carleson measure on the unit disc is a positive measure that embeds continuously the Hardy space inside the corresponding L^2 space on the unit disc. The celebrated work of Carleson characterizes such measures in terms of a geometric condition that has to be tested only on squares based on the unit circle. Such notions have a natural extension to the polydisc, but in this case the geometric characterization becomes much more complicated to work with. In this talk, we will consider atomic measures on the polydisc generated by sequences, since determining if such measures are Carleson plays an important role in the theory of interpolating sequences. In particular, we will consider a random sequence in the polydisc, and we will discuss the 0-1 law for it to generate a Carleson measure almost surely. While in the one dimensional case such 0-1 law can be found by using Carleson's geometric condition, such tool is unavailable in the multi-variable setting. We will then discuss a well known reformulation of the problem in terms of random Gram matrices, and then describe those sequences that generates almost surely a Carleson measure for the polydisc by using tools from the theory of random matrices.

• Date: 27.11.2023
  Speaker: Petar Nizic-Nikolac (ETH Zürich)
  Time: 16:15
  Title: Non-asymptotic Link from Free Probability to Random Matrix Theory: Products of Gaussian Random Matrices
  Abstract: One central question in Random Matrix Theory is to determine how the basic parameters of the model (dimension, structure, matrix variance...) impact more complicated properties (spectral norm, minimal eigenvalue, invertibility...). Answers to these questions often provide useful tools when analyzing stochastic algorithms. These tools can be assessed through three different categories: generality (of models/assumptions), sharpness, and asymptoticity. Specifically, to bound the spectral norm of a Gaussian random matrix, many tools are known, each exhibiting a different trade-off in these categories. Usually, these results are either non-asymptotic but with an additional logarithmic dependence on dimension or exact but asymptotical.
  A recent work by Bandeira, Boedihardjo, and van Handel presented both exact and non-asymptotic bounds for a general class of Gaussian random matrices. This was achieved by importing techniques from Free Probability that exactly capture non-commutativity on an intrinsic level. The talk will focus on using this non-asymptotic link to import other such techniques while increasing model generality, particularly for a product of Gaussian random matrices. This is joint work with Bandeira, van Handel, and Zeng.

• Date: 17.11.2023
  Speaker: Fabian Selzer
  Time: 14:15
  Title: Das invariante Teilraumproblem

• Date: 13.11.2023
  Speaker: Qi Wang
  Time: 16:15
  Title: Die Cuntz-Algebra

• Date: 30.10.2023
  Speaker: Arne Berrens
  Time: 16:15
  Title: Non-commutative Function Theory and its commutative Applications
  Abstract: In this talk, we use non-commutative function theory to better understand certain spaces of commutative holomorphic functions. The main object considered here is the Fock space. We can think of the Fock space as the non-commutative version of the Hardy space. Further, every complete Pick space can be embedded into a Fock space. With the help of this embedding, we can prove many results for all complete Pick spaces via the Fock space. Davidson and Pitts proved an inner-outer factorization similar to that in the Hardy space. Building on this result, Jury and Martin obtained a better description of weak products of complete Pick spaces. The weak product is a generalization to the Hardy space H^1.

  Jury and Martin proved further a Blaschke-singular-outer factorization in the Fock space. This factorization is similar to the Blaschke-singular-outer factorization in the Hardy space. Aleman, Hartz, McCarthy and Richter showed that one can use the non-commutative inner-outer factorization to get the subinner-free outer factorization in the complete pick spaces. Following this approach and using the Blaschke-singular-outer factorization, we can further factor the subinner factor into a sub-Blaschke and sub-singular part.

• Date: 29.09.2023
  Speaker: Nina Kiefer
  Time: 14:15
  Title: Connection between the Compatibility of POVMs and Inclusion of Free Spectrahedra
  Abstract: In my talk, I will discuss the connection between compatible POVMs and the inclusion of free spectrahedra which was discovered by Andreas Bluhm and Ion Nechita. The emphasis is on an example illustrating this connection which is worked out both numerically and analytically.
  Free spectrahedra are matrix convex (free) sets determined by linear matrix inequalities; in particular, they generalize free spectrahedra, which are fundamental objects in various areas of mathematics such as convex optimization and real algebraic geometry. Compatible POVMs are settled in the field of quantum information theory and are important for some quantum information tasks. POVMs which are not compatible can be made compatible by adding noise.
  We will see that the noise level which is needed to make POVMs compatible can be expressed by deformations of free spectrahedra. In my presentation, I will also provide the background on POVMs and free spectrahedra which is needed for this purpose.

• Date: 24.07.2023
  Speaker: Abhay Jindal, Indian Institute of Science, Bengaluru, India
  Time: 16:15
  Title: Complete Nevanlinna-Pick kernels and the characteristic function
  Abstract

• Date: Tuesday, 18 July 2023
  Time: 16:15-17:15
  Place: SR 10
  Speaker: Marwa Banna, New York University Abu Dhabi.
  Title: Quantitative estimates on random matrices using free probability tools
  Abstract

• Date: 17.07.2023
  Speaker: Shuaibing Luo, Hunan University
  Time: 16:15
  Title: Some operator inequalities and a question of Shimorin’s
  Abstract: I will define some types of operators by operator inequalities, and present some of their properties. Then I will introduce a question of Shimorin’s which concerns these types of operators. I will present some partial results or idea to this question. This is a joint work with Eskil Rydhe.

• Date: 11.07.2023
  Speaker: Christopher Felder, Indiana University
  Room: SR 10
  Time: 16:15
  Title: Units for Forward Operator Monoids
  Abstract: This talk will introduce a forward operator monoid a discrete collection of bounded linear operators acting on a separable Hilbert space, which contains the identity, and has a strict monoid structure.
  We will then discuss generalized inner and cyclic vectors for these monoids, with a focus on vectors which are both inner a cyclic, which we will call units. Time permitting, we will connect this to some interesting open problems in analysis, including some completeness and approximation problems in Hilbert function spaces.

• Date: 10.07.2023
  Speaker: Georgios Tsikalas, Washington University in St. Louis
  Time: 16:15
  Title: Denjoy-Wolff points on the bidisk
  Abstract

• Date: Monday, 3 July 2023
  Speaker: Pei-Lun Tseng, New York University Abu Dhabi.
  Time: 16:00-17:00. (Note that we start at 16 Uhr s.t.)
  Place: HS IV
  Title: Infinitesimal operators and the Infinitesimal distributions of anticommutators and commutators
  Abstract: The idea of free independence (or freeness) was introduced by Voiculescu in 1985. It is very useful in the study of the asymptotic behavior of random matrices. Over time, numerous extensions and generalizations of free probability have emerged. One such generalization is infinitesimal freeness. In this presentation, we will begin by providing an overview of infinitesimal free probability theory and its connection to random matrix theory. Subsequently, we will delve into the topic of infinitesimal operators and explore their properties. Additionally, we will demonstrate techniques for computing infinitesimal distributions of anticommutators and commutators. Lastly, we will examine the concept of infinitesimal R-diagonal operators. This is joint work with J. Mingo. 

• Date: 15.05.2023
  Speaker: Nina Kiefer
  Time: 16:15
  Title: Connection between the compatibility of POVMs and inclusion of free spectrahedra
  Abstract: In my talk, I will discuss the connection between compatible POVMs and the inclusion of free spectrahedra which was discovered by Andreas Bluhm and Ion Nechita.
  Free spectrahedra are matrix convex (free) sets determined by linear matrix inequalities; in particular, they generalize so-called "spectrahedra", which are fundamental objects in various areas of mathematics such as convex optimization and real algebraic geometry. Compatible POVMs are settled in the field of quantum information theory and are important for some quantum information tasks, for example simultaneous measurements.
  We will see that compatibility of POVMs is equivalent to the inclusion of certain free spectrahedra (one of them being the so-called "matrix jewel") and that a set of POVMs can be made compatible by "adding noise", the needed amount of which can be expressed by deformations of free spectrahedra. In my presentation, I will also provide the background on POVMs and free spectrahedra which is needed for this purpose.

• Date: 08.05.2023
  Speaker: Stefan Richter (UT Knoxville)
  Time: 16:15
  Title: Multivariable versions Kaluza's Lemma
  Abstract

• Date: 24.04.2023
  Speaker: Evangelos Nikitopoulos
  Time: 16:15
  Title: Noncommutative C^k Functions, Multiple Operator Integrals, and Derivatives of Operator Functions
  Abstract

• Date: 06.02.2023
  Speaker: Alan Sola, Stockholm University
  Time: 16:15
  Title: Local theory of stable polynomials and bounded rational functions
  Abstract: We will discuss the boundary behavior of bounded rational functions in several variables from several perspectives, including existence of non-tangential limits and higher non-tangential regularity. The results we obtain in two variables rely on local descriptions of stable polynomials, and motivate a conjecture (since resolved by J. Kollar) regarding the characterization of bounded rational functions in the bidisk with a given stable denominator.
  This reports on joint work with K. Bickel, G. Knese, and J.E. Pascoe.

• Date: Tuesday, 31. Januar 2023
  Time: 17:15-18:15
  Place: HS IV
  Speaker: Jacob Campbell (Waterloo, Canada) 
  Title: Commutators in finite free probability
  Abstract: In free probability, a fundamental result of Voiculescu is that random unitary matrices are asymptotically free. A representative special case is the fact that sums A + U B U* and products A U B U* of large randomly rotated matrices approximate free additive and multiplicative convolution. In 2015, Marcus, Spielman, and Srivastava realized that in the non-asymptotic setting, one can recover ``finite" analogues of these free convolutions by looking at the expected characteristic polynomials of A + U B U* or A U B U*.   After reviewing these ideas, I will show how techniques from combinatorial representation theory can help to understand finite free convolutions, focusing on the problem (which I recently solved in arXiv:2209.00523) of describing the commutator of randomly rotated matrices in this context. The main techniques are Weingarten calculus and the Goulden-Jackson immanant formula. Time permitting, I will discuss some combinatorial questions which are raised by comparison with the commutator in free probability.

• Date: Thursday, 26 Januar 2023
  Time: 16:15-17:15
  Place: SR 9
  Speaker: Jinzhao Wang (Stanford)
  Title: Free probability in quantum gravity
  Abstract: I will survey two models in quantum gravity that showcase the effectiveness of free probability. They are the Penington-Shenker-Stanford-Yang (PSSY) model and the Double Scaled SYK model. Unlike other physical applications that mostly relate to free probability via random matrices. Here the links are drawn combinatorially and algebraically. This connection allows us to formulate and address questions that are otherwise difficult. In particular, I will emphasize on what do we gain by using the free probabilistic toolkit. 

• Date: 16.01.2023
  Speaker: Freek Witteveen
  Time: 16:15
  Title: Random tensor network states and free probability theory
  Abstract: Random quantum states are an important tool in quantum information theory. In this talk I will discuss random tensor network states, which have found application both in quantum information theory and as a toy model for holographic quantum gravity. We introduce a refined model with arbitrary link states. I will explain how the entanglement properties of such tensor network states depend on the graph structure and on the link states, focusing on a connection to free probability theory. This talk is based on arXiv:2206.10482 which is joint work with Newton Cheng, Cecilia Lancien, Geoff Penington and Michael Walter.

• Date: 07.11.2022
  Speaker: Maximilian Tornes, Universität des Saarlandes
  Time: 17:15
  Title: Weighted composition operators on unitarily invariant spaces on B_d
  Abstract

• Date: 11.07.2022
  Speaker: Marwa Banna (NYU Abu Dhabi)
  Time: 16:15
  Title: Berry-Esseen Bounds for Operator-valued Free Limit Theorems
  Abstract:
  The development of free probability theory has drawn much inspiration from its deep and far reaching analogy with classical probability theory. The same holds for its operator-valued extension, where the fundamental notion of free independence is generalized to free independence with amalgamation as a kind of conditional version of the former. Its development naturally led to operator-valued free analogues of key and fundamental limiting theorems such as the operator-valued free Central Limit Theorem due to Voiculescu and the asymptotic distributions of matrices with operator-valued entries.
  In this talk, we show Berry-Esseen bounds for such limit theorems. The estimates are on the level of operator-valued Cauchy transforms and the L\'evy distance. We also address the multivariate setting for which we consider linear matrix pencils and noncommutative polynomials as test functions. The estimates are in terms of operator-valued moments and yield the first quantitative bounds on the Lévy distance for the operator-valued free CLT. This also yields quantitative estimates on joint noncommutative distributions of operator-valued matrices having a general covariance profile.
  This is a joint work with Tobias Mai.

• Date: 16. May 2022

  • Speaker: Nikolaos Chalmoukis
    Time: 16:15
    Title: Semigroups of composition operators on spaces of analytic functions.
    Abstract: We will discuss the maximal subspace of strong continuity of a semigroup of composition operators acting on the space of analytic functions of bounded mean oscillation in the unit disc. The minimality of this space is related to a well known theorem of Sarason about the space of analytic functions of vanishing mean oscillation. In the case of elliptic semigroups we give a complete characterization in terms of the Koenigs function of the semigroups that can replace rotations in Sarason's Theorem. This answers to the affirmative a conjecture of Blasco et al. Similar results are also obtained for the Bloch space.
    This is a joint work with V. Daskalogiannis.

  • Speaker: Lisa Karst
    Time: 17:15
    Title: The Fejér-Riesz theorem and Schur complements
    Abstract

• Date: 9. May 2022
  Speaker: Sebastian Toth
  Time: 16:15
  Titel: Uniqueness of the multiplier functional calculus for pure K-contractions
  Abstract

• Date: 2. May 2022
  Speaker: Rachid Zarouf, Aix-Marseille Université
  Time: 16:15
  Title:  A constructive approach to Schäffer's conjecture
  Abstract

• Date: 25. April 2022
  Speaker: Alberto Dayan, Norwegian University of Science and Technology
  Time: 16:15
  Title: Dobinski Sets,  Function Theory and Sets of Null Capacity
  Abstract: The first half of the talk will focus on the construction of some Dobinski sets, which can be thought of as exceptional subsets of the unit interval made of points that are very well approximated via dyadic rationals. We will determine their logarithmic Hausdorff dimension and their logarithmic capacity. The second half of the talk will try to give a brief overview of how such exceptional sets can be used in function theory. In particular, we will see how sets of capacity zero are related to some open problems for the Dirichlet space on the unit disc, and time permitting we discuss some ongoing research in that direction.

• Date: 31. January 2022
  Speaker: Daniel Gromada
  Time: 16:15
  Title: New examples of quantum graphs
  Place: Zoom
  Abstract: Quantum graphs are the analogues of classical graphs in the world of non-commutative geometry. Their definition is very new and very little is known about them so far. Not only that: the current literature is also lacking some concrete non-trivial examples of quantum graphs to begin with. In this talk, we are going to summarize three different approaches for the definition of a quantum graph. Then we will present some ways how to construct concrete examples. We show how quantum graphs over a fixed quantum space can be classified, we show an example of a quantum graph which is not quantum isomorphic to any classical graph, and we show a certain twisting procedure for classical Cayley graphs of abelian groups. This talk is based on a recent preprint arXiv:2109.13618.

• Date: 24. January 2022
  Speaker: Nicolas Faroß
  Time: 16:15
  Title: Spatial Pair Partitions and Applications to Finite Quantum Spaces
  Place: MS Teams
  Abstract: In 2016, Cébron-Weber introduced spatial partition quantum groups as a generalization of easy quantum groups. These are compact matrix quantum groups whose intertwiners are indexed by categories of three-dimensional partitions.
  We study the quantum group associated to the category spatial pair partitions on two levels and show that it is isomorphic to the projective orthogonal groups. Further, we generalize combinatorial methods for partitions to the setting of spatial partition. This allows us to find an explicit description of a category of spatial partitions linked to quantum symmetries of finite quantum spaces.

• Date: 17. January 2022
  Speakers: 

  • Alexander Wendel
    Time: 16:15
    Title: Quantum Channels and Entangled States associated to Easy Quantum Groups
    Place: MS Teams
    Abstract: In 2017 Brannan and Collins constructed highly-entangled spaces and states from the representation theory of the orthogonal quantum groups. A key role in their construction is played by the famous Jones-Wenzl projections. These projections are usually defined via a certain commutation property and are projections onto irreducible representations of the orthogonal quantum group.
    Shortly before (2014/2016) Freslon and Weber gave a combinatorial characterisation of the irreducible representations and fusion rules of easy quantum groups.
    We are going to combine these two papers to investigate howfar one can carry over the results of Brannan and Collins to other easy quantum groups. Especially we are going to show that the projections onto irreducibles satisfy a similar characterisation as the Jones-Wenzl projections and are going to characterise by this the image of these projections. We are then going to transfer some results on entangled spaces to the symmetric quantum group and indicate how to carry out these constructions for other easy quantum groups.

  • Arne Berrens
    Time: 17:00
    Title: Von Neumann algebras and zero sets of Bergman spaces
    Place: MS Teams
    Abstract: The leading question in this talk will be under which condition there exists a Bergman space function vanishing on a given set. The Bergman space is the space of holomorphic functions on the unit disc that are square integrable. Using von Neumann algebras, we get new insights into the structure of the weighted Bergman spaces. Vaughan Jones used Fuchsian groups that act on the Bergman space as well as on the upper half plane. By studying the group von Neumann algebra they generate, he got a necessary and sufficient condition for the existence of a vanishing function on the orbit. To get to this result, one has to use mainly the theory of von Neumann dimension as well as the theory of reproducing kernel Hilbert spaces.
    This approach is not constructive, and we only get the existence of this function and no further information on what this function might look like. We will also look further into the connection of von Neumann algebras and Bergman spaces.

• Date: 10. January 2022
  Speaker: Steven Klein
  Time: 16:15
  Title: Shlyakhtenko's non-microstates approach to strongly 1-boundedness
  Place: MS Teams
  Abstract: Building on Voiculescu's microstates approach to the analogue of entropy in free probability theory, Jung introduced in 2007 some property of von Neumann algebras called "strongly 1-boundedness" which has found many interesting applications. Recently, in 2020, Shlyakhtenko developed an approach to strongly 1-boundedness using non-microstates techniques. In particular, he proved estimates for the non-microstates free entropy of operators satisfying algebraic relations and used this to give an alternative proof of a criterion for strongly 1-boundedness obtained originally by Jung.
  In my talk, I will give a brief introduction to Voiculescu's concepts of free entropy and will discuss their relations to strongly 1-boundedness with focus on Shlyakhtenko's non-microstates approach.

• Date: 15. December 2021
  Speaker: Simon Schmidt, QMATH, Copenhagen
  Time: 11:00
  Title: A graph with quantum symmetry and finite quantum automorphism group
  Place: Zoom
  Abstract: This talk concerns quantum automorphism groups of graphs, a generalization of automorphism groups of graphs in the framework of compact matrix quantum groups. We will focus on certain colored graphs constructed from linear constraint systems. In particular, we will give an explicit connection of the solution group of the linear constraint system and the quantum automorphism group of the corresponding colored graph. Using this connection and a decoloring procedure, we will present an example of a graph with quantum symmetry and finite quantum automorphism group. This talk is based on joint work with David Roberson.

• Date: 13. December 2021
  Speakers: 

  • Matias Klimpel
    Time: 16:15
    Title: Representations of Graph C*-algebras
    Place: MS Teams
    Abstract: Graph C*-algebras were introduced in 1998 as a generalization of Cuntz-Krieger algebras introduced by Cuntz and Krieger in 1980, which in turn arose as a more generalized version of the Cuntz Algebra O_n introduced by Cuntz in 1977. As we will see, the class of graph C*-algebras is quite large and as such a useful one to understand.
    In this talk we will present these objects and their relations as well as visualize them on a host of examples. In particular, we classify all graph C*-algebras associated to finite graphs without cycles, give an algorithm to construct a non-trivial representation for a graph C*-algebra associated to a row-finite graph and present two import uniqueness theorems for graph C*-algebras, namely the gauge-invariant uniquess theorem and the Cuntz-Krieger uniqueness theorem.

  • Dean Zenner
    Time: 17:00
    Title: Hypergraph C*-algebras
    Place: MS Teams
    Abstract: In this talk I will introduce the concept of hypergraph C*-algebras. The concept is based on a new definition that was conveyed to me by Simon Schmidt and Moritz Weber.
    Our main goal is to show that hypergraph C*-algebras define a generalization of graph C*-algebras.  In contrary to graph C*-algebras, we will see that hypergraph C*-algebras do not need to be nuclear.  They actually form a stricly larger class than the class of graph C*-algebras. Besides that, we will have a look at some interesting examples that I investigated.
    At the end of the talk I will speak about a way to 'hyperize' graph C*-algebras.

• Date: 29 November 2021
  Time: 16:15
  Speaker: Marc Hermes
  Title: Peano Arithmetic in Constructive Type Theory and Tennenbaum's Theorem
  Place: MS Teams
  Abstract: Gödel's first incompleteness theorem entails that the first-order theory of Peano arithmetic (PA) and its consistent extensions admit a wealth of independent statements. By the completeness theorem then, PA cannot be categorical, meaning it does not posses a unique model up to isomorphism.  
  A theorem by Stanley Tennenbaum however tells us that if we restrict our attention to computable models, first-order PA is categorical with regards to this class of models.
   The goal of this talk is to present the first-order theory of PA inside of a constructive type theory and to revisit and study Tennenbaum's theorem in this constructive setting.
  We will start out the talk with an introduction to the maybe unfamiliar world of constructive mathematics and how this setting influences the possibilities we have in the investigation of mathematical questions in general. We then come back to the particular case of Tennenbaum’s theorem, where the setting allows for a synthetic viewpoint of computability, by consistently assuming that every function on the natural numbers is computable (i.e. Church's thesis), making it possible to abstract from many details in computability arguments. We will then finish with a few words on the computer-verified proof of the theorem.