Verified Mathematical Foundations in Rocq
Overview
Rigorous mathematics requires that theorems be provably correct. Proof assistants such as Rocq make this literal: every step of a proof is mechanically verified by a computer. I contribute to MathComp-Analysis, a large-scale formalization of mathematical analysis built on the Mathematical Components library.
My focus is on probability theory — building machine-checked foundations for the mathematics that underpins statistics, machine learning, and information theory.
Probability Theory and Lebesgue Integration
Classical probability theory rests on measure theory and the Lebesgue integral. I formalize this infrastructure in Rocq, including:
- Measure spaces, σ-algebras, and measurable functions
- The Lebesgue integral and its key theorems (monotone convergence, dominated convergence, Fubini)
- Probability measures, random variables, and independence
- Concentration inequalities — quantitative bounds (e.g., Markov, Chebyshev, Hoeffding) that are essential for statistical machine learning
This work bridges pure mathematics and applications: the same formalized concentration inequalities that appear in probability textbooks can be instantiated to give verified guarantees for learning algorithms.
Robust Statistics
Beyond pure probability, I work on verified algorithms for robust statistics — estimation methods that remain reliable even when data contains outliers or has been adversarially corrupted. Specific targets include:
- Verified robust mean estimation (trimmed means, filtering algorithms)
- Machine-checked proofs of correctness for statistical procedures such as risk-limiting audits
Related Publications
Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa: Formalizing concentration inequalities in Rocq: infrastructure and automation. ITP 2025 PDF slides
Reynald Affeldt, Alessandro Bruni, Pierre Roux, Takafumi Saikawa: Yet another formal theory of probabilities in Coq. TYPES 2024 slides abstract
Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann: Robust Mean Estimation by All Means (Short Paper). ITP 2024 PDF
Ieva Daukantas, Alessandro Bruni, Carsten Schürmann: Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation. PPDP 2021
Software
MathComp-Analysis — I contribute a formalization of probability theory to this Rocq/Coq library. The code is open-source and available on GitHub.