从讲义到Lean：形式化一本概率论教材
From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory
浏览论文内容
中文总结 AI 辅助
本文开展Lean形式化工作，对一本14章的概率论教材进行形式化，生成机器可验证配套资料，复用Mathlib结果并引入接口引理，为AI辅助数学构建形式化基础。
中文摘要 AI 辅助
随着大型语言模型生成数学论证的能力不断增强，数学领域可能面临的不是证明稀缺，而是看似合理的证明过剩。在这种环境下，验证、阐释以及将证明整合到可复用的数学基础设施中成为核心任务。我们报告了一项正在进行的Lean形式化工作，针对的是《测度论概率论：应用于统计学、金融学与工程学》这本包含14章的高等本科生教材，内容涵盖从黎曼-斯蒂尔杰斯积分到鞅和极限定理的主题。该项目生成了这本教材的机器可验证配套资料，并为未来涉及概率论的形式化工作贡献了可复用的基础设施。Lean形式化提供了计算机验证的陈述和证明，明确了假设，并允许读者查阅教材结果的精确逻辑内容。一个核心挑战是弥合教材表述与Mathlib更通用的测度论接口之间的差距。我们尽可能复用Mathlib的结果，当教材表述与库抽象存在差异时，引入可审核的接口引理。该项目表明，形式化教材可支持教学、澄清数学假设，并助力构建可靠的AI辅助数学所需的形式化基础。
英文摘要
As large language models become increasingly capable of generating mathematical arguments, mathematics is likely to face not a scarcity of proofs but an abundance of plausible ones. In such an environment, verification, exposition, and incorporation into reusable mathematical infrastructure become central tasks. We report on an ongoing Lean formalization of "Measure-Theoretic Probability: With Applications to Statistics, Finance, and Engineering", a fourteen-chapter upper-level undergraduate textbook covering topics from Riemann--Stieltjes integration to martingales and limit theorems. The project produces a machine-checked companion to the textbook and contributes reusable infrastructure for future formalizations involving probability theory. A Lean formalization provides computer-checked statements and proofs, makes hypotheses explicit, and allows readers to inspect the precise logical content of textbook results. A central challenge is to bridge textbook-facing statements with Mathlib's more general measure-theoretic interfaces. We reuse Mathlib results when possible and introduce reviewable interface lemmas when the textbook formulation and library abstraction differ. The project illustrates how formalized textbooks can support teaching, clarify mathematical assumptions, and help build the formal foundations needed for reliable AI-assisted mathematics.
