Verified Math Foundations

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. Building on this infrastructure in MathComp-Analysis, I formalize probability theory in Rocq, including:

• Probability measures, random variables, and independence
• Concentration inequalities — quantitative bounds (e.g., Markov, Chebyshev, Hoeffding) that are essential for statistical machine learning
• Lp spaces — formalized theory of Lebesgue function spaces, providing key tools for functional analysis and probability

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. These foundations directly support my work on Neurosymbolic AI, where verified probability theory provides the mathematical backbone for reasoning about neural network robustness and correctness.

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

1. Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, et al.: Mathematical Components Analysis. 2025

2. Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa: Formalizing concentration inequalities in Rocq: infrastructure and automation. ITP 2025 PDF slides

3. Reynald Affeldt, Alessandro Bruni, Pierre Roux, Takafumi Saikawa: Yet another formal theory of probabilities in Coq. TYPES 2024 slides abstract

4. 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

5. Ieva Daukantas, Alessandro Bruni, Carsten Schürmann: Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation. PPDP 2021

Funding

This work is supported in part by the Carlsberg Foundation grant VeriFunAI and through collaborations within the EuroProofNet COST Action network.

Software

MathComp-Analysis — I contribute a formalization of probability theory to this Rocq/Coq library. The code is open-source and available on GitHub.

Infotheo — A Rocq/Coq library for information theory and probability, formalizing entropy, mutual information, and related results.