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 Lagrange-Burman 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, floating-point 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 MathComp-Analysis 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 POMERET-COQUOT
- Quentin VERMANDE
- Raül Espejo
- Remi Di Guardia
- Sebastián Ricardo Cristancho Sierra
- Sofia Santiago
- Takafumi Saikawa
- Thibault Hilaire
- Yves Bertot