AI 中文总结
本文在 Lean 证明助手中形式化 $q$-级数理论，通过构造 $q$-Pochhammer 符号等基本构件，验证了 Jacobi 三重积公式和 Rogers-Ramanujan 恒等式，为模形式等领域的未来形式化奠定基础。
AI 中文摘要
$q$-级数和基本超几何级数理论在组合学、数论和表示论的交汇处起着关键作用。从 Euler 和 Jacobi 的经典分拆恒等式到类域论、顶点算子代数和 Monster 月光猜想等现代发展，$q$-级数为广泛深刻的应用提供了分析框架。本文讨论了在 Lean 证明助手中形式化该理论的过程，这需要精心设计可扩展且通用的结构，以调和形式代数恒等式与分析收敛性质。我们通过聚焦于 $q$-Pochhammer 符号、$q$-二项式系数、Bailey 引理及类似原语的构造来应对这些基础性挑战。为展示该工作的实用性，我们提供了 Jacobi 三重积公式和著名的 Rogers-Ramanujan 恒等式的完全验证证明，这些恒等式是该领域的历史和技术基准。本工作为未来形式化 mock theta 函数、模形式以及支撑其在数学和物理中应用的多样化代数结构建立了严格的计算基础。
英文摘要
The theory of $q$-series and basic hypergeometric series plays a crucial role at the intersection of combinatorics, number theory, and representation theory. From the classical partition identities of Euler and Jacobi to modern developments in class field theory, vertex operator algebras, and the Monstrous Moonshine conjecture, $q$-series provide the analytic framework for a wide range of profound applications. In this paper, we discuss the formalization of this theory in the Lean proof assistant, a process that requires careful design of scalable and versatile structures to reconcile formal algebraic identities with analytic convergence properties. We address these foundational challenges by focusing on the construction of $q$-Pochhammer symbols, $q$-binomial coefficients, Bailey's Lemma and similar primitives. To demonstrate the utility of this work, we provide fully verified proofs of the Jacobi Triple Product formula and the celebrated Rogers-Ramanujan identities, which serve as both historical and technical benchmarks for the field. This work establishes a rigorous computational foundation for the future formalization of mock theta functions, modular forms, and the diverse algebraic structures that underpin their applications across mathematics and physics. AxiomProver was used to produce the formalizations in this paper.
Comments38 pages
