Skip to content

Latest commit

 

History

History
242 lines (167 loc) · 10.3 KB

team-exercises.md

File metadata and controls

242 lines (167 loc) · 10.3 KB
title
AI4Math 练习项目说明

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. 给定特征 $0$ 的域上有限维线性空间 $V$. 设 $A,B:V\to V$ 线性自同态, 证明 $$ AB-BA\ne\mathrm{id}_V $$

习题 2. 线性空间 $V$ 的线性自同态 $p:V\to V$ 满足 $p^2=p$, 证明 $V=\operatorname{Ker}p\oplus\operatorname{Im}p$

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

习题 4 ($\star$). 基域 $\mathbb R$ 上的 $n\times n$ 任意矩阵 $A$, 证明 $$ \operatorname{Rank}A=\operatorname{Rank}A^\text TA $$

习题 5 ($\star$). 线性映射 $f:M_n(k)\to k$ 满足 $f(AB)=f(BA)$, 证明 $f=c\operatorname{Tr}$ 对某 $c\in k$

抽象代数

习题 6. 对群 $G$ 的两个子群 $H_1,H_2$ 使 $H_1\cup H_2$ 是子群, 证明 $H_1,H_2$ 具有互相包含关系

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

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

习题 9. 证明 $4$ 元群总是 Abel 群

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

习题 11 ($\star$). 请写出 Abel 群映射正合的定义, 并从你写出的定义出发, 证明 Abel 群的四引理：设 Abel 群 $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 环 $R$ 上理想 $I$ 和有限生成模 $M$, 存在 $r\in I$ 使 $$ (1-r)\bigcap_{k\ge 0}I^kM=0 $$

习题 13 ($\star$). 环 $R$ 和 $R$ -模正合列 $0\to M\to N\to P\to 0$, 证明结合素理想的包含关系： $$ \operatorname{Ass}_R(M)\subset\operatorname{Ass}_R(N)\subset\operatorname{Ass}_R(M)\cup\operatorname{Ass}_R(P) $$

习题 14 ($\star$). 给定环 $R$ 和有限生成 $R$-模 $M$, $R$-模满自同态 $f:M\to M$, 证明 $f$ 是同构

习题 15. 证明 素理想回避定理：设环 $R$ 中有素理想 $\mathfrak p_1,\cdots,\mathfrak p_n$ 是和一般的理想 $I$, 如果 $I\not\subset\mathfrak p_i$ 对所有 $i$ 成立, 则存在 $x\in I$ 使 $x\not\in\mathfrak p_i$ 对所有 $i$ 成立

数论基础

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

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

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

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

基础分析

习题 20. 求极限 $$ \lim_{x\to+\infty}\left(1+\frac1x\right)^{x^2}e^{-x}=\frac1{\sqrt e} $$

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

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

点集拓扑

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

习题 24 ($\star$). 定义 $\mathbb R$ 上的 Sorgenfrey 拓扑, 证明它 $C_1$ 但不 $C_2$

泛函分析

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

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

计算数学相关

下面列了 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]

@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]

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