Workshop
The Mathematical Components Workshop will take place on Wednesday 7 December 2022.
This event has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (FRESCO grant agreement No. 101001995)
Program
 09:30  10:00 : Welcome coffee
 10:00  11:00 : Georges Gonthier, Legacy of the odd order: 10 years of Mathematical Components
 11:00  12:00 : Florent Hivert, Enumerative Combinatorics in MathComp: Formal Power Series and the example of Catalan numbers
 12:15  13:45 : Lunch
 14:00  15:00 : Jeremy Avigad, From Mathematical Components to Mathlib
 15:00  16:00 : Guillaume Melquiond, Numerical Computations and Formal Proofs
 16:00  16:30 : Coffee break
 16:30  17:30 : Reynald Affeldt, Application of Mathematical Components to probabilities and program formalization
Abstracts

Legacy of the odd order: 10 years of Mathematical components

From Mathematical Components to Mathlib
The design of Lean and mathlib were influenced by a number of other systems and libraries. Coq/SSReflect and the Mathematical Components library were prominent among them. In this talk, I will survey the state of Lean and mathlib today, discuss some of the ideas that they inherit from SSReflect and Mathematical Components, and talk about the way the ideas carry over. I will also characterize some of the differences between the projects, and explore possibilities for future interaction.

Enumerative Combinatorics in MathComp: Formal Power Series and the example of Catalan numbers.
One of the main tools in the field of enumerative combinatorics is the notion of formal power series which allows to manipulate easily and efficiently the sequences of numbers counting families of combinatorial objects according to a notion of size. Based of a work of Cyril Cohen and Boris Djalal, we developed two formalizations of power series : the first is axiom free and formalize truncated power series. The second needs classical axioms and formalize (infinite) power series as inductive limits of the truncated ones.
As an application, we prove the textbook result stating that the number of binary trees with n nodes is given by the Catalan number. Aside a bijective proof, the idea is to first prove that the generating series of Catalan number verify the algebraic equation
\[F = 1 + X F^2\]Then to extract the coefficients, three approach are used : the extended Newton binomial identity, the LagrangeBurman inversion theorem and holonomic computation translating the algebraic equation to a differential one. We try the three approaches for both truncated and infinite series which allows us to compare the advantages of the two kinds of series.

Numerical Computations and Formal Proofs
The main role of a system like Coq is to verify all the details of a proof written by the user using a formal language. Using such a proof assistant offers an unmatched confidence in the theorem statements, at the expense of a huge and tedious work by the user. While this approach is usually applied to symbolic reasoning, this talk will show how one can formalize mathematical theorems whose proofs rely on numerical computations. The first step is to implement arithmetic algorithms from the ground up in the logic of Coq: integer arithmetic, floatingpoint arithmetic, interval arithmetic, Taylor models. Once they have been formally verified, these numerical algorithms can be used inside formal proofs to alleviate the user proof effort. Moreover, they pave the way to using Coq, not only as proof assistant, but also as a computer algebra system: global optimization, root finding, proper and improper definite integrals, plots, and so on.

Application of Mathematical Components to probabilities and program formalization
We report on our experience using the Mathematical Components library to formalize information theory and effectful programs. MathComp provided us with crucial ingredients for that purpose: iterated operators to represent finite distributions and packed classes to represent convex spaces. Starting from these data structures, we formalized a hierarchy of monad interfaces that includes random choice and used this hierarchy to mechanize monadic equational reasoning in Coq. More recently, we could also take advantage of MathCompAnalysis and its formalization of measure and integration theory to formalize the semantics of a probabilistic language.
Sponsors
List of participants
 Ahmed Abdelraoof
 Affeldt Reynald
 Alain Delaët–Tixeuil
 Alessandro Bruni
 Ariel Kellison
 Assia Mahboubi
 Christopher Mary Kouam
 Cosimo P. Brogi
 Cyril Cohen
 David Ilcinkas
 Ekaterina Komendantskaya
 Emilio Jesús Gallego Arias
 Enrico Tassi
 Faustine OLIVA
 Felipe Lisboa Malaquias
 Florent Hivert
 Georges Gonthier
 Guillaume Melquiond
 Jerome Leroux
 Kazuhiko Sakaguchi
 Laurence Rideau
 Laurent Thery
 Marina López
 Maxime Denes
 Mohit Kumar Tekriwal
 Mouhcine Houda
 Natalia Slusarz
 Péter Bereczky
 Pierre Jouvelot
 Pierre POMERETCOQUOT
 Quentin VERMANDE
 Raül Espejo
 Remi Di Guardia
 Sebastián Ricardo Cristancho Sierra
 Sofia Santiago
 Takafumi Saikawa
 Thibault Hilaire
 Yves Bertot