帽集问题的形式化求解
Formalizing the Solution to the Cap Set Problem
摘要：
在2016年，Ellenberg和Gijswijt建立了一个新的关于没有三项算术级数的$\mathbb{F}^n_q$子集大小的上限。这个问题已经得到了很多数学上的关注，特别是在$q = 3$的情况下，它通常被称为\emph{cap set problem}。Ellenberg和Gijswijt的证明发表在《\emph{Annals of Mathematics}》上，值得注意的是它巧妙地使用了初等方法。本文描述了一个形式化的证明在精益证明助手，包括一般结果在$\mathbb{F}^n_q$和具体值的情况下$q = 3$。我们忠实地遵循笔和纸的论点来构建界限。我们的工作表明，（某些）现代数学是在证明助手的范围之内。
英文摘要：
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $\mathbb{F}^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the \emph{cap set problem}. Ellenberg and Gijswijt's proof was published in the \emph{Annals of Mathematics} and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in $\mathbb{F}^n_q$ and concrete values for the case $q = 3$. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
