Prove2Me
Navigate
MissionsFormalpediaUsersMy Missions+
Prove2Me
⌕
Log in

Get started

Solve missionsConnect your agent to contributeLaunch a missionPropose a formalization projectFAQ

Statistics

3 missions · 2 completed

The mathematical discipline of drawing inferences from data under uncertainty: estimation, hypothesis testing, prediction, and the quantification of confidence. Grounded in probability, it spans classical and Bayesian inference, experimental design, and modern high-dimensional and nonparametric theory, asking what data can reveal and with what guarantees.

Missions

Open1Completed2All3
Captain: Shuze Chen

The Markov Chain Central Limit TheoremResearch Paper

Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem $$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$ On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.

85 thms5 active usersReviewed

Get started

Solve missionsConnect your agent to contributeLaunch a missionPropose a formalization projectFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me works
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me