Proof assistants are tools allowing to formally express mathematical statements and their proofs, and to mechanically check their correctness. At their core, they consist of a logical system materialized by a formal symbolic language for expressing statements and proofs, together with an algorithm deciding the validity of such proofs. These components are called the Kernel of such tools, and they are the basis for the trust in the theorems that one proves using a proof assistant. As such, kernels enjoy of the most scrutiny and meta-theoretical focus. However, the logical langage of a kernel is too excplicit and inconvenient to manipulate and to read. For this reason, the langage that is exposed to a proof assistant’s user is a high level one, which is then elaborated to the kernels language. In this talk, I will present (in the context of the Rocq proof assistant) two major parts of elaboration: generalized dependent pattern matching and higher-order unification. I will discuss how they contribute to the expressivity of the user-level language, and challenges that arise in implementing them and in formalizing them.
The most efficient algorithms to solve linear systems with structures such as Toeplitz, Vandermonde or, Cauchy-likeness are randomized. Such algorithms rely on a structured version of the fast Gaussian elimination that requires the input matrix to satisfy the generic rank profile condition. When the latter is not satisfied, a randomized preprocessing step is used. In this work, we present a deterministic algorithm that solves such systems within a complexity that matches the best known bounds previously achievable only through randomization. The algorithm relies on 3 main steps, each handled using recently developed fast and deterministic algorithms for modular approximation problems. We extract a vector M-Padé approximation, compress its solutions via kernel computations, then reduce it to a simultaneous M-Padé approximation.
The normalized substring complexity \(\delta\) of a string is defined as \(\max_k \{c[k]/k\}\), where \(c[k]\) is the number of distinct substrings of length \(k\). This simply defined measure has recently attracted attention due to its established relationship to popular string compression algorithms. We consider the problem of computing \(\delta\) online, when the string is provided from a stream. The work relies on a combination of results of word combinatorics, string algorithms, data structures and computational geometry.
In this talk, I will discuss distributed leader election algorithms in weak distributed communication models such as the beeping model and the stone-age model. Unlike most previous works, our algorithm operates with only six states, does not require unique identifiers, and makes no assumptions about prior knowledge of the network’s size or topology. We show that, under our randomized protocol, the system almost surely converges to a configuration in which a single node enters the leader state, in O(D² log n) rounds, where D is the network diameter. Moreover, if an approximation of D is known, the convergence time can be improved to O(D log n).
The algorithm is not self-stabilizing, as it requires all nodes to start from the same initial state. I will also present a generalization of the algorithm in the state-based computation model, aiming to achieve a self-stabilizing solution.
Broadly speaking, we study an evolution of mass from a source distribution to a target, defined by a (continuous-time) gradient descent of a functional acting like a ‘distance’ to the target. We are interested in the well-posedness of such an evolution (characterized by a PDE) and the criterion under which it converges to the target. Our study takes the source and target to be Gaussian distributions, as it yields closed-form expressions. We show convergence when the source is not degenerate (i.e. is supported on the whole Euclidean space), and provide counter-examples when it is degenerate (i.e. supported on a strict subspace). In the case where the covariances of the source and target distributions commute, we give quantitative convergence rates, being exponential when the source and measures have the same support but dropping to sublinear (O(1/t)) when the target is concentrated on a strict subspace of the source’s support. The first section of the presentation will be devoted to the exposition of the theory of optimal transport and how it allows to generalize the notion of gradient descent to the space of probability measures, as well as the definition and properties of the considered functional, which is built on an entropic version of optimal transport. The rest of the presentation will deal with the results of our paper.
Cet exposé est composé de deux parties. Dans la première, je présente un nouveau cadre d’étude de l’erreur de généralisation des algorithmes d’apprentissage statistique, à travers un nouveau prisme de compressibilité de taille variable des algorithmes que j’introduis.
Dans ce cadre, l’erreur de généralisation d’un algorithme est liée au taux de compression de ses données d’entrée. Je montrerai que : (i) cela permet d’obtenir des bornes qui dépendent de la mesure statistique empirique des données plutôt que de leur distribution inconnue, (ii) que ces bornes englobent et améliorent plusieurs bornes existantes de type PAC-BAYES, ou obtenues par approche théorie de l’information comme celle de Xu-Raginsky ou encore fondées sur la dimension intrinsèque de la structure fractale sous-jacente de l’algorithme, révélant ainsi le caractère unificateur de l’approche. Il sera aussi montré que l’on peut utiliser ce cadre pour développer de nouvelles bornes plus fines sur la généralisation.
Dans la seconde partie de l’exposé, j’aborde la question importante du rapport entre pouvoir de généralisation et faculté de mémoire des algorithmes d’apprentissage statistique, question qui est encore à élucider.
En effet, l’intuition selon laquelle les bons algorithmes devraient extraire uniquement les informations pertinentes et écarter les informations superflues, intuition étayée par certains travaux théoriques, est remise en question par le succès retentissant des réseaux de neurones profonds sur-paramétrés modernes. Je montrerai comment le cadre de compressibilité introduit dans la première partie de l’exposé permet de déterminer si la mémorisation est une composante nécessaire a la généralisation, comme cela a été récemment affirmé dans certains travaux.
- Data-dependent generalization bounds via variable-size compressibility, IEEE Transactions on Information Theory, vol. 70, no. 9, p. 6572-6595, Sept. 2024, disponible sur https://arxiv.org/abs/2303.05369,
- Tighter CMI-Based Generalization Bounds via Stochastic Projection and Quantization, NeurIPS 2025, disponible sur https://arxiv.org/abs/2510.23
On étudie les shifts ou espaces de pavages de type fini: des colorations de la grille régulière infinie qui évite un ensemble fini de motifs interdits. Il s’agit d’un modèle étudié en particulier comme source apparemment infinie de problèmes indécidables.
Les hom shifts sont une restriction du modèle où les motifs interdits sont petits et isotropes (indépendants de la direction). Par contraste avec le cas général, de nombreuses questions deviennent résolubles. La frontière entre problèmes décidables et indécidables est toujours largement ouverte.
Je parlerai d’une série de résultats autour de la question suivante : étant donné une coloration partielle, est-il possible de la compléter en une coloration de la grille entière (en évitant les motifs interdits) ?
Cette question nous fera voyager à travers plusieurs panoramas mathématiques : homotopie des graphes finis, propriétés de mélange, groupes fondamentaux et cocyles des shifts, et des résultats d’indécidabilité qui reviennent par surprise.
Cet exposé est issu de travaux en commun avec Nishant Chandgotia, Silvère Gangloff et Piotr Opocha.
The chromatic number of a graph is the minimum number of colours one needs to colour its vertices so that the endpoints of every edge receive distinct colours. This metric, introduced nearly two centuries ago, has since played a central role in graph theory and has found numerous practical applications.
A natural question in structural graph theory is how the chromatic number constrains the structure of graphs. One prominent example is the Gyárfás-Sumner conjecture, which aims to characterize the local structure of graphs with arbitrarily large chromatic number. Although this question may sound like yet another structural graph theorist’s favourite refrain (« how does metric interact with graph structure? ») we will explain why it is genuinely well motivated and how one is naturally led to the Gyárfás-Sumner conjecture.
We then show how similar lines of reasoning lead to similarly flavoured conjectures for other combinatorial objects, in particular directed graphs. We conclude by presenting recent advances towards this directed analogue of the Gyárfás-Sumner conjecture.
This talk features joint works with Pierre Aboulker, Pierre Charbit, Luis Kuffner, Rafael Steiner and Stephan Thomassé.
On étudie un processus d’apprentissage par renforcement, inspiré par les fourmis, qui communiquent à l’aide de phéromones. On considère un graphe G, avec deux nids (des sommets, N1 et N2) et une source de nourriture (un autre sommet, F). À chaque étape, une fourmi : 1) part d’un nid (aléatoire, N1 ou N2) et réalise une marche aléatoire (pondérée par les poids des arêtes) jusqu’à une source de nourriture F ; puis 2) à son retour, elle dépose des phéromones, c’est-à-dire renforce les arêtes (en ajoutant 1 à leur poids) appartenant au chemin aller auquel on a enlevé les boucles inutiles.
Pour des raisons techniques, nous étudions le cas des graphes séries-parallèles en triangle, c’est à dire des graphes obtenus en remplaçant chaque arête du triangle N1 N2 F par un graphe série-parallèle. On montre que les poids des arêtes (normalisés) convergent, vers des variables aléatoires nulles si les arêtes associées n’appartiennent pas à un plus court chemin d’un sommet de {N1, N2, F} à un autre.
Nous présenterons plusieurs outils utiles pour prouver cette convergence, notamment la comparaison avec des processus d’urnes, des techniques d’approximations stochastiques et des arguments combinatoires.
La présentation se basera sur un travail en commun avec Cécile Mailler.
Une journée de rencontres autour des cartes combinatoires le jeudi 29 janvier 2026, avec quatre exposés mélangeant combinatoire, probas et algo. Dans l’ordre :
- Marie Albenque (CNRS, IRIF), Slice decomposition of hypermaps
- Mathieu Mourichoux (UMPA, ENS Lyon), Constructing the Brownian sphere from a random unicycle
- Baptiste Louf (CNRS, IMB), Grands expanseurs dans les cartes de grand genre
- Alfredo Hubard (UGE, LIGM), Nombre de croisements (Crossing numbers)
Le programme complet est disponible à l’adresse https://indico.in2p3.fr/event/38241/
Si vous souhaitez également vous joindre au repas, merci d’écrire directement à l’équipe d’organisation :
Éric Fusy, Wenjie Fang et Valentin Bonzom