This talk has a dual aim: to provide a mathematical overview of Stone duality theory, and to invite collaboration on its Lean formalization.
Stone duality is an algebraic way of looking at profinite topologies. A profinite set is a compact, T2, totally disconnected space, or, equivalently, a topological space which can be obtained as the projective limit of finite discrete spaces. Stone proved in the 1930s that the category of profinite sets is dually equivalent to that of Boolean algebras, and, more generally, that the category of spectral spaces is dually equivalent to that of bounded distributive lattices. I will explain how spectral spaces can be advantageously understood as profinite posets, also known as Priestley spaces. I will also point to more modern research that takes Stone duality further, and may touch upon some mathematical contexts where it pops up, notably topos theory and condensed mathematics.
Elements of Stone duality theory have been formalized in Lean over the past few years, and I will report on some of the most recent progress. I will also propose a number of concrete formalization goals at various levels of estimated difficulty, to provide the audience with some potential project ideas for this week.[-]

The calculus of homotopy functors is an important topological tool that has been used to shed light on and make connections between fundamental structures in homotopy theory and K-theory. It has also inspired the creation of new types of functor calculi to tackle problems in algebra and topology. In this talk, I will begin by describing properties that a functor calculus should have, before looking at a particular functor calculus, the abelian functor calculus, that has its origins in the work of Eilenberg, Mac Lane, Dold, and Puppe. Using this calculus, one can define the analog of a “directional derivative” for functors of abelian categories. I will describe how this directional derivative is used to create a cartesian differential category from abelian functor calculus, and if time permits, discuss some related work on connections between functor calculus and differential categories.[-]

Recall that normality is a elementary form of randomness: an infinite word is normal to a given alphabet if all blocks of symbols of the same length occur in the word with the same asymptotic frequency. We consider a notion of independence on pairs of infinite words formalising that two words are independent if no one helps to compress the other using one-to-one finite transducers with two inputs. As expected, the set of independent pairs has Lebesgue measure 1. We prove that not only the join of two normal words is normal, but, more generally, the shuffling with a finite transducer of two normal independent words is also a normal word. The converse of this theorem fails: we construct a normal word as the join of two normal words that are not independent. We construct a word x such that the symbol at position n is equal to the symbol at position 2n. Thus, x is the join of x itself and the subsequence of odd positions of x. We also show that selection by finite automata acting on pairs of independent words preserves normality. This is a counterpart version of Agafonov's theorem for finite automata with two input tapes.
This is joint work with Olivier Carton (Universitéé Paris Diderot) and Pablo Ariel Heiber (Universidad de Buenos Aires).[-]

Carleson's Theorem states that for $1 < p < \infty$, the Fourier series of a function $f$ in $L^p[-\pi,\pi]$ converges to $f$ almost everywhere. We consider this theorem in the context of computable analysis and show the following two results.
(1) For a computable $p > 1$, if $f$ is a computable vector in $L^p[?\pi,\pi]$ and $t_0 \in [-\pi,\pi]$ is Schnorr random, then the Fourier series for $f$ converges at $t_0$.
(2) If $t_0 \in [-\pi,\pi]$ is not Schnorr random, then there is a computable function $f : [-\pi,\pi] \rightarrow \mathbb{C}$ whose Fourier series diverges at $t_0$.
This is joint work with Timothy H. McNicholl, and Jason Rute.[-]

I will discuss two recent interactions of the field called randomness via algorithmic tests. With Yokoyama and Triplett, I study the reverse mathematical strength of two results of analysis. (1) The Jordan decomposition theorem says that every function of bounded variation is the difference of two nondecreasing functions. This is equivalent to ACA or to WKL, depending on the formalisation. (2) A theorem of Lebesgue states that each function of bounded variation is differentiable almost everywhere. This turns out to be equivalent WWKL (with some fine work left to be done on the amount of induction needed). The Gamma operator maps Turing degrees to real numbers; a smaller value means a higher complexity. This operator has an analog in the field of cardinal characteristics along the lines of the Rupprecht correspondence [4]; also see [1]. Given a real p between 0 and 1/2, d(p) is the least size of a set G so that for each set x of natural numbers, there is a set y in G such that x and y agree on asymptotically more than p of the bits. Clearly, d is monotonic. Based on Monin's recent solution to the Gamma question (see [3] for background, and the post in [2] for a sketch), I will discuss the result with J. Brendle that the cardinal d(p) doesn't depend on p. Remaining open questions in computability (is weakly Schnorr engulfing equivalent to "Gamma = 0"?) nicely match open questions about these cardinal characteristics.[-]

One of the most fundamental problem in tiling theory is to decide, given a surface, a set of tiles and a tiling rule, whether there exist a way to tile the surface using the set of tiles and following the rules. As proven by Berger in the 60's, this problem is undecidable in general.
When formulated in terms of tilings of the discrete plane by unit tiles with colored constraints, this is called the Domino Problem and was introduced by Wang in an effort to solve satisfaction problems for ??? formulas by translating the problem into a geometric problem.
In this course, we will give a brief description of the problem and to the meaning of the word “undecidable”, and then give two different proofs of the result.[-]

Après une introduction générale présentant les principaux modèles et problèmes étudiés, nous étudierons plus précisément trois sujets qui permettront d'illustrer des propriétés algorithmiques, des aspects algébriques et logiques de cette théorie :
- caractérisation, décision et minimisation des transducteurs séquentiels ;
- équivalence et fonctionnalité de transducteurs : de l'indécidabilité à la décidabilité ;
- présentation logique des transducteurs, et clôture par composition.[-]

Après une introduction générale présentant les principaux modèles et problèmes étudiés, nous étudierons plus précisément trois sujets qui permettront d'illustrer des propriétés algorithmiques, des aspects algébriques et logiques de cette théorie :
- caractérisation, décision et minimisation des transducteurs séquentiels ;
- équivalence et fonctionnalité de transducteurs : de l'indécidabilité à la décidabilité ;
- présentation logique des transducteurs, et clôture par composition.[-]

Semistructured data is an umbrella term encompassing data models which are not logically organized in tables (i.e., the relational data model) but rather in hierarchical structures using markers such as tags to separate semantic elements and data fields in a ‘self-describing' way. In this lecture we survey some of the multiple connections between formal language theory and semi-structured data, in particular concerning the XML format. We will cover ranked and unranked tree automata, and its connections to Monadic Second Order logic, First Order logic, and XPath. The aim is to take a glimpse at the landscape of closure properties, algorithms and expressiveness results for these formalisms.[-]