PKU BICMR AI for Math

Appearance

On this page

AI4Math 练习项目说明 ​

2023 年 7 月

项目要求 ​

  • 我们将按照基础数学方向和应用数学方向将全体同学分成项目小组，3-4 位同一方向的同学构成一组。

  • 根据小组成员的方向，请参考「选题样例」一节确定小组选题。你可以选择样例中的题目，也可以自选与之难度类似的其他题目。请使用 Lean4 完成所选择的定理叙述的形式化，并完成其证明。

  • 确认选题后，请每组派一位同学与助教沟通确认所选的题目，确认选题难度是否适中，并协调不同组之间的选题尽量互不重复。基础数学选题的小组请与姜杰东联系，应用数学选题的小组请与李晨毅或王子彧联系。

  • 项目将于 2023.07.25-2023.07.29 每天下午进行展示。请在展示前，将编译通过的 .lean 文件，提前发给助教。请在文件开头的注释中注明小组成员的构成。

  • 完成本项目时，你可以使用包括搜索引擎在内的任意电子工具。我们也推荐你在 Lean 社群上将你遇到的问题大胆提问，或与其他同学或助教讨论。但我们仍要求小组成员在获得必要的帮助后，独立地写下整个形式化证明。

  • 本项目的目的，在于训练大家查找 Mathlib 的能力，与有条理的形式化数学定理的能力。因此后文中所列出的题目，对于有该领域基础知识的同学相对简单。搜索引擎亦能很好地帮助你得到相关问题的正确数学证明。

  • 在完成项目的过程中，请注意以下诸点：

    1. 请首先查找并阅读 Mathlib 中与选题相关的内容，若小组选题在 Mathlib 上已经有较完善的基础，请尽量避免重复造轮子。

    2. 若小组选题在 Mathlib 上没有完善的基础，你可能需要自行写下相关定义，及前续定理。

    3. 对于需要自选具体形式化定理内容的小组，你所选的定理可以是教科书的课后习题、经典推论、或者其他定理，但请检索该命题是否在 Mathlib 中已经有相似命题，如果确有类似的，请更换命题。（请注意，有些看似简单的定理在 Lean 中的证明是较为困难的，请谨慎选择并与助教交流你想证明的题目）我们希望大家主要展示 Mathlib 定理与 tactics 的使用，不要求大家攻克难题。

  • 在进行项目展示时，请注意以下诸点：

    1. 若小组所研究的题目在 Mathlib 上已经有较完善的基础，请在展示时首先大致讲解课题相关定理在 Lean 中的实现与使用。

    2. 若小组选题在 Mathlib 上没有完善的基础，请在展示时首先讲解相关定义及前续定理在 Lean 中的实现及使用。

    3. 如果你所证明的定理不是大一大二基础课程所含内容，建议大家在展示时先讲解该定理使用自然数学语言的证明。

    4. 欢迎大家分享（吐槽）一部分使用 Lean 的经验，可以是选 Lean 实现过程中与实际的数学工作中不太一致的地方。如果可以的话，可以分享你认为对研究领域的后续知识形式化会遇到哪些难点。

    5. 课堂展示时请展示你的代码，语言为 Lean4，可以使用幻灯片辅助展示但并非必要，展示的主要目的是为其他同学讲清楚 Lean 在数学研究的不同分支上如何使用。

选题样例 ​

基础数学相关 ​

  • 以下列出数十个问题，它们被分为几个板块: 线性代数、抽象代数、 交换代数、数论、基础分析、点集拓扑、泛函. 每个板块大致有几个小题。你可以从中选择你喜欢的板块和问题或是选择其他难度相似的问题。带 ⋆\star 标记的问题相较于其他问题可能更具形式化方面的难度。

  • 你也可以选择其他数学分支的定理进行形式化，例如：组合恒等式。

  • 如果你认为完成一道题目过于简单，可以选择多道题目完成。

  • 如果你觉得某问题的叙述有误， 则你可以解释错误并按照你的想法更正，并形式化更正后的定理。

线性代数 ​

习题 1. 给定特征 00 的域上有限维线性空间 VV. 设 A,B:V→VA,B:V\to V 线性自同态, 证明

AB−BA≠idVAB-BA\ne\mathrm{id}_V

习题 2. 线性空间 VV 的线性自同态 p:V→Vp:V\to V 满足 p2=pp^2=p, 证明 V=Ker⁡p⊕Im⁡pV=\operatorname{Ker}p\oplus\operatorname{Im}p

习题 3. 给定有限维线性空间 VV 的线性自同构 f:V→Vf:V\to V, 若 VV 的子空间 WW 是 ff-不变的子空间, 则它也是 f−1f^{-1}-不变的子空间.

习题 4 (⋆\star). 基域 R\mathbb R 上的 n×nn\times n 任意矩阵 AA, 证明

Rank⁡A=Rank⁡ATA\operatorname{Rank}A=\operatorname{Rank}A^\text TA

习题 5 (⋆\star). 线性映射 f:Mn(k)→kf:M_n(k)\to k 满足 f(AB)=f(BA)f(AB)=f(BA), 证明 f=cTr⁡f=c\operatorname{Tr} 对某 c∈kc\in k

抽象代数 ​

习题 6. 对群 GG 的两个子群 H1,H2H_1,H_2 使 H1∪H2H_1\cup H_2 是子群, 证明 H1,H2H_1,H_2 具有互相包含关系

习题 7. 证明有限群到 C×\mathbb C^\times 的同态穿过 S1S^1

习题 8. 证明 pqpq 阶群不是单群, 其中 p,qp,q 是不相同的素数

习题 9. 证明 44 元群总是 Abel 群

习题 10. 证明二次扩张都是 Galois 扩张

习题 11 (⋆\star). 请写出 Abel 群映射正合的定义, 并从你写出的定义出发, 证明 Abel 群的四引理：设 Abel 群 A,B,C,D,A′,B′,C′,D′A,B,C,D,A',B',C',D' 有如下图表

A→B→C→D↓α↓β↓γ↓δA′→B′→C′→D′\begin{CD} A @>>> B @>>> C @>>> D \\ @VV\alpha V @VV\beta V @VV\gamma V @VV\delta V \\ A' @>>> B' @>>> C' @>>> D' \end{CD}

若 α\alpha 是满射且 β,δ\beta, \delta 是单射, 则 γ\gamma 是单射； 若 δ\delta 是单射且 α,γ\alpha,\gamma 是满射, 则 β\beta 是满射

交换代数 ​

习题 12 (⋆\star). 证明 Krull 交定理: Noether 环 RR 上理想 II 和有限生成模 MM, 存在 r∈Ir\in I 使

(1−r)⋂k≥0IkM=0(1-r)\bigcap_{k\ge 0}I^kM=0

习题 13 (⋆\star). 环 RR 和 RR -模正合列 0→M→N→P→00\to M\to N\to P\to 0, 证明结合素理想的包含关系：

Ass⁡R(M)⊂Ass⁡R(N)⊂Ass⁡R(M)∪Ass⁡R(P)\operatorname{Ass}_R(M)\subset\operatorname{Ass}_R(N)\subset\operatorname{Ass}_R(M)\cup\operatorname{Ass}_R(P)

习题 14 (⋆\star). 给定环 RR 和有限生成 RR-模 MM, RR-模满自同态 f:M→Mf:M\to M, 证明 ff 是同构

习题 15. 证明 素理想回避定理：设环 RR 中有素理想 p1,⋯ ,pn\mathfrak p_1,\cdots,\mathfrak p_n 是和一般的理想 II, 如果 I⊄piI\not\subset\mathfrak p_i 对所有 ii 成立, 则存在 x∈Ix\in I 使 x∉pix\not\in\mathfrak p_i 对所有 ii 成立

数论基础 ​

习题 16. 对正整数 a,s,ta,s,t, 证明 agcd⁡(s,t)−1=gcd⁡(as−1,at−1)a^{\operatorname{gcd}(s,t)}-1=\operatorname{gcd}(a^s-1,a^t-1)（作为bonus, 可以证明对任意正整数 nn, n∤2n−1n\nmid 2^n-1）

习题 17 (⋆\star). 对 K=Q[−3]K=\mathbb Q[\sqrt{-3}], 证明它的整数环 OK=Z[ω]\mathcal O_K=\mathbb Z[\omega] 其中 ω=12(1+−3)\omega=\frac12(1+\sqrt{-3}), 并且证明 OK\mathcal O_K 是主理想整环

习题 18 (⋆\star). 证明域的有限乘法群是循环群

习题 19. 设 pp 是奇素数, 证明 x2+y2=1x^2+y^2=1 在 Fp\mathbb F_p 中的解数为 p−(−1)(p−1)/2p-(-1)^{(p-1)/2}

基础分析 ​

习题 20. 求极限

lim⁡x→+∞(1+1x)x2e−x=1e\lim_{x\to+\infty}\left(1+\frac1x\right)^{x^2}e^{-x}=\frac1{\sqrt e}

习题 21 (⋆\star). 奇数次实系数多项式必有实根

习题 22 (⋆\star). 周期三蕴含混沌的 Li-Yorke 定理：若 f:[0,1]→[0,1]f:[0,1]\to[0,1] 是连续映射, 且 ff 存在 33-周期点, 则对任意正整数 nn, ff 存在 nn-周期点

点集拓扑 ​

习题 23. 证明紧空间到 T2T_2（Hausdorff）空间的连续双射是同胚

习题 24 (⋆\star). 定义 R\mathbb R 上的 Sorgenfrey 拓扑, 证明它 C1C_1 但不 C2C_2

泛函分析 ​

习题 25 (⋆\star). 可分 Hilbert 空间上的紧算子是有限秩算子的极限

习题 26. 给定 X,YX,Y 是 Banach 空间和连续线性算子 f:X→Yf:X\to Y. 证明 f(X)f(X) 要么是 YY, 要么是第一纲的

计算数学相关 ​

下面列了 8 个相关选题，每个选题提到了相关方向的一些定理，给了一些参考文献的部分内容，里面可能涉及到了很多定理与例子。实际形式化的时候，可以从易到难，从例子到定理。

  1. 凸集：可以将 1.3.1 节 [1] 中的一些例子的证明形式化，也可以尝试证明 1.3.3 节中的凸集分离定理不同形式（这可能在 Mathlib 库中的 Hahn-Banach 定理中提到过）。

  2. 凸函数：可以在 1.3.2 节 [1] 中形式化凸函数的一些性质与判定（如梯度单调、海瑟矩阵半正定等）。也可以形式化有关强凸函数的性质。 如果高维函数难以操作，也可以先尝试在一维函数的背景下形式化。

  3. 向量范数和矩阵范数：可以探索 Mathlib 中关于范数已经有的结论，探索部分还没有形式化的内容，可以参考 [1] 1.2.1 相关内容。

  4. 高维微积分：可以尝试使用 fderiv 和 deriv 的定义来形式化一些高维微积分或 计算矩阵函数的导数。如果定理形式化较为困难，也可以从例子入手。

  5. 多项式插值、样条：可以考虑拉格朗日插值的存在性以及误差估计，样条函数的存在性等等内容，也可以从最佳逼近角度证明一些基本定理，参考 [2] 第二章的部分内容。

  6. 矩阵迹和行列式： 可以将矩阵计算的一些特性形式化，如分块矩阵、Schur 补、SMW 公式。注意其中部分内容在 Mathlib 中已经形式化。可以参考 [1] 中 1.2.4 节相关内容。

  7. 数值微分、数值积分：可以给出微分和积分格式的误差估计，灵活应用导数、积分和中值定理。参考文献为 [2] 第三章部分。

  8. 矩阵的特征值和特征向量相关性质：例如实对称矩阵一定有实特征值等等，可以参考 [1] 1.2.2 节相关内容。

[1]

BibTeX
@book{sun2006optimization,
  title={Optimization theory and methods: nonlinear programming},
  author={Sun, Wenyu and Yuan, Ya-Xiang},
  volume={1},
  year={2006},
  publisher={Springer Science \& Business Media}
}

[2]

BibTeX
@book{张平文2007数值分析,
  title={数值分析},
  author={张平文，李铁军},
  year={2007},
  publisher={北京大学出版社}
}