Markov kernels in Mathlib's probability library
Pith reviewed 2026-05-18 10:47 UTC · model grok-4.3
The pith
Markov kernels allow a single formal definition of conditional distributions, independence, and sub-Gaussian variables inside Mathlib.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
Markov kernels are introduced as measurable maps from a measurable space to the space of probability measures on another space; the formalized disintegration theorem then yields conditional probability distributions of random variables and posterior distributions, while the same object supplies uniform definitions of independence, conditional independence, sub-Gaussianity, entropy, and Kullback-Leibler divergence.
What carries the argument
The Markov kernel, a measurable map sending each point of one space to a probability measure on a second space, which carries the disintegration theorem and the uniform definitions of independence and sub-Gaussianity.
If this is right
- Conditional distributions of random variables become directly constructible from joint distributions via the disintegration theorem.
- Independence and conditional independence receive a common definition expressed through kernels.
- Sub-Gaussian random variables are characterized uniformly using the same kernel machinery.
- Formal expressions for entropy and Kullback-Leibler divergence follow from kernel operations.
Where Pith is reading between the lines
- The kernel-based approach could be reused to formalize other derived concepts such as mutual information or conditional entropy without new primitives.
- Posterior distributions obtained this way may support machine-learning proofs that rely on Bayesian updating inside the library.
- Similar disintegration arguments might extend to formalizations of stochastic processes or martingales.
Load-bearing premise
The existing definitions of random variables and measures already present in Mathlib's probability folder are correct.
What would settle it
An explicit pair of random variables on concrete spaces for which the formalized disintegration theorem returns a conditional distribution that fails to satisfy the defining integral equation of conditional expectation.
read the original abstract
The probability folder of Mathlib, Lean's mathematical library, makes a heavy use of Markov kernels. We present their definition and properties and describe the formalization of the disintegration theorem for Markov kernels. That theorem is used to define conditional probability distributions of random variables as well as posterior distributions. We then explain how Markov kernels are used in a more unusual way to get a common definition of independence and conditional independence and, following the same principles, to define sub-Gaussian random variables. Finally, we also discuss the role of kernels in our formalization of entropy and Kullback-Leibler divergence.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The manuscript describes the formalization of Markov kernels in Mathlib's probability library. It presents their definition and properties, details the machine-checked formalization of the disintegration theorem for Markov kernels, and shows how this theorem is applied to define conditional probability distributions of random variables and posterior distributions. The paper further explains the use of Markov kernels to obtain common definitions of independence and conditional independence, to define sub-Gaussian random variables, and to formalize entropy and Kullback-Leibler divergence.
Significance. This contribution provides verified, machine-checked foundations for key probabilistic constructs in Lean, including the disintegration theorem and its applications to conditioning and information-theoretic quantities. The explicit use of Lean proofs removes derivation gaps and supports reliable reuse in further formalizations of Bayesian methods and statistical learning. These strengths are load-bearing for the paper's value as a library-building effort.
minor comments (2)
- [Abstract] The phrase 'in a more unusual way' (abstract) for the independence definition would benefit from a one-sentence pointer to the specific section or lemma that implements it, to improve immediate readability for readers unfamiliar with the kernel approach.
- [Disintegration theorem section] Notation for the disintegration theorem (likely §3 or §4) could include an explicit statement of the measurability conditions on the kernel to avoid any ambiguity when readers compare it with textbook statements.
Simulated Author's Rebuttal
We thank the referee for their positive review of our manuscript on the formalization of Markov kernels in Mathlib's probability library. We appreciate the recognition of the contribution's significance for providing machine-checked foundations for probabilistic constructs, including the disintegration theorem and its applications to conditioning, independence, and information-theoretic measures. We are pleased with the recommendation to accept.
Circularity Check
No significant circularity; formalization is machine-checked on prior library
full rationale
The paper presents definitions, properties, and a formalization of the disintegration theorem for Markov kernels inside Mathlib, then uses it to define conditional distributions, independence, sub-Gaussian variables, entropy, and KL divergence. All steps are Lean proofs and type-theoretic constructions built on the existing probability folder whose basic random-variable and measure definitions are already accepted. No fitted parameters, self-definitional equations, or load-bearing self-citations appear; the verification is external to the paper via the Lean kernel and Mathlib's prior components. This satisfies the criteria for a self-contained, non-circular formalization result.
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Standard axioms of probability measures and random variables as already formalized in Mathlib
Lean theorems connected to this paper
-
IndisputableMonolith/Foundationreality_from_one_distinction unclear?
unclearRelation between the paper passage and the cited Recognition theorem.
We present their definition and properties and describe the formalization of the disintegration theorem for Markov kernels... used to define conditional probability distributions... independence and conditional independence... sub-Gaussian random variables... entropy and Kullback-Leibler divergence.
-
IndisputableMonolith/CostJcost unclear?
unclearRelation between the paper passage and the cited Recognition theorem.
structure Kernel(X Y:Type *)... measurable′ :Measurable toFun
What do these tags mean?
- matches
- The paper's claim is directly supported by a theorem in the formal canon.
- supports
- The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
- extends
- The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
- uses
- The paper appears to rely on the theorem as machinery.
- contradicts
- The paper's claim conflicts with a theorem or certificate in the canon.
- unclear
- Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.