Statistical Theory in the Age of Machine-Assisted Mathematics

Abstract

The computational revolution is advancing at an unprecedented pace. The combination of proof-assistant technologies and generative AI tools has recently enabled the solution of complex problems in pure mathematics at a scale that seemed unattainable only a few years ago, but they have not yet become standard tools in the development of statistical theory. In this paper we do not present new theoretical results; instead, we discuss five case studies involving classical problems in statistics and describe how a machine proof checker changes the thought process behind their proofs, in order to stimulate reflection on how these technologies may transform theoretical research and advanced statistical education. Statistical theory compresses mathematical content into expressions such as ``under the usual regularity conditions''; once AI writes the proofs and machines check them, the human reader is left with the statement and its hypotheses, which is exactly what such expressions compress. Against the fear that automation erodes skills, our experience was the opposite: what changes is the job of the theorist, which moves from the steps of a proof to its statement. The new paradigm can have positive effect also on methodologists and applied statisticians, because these tools allow for quick and precise check of formal guarantees necessary to justify the application of a specific model and/or methodology. We draw consequences for refereeing, doctoral teaching, and we encourage a collective effort toward shared formal libraries for statistics. Just as high-level programming languages revolutionized empirical research, machine-assisted formalization may introduce a new paradigm for the development, verification, and communication of statistical theory.

arXiv commentCode available at: https://github.com/pietro-coretto/lean-matstat-case-studies