发表机构
Department of Economics and Statistics, University of Salerno (Italy)（萨莱诺大学经济与统计系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文探讨机器辅助数学技术对统计理论研究与教学的潜在变革，通过案例研究说明其在统计经典问题分析中的应用，呼吁构建形式化知识库，推动统计理论发展与教学革新。
AI 中文摘要
计算革命正以前所未有的速度推进，证明助手技术与生成式AI工具的结合，近期已能解决纯数学领域的复杂问题，其规模在数年前还被认为遥不可及。然而，这些技术尚未成为统计理论发展的标准工具。本文不提出新的理论结果，而是讨论五个涉及统计学经典问题的案例研究，描述如何使用机器证明检查对这些问题进行分析。我们的目标并非提出确定的工作流程，而是激发思考：这些技术可能如何改变理论研究与高级统计教育。我们聚焦两个主要方面：其一，统计理论常将大量数学内容压缩为“在通常正则性条件下”这类表述，用机器可验证语言进行形式化，会迫使每个假设明确化，揭示隐藏的依赖关系，加深对形式化对象的理解；其二，我们认为统计学界可从协作构建形式化公理、定义与定理的知识库中获益，这能支持更精确、可靠的理论发展。最后，我们探讨这些工具在研究生教育中的作用：正如高级编程语言通过支持快速实验与原型设计，彻底改变了实证研究，机器辅助形式化可能为统计理论的构建、验证与交流引入新范式。
英文摘要
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.
CommentsCode available at: https://github.com/pietro-coretto/lean-matstat-case-studies
