Designing a Formal Statistics Library
A collaborative visit to design a coherent, domain-specific statistics library in Lean 4 and Mathlib, and to plan a follow-on workshop.
A collaborative visit to design a coherent, domain-specific formal statistics library in Lean 4. Modern statistical theory draws on real and functional analysis, measure-theoretic probability, stochastic calculus, combinatorics, information theory, differential geometry, convex geometry, and algebra; existing Lean/Mathlib efforts in this space are isolated, and a coordinated library would build on Mathlib foundations and contribute back to it. Goals for the visit include refining a build-order blueprint (target definitions, theorems, Mathlib prerequisites, and estimated difficulty per branch), determining optimal abstraction levels, and beginning formalization of the most highly connected components.