Statistical Theory in the Age of Machine-Assisted Mathematics: Rethinking How Theory Is Made and Taught
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. However, these technologies 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 they can be analyzed using a machine proof-checking. Our goal is not to propose a definitive workflow, but to stimulate reflection on how these technologies may transform theoretical research and advanced statistical education. We focus on two main aspects. First, statistical theory often compresses substantial mathematical content into expressions such as "under the usual regularity conditions". Formalization in a machine-verifiable language forces each assumption to be explicit, reveal hidden dependencies, and provide a deeper understanding of the formalized objects. Second, we argue that the statistical community could benefit from a collaborative effort to build repositories of formalized axioms, definitions, and theorems, supporting more precise and reliable theoretical developments. Finally, we discuss the role of these tools in graduate education. Just as high-level programming languages revolutionized empirical research by enabling rapid experimentation and prototyping, machine-assisted formalization may introduce a new paradigm for the development, verification, and communication of statistical theory.
Related
- Development of APOS Model Student Worksheet Assisted by GeoGebra on Line and Angle Material Representation in Mathematics in Junior High School
- On AI and Progress in Mathematics: Dreaming a Mathematical Universal Machine
- Studying proof data with proof theory: the case of AI-generated mathematics
- What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics
- A statistical theory for blind denoising: minimax estimation of the noise level from a single sample
BibTeX
@misc{coretto2026statistical,
title = {{Statistical Theory in the Age of Machine-Assisted Mathematics: Rethinking How Theory Is Made and Taught}},
author = {Pietro Coretto},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.04481},
eprint = {2609.04481},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.04481},
}
RIS
TY - UNPB
TI - Statistical Theory in the Age of Machine-Assisted Mathematics: Rethinking How Theory Is Made and Taught
AU - Pietro Coretto
PY - 2026
DA - 2026/09/03
PB - arXiv
DO - 10.48550/arxiv.2609.04481
UR - https://arxiv.org/abs/2609.04481
AB - 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. However, these technologies 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 they can be analyzed using a machine proof-checking. Our goal is not to propose a definitive workflow, but to stimulate reflection on how these technologies may transform theoretical research and advanced statistical education. We focus on two main aspects. First, statistical theory often compresses substantial mathematical content into expressions such as "under the usual regularity conditions". Formalization in a machine-verifiable language forces each assumption to be explicit, reveal hidden dependencies, and provide a deeper understanding of the formalized objects. Second, we argue that the statistical community could benefit from a collaborative effort to build repositories of formalized axioms, definitions, and theorems, supporting more precise and reliable theoretical developments. Finally, we discuss the role of these tools in graduate education. Just as high-level programming languages revolutionized empirical research by enabling rapid experimentation and prototyping, machine-assisted formalization may introduce a new paradigm for the development, verification, and communication of statistical theory.
ER -