Formalizing the Solution to the Cap Set Problem

This web page collects the auxiliary materials for the paper Formalizing the Solution to the Cap Set Problem by Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis.

Informal writeup

As the first step in our efforts, Sander Dahmen produced a detailed paper proof of the theorem, which we followed during the formalization process. We make this blueprint available here as a reference.

Current Lean code

The most up-to-date version of our formalization can be found here. It compiles with Lean version 3.4.2.

Lean code at submission

We keep a branch of our formalization frozen in the state it was on March 31, 2019, the date of submission of our paper to ITP. This can be found here. It compiles with Lean version 3.4.2 and mathlib commit 2e7f0099d2e97b370de475f8e7854f5557c265b7.

Code organization

All theorem numbers correspond to our detailed paper proof.

• The files library.lean and has_deriv.lean contain background definitions and theorems that will be moved to mathlib.
• The file section_9.lean contains the proof of Lemma 9.2, used in section 12.
• The file section_10_11_12.lean corresponds to Section 4 of our paper. It contains the construction of the cap set bound.
• The file section_13a.lean contains developments needed for our original proof of the asymptotics, corresponding to the appendix of our paper. It is not used in the final result.
• The file section_13b.lean corresponds to Section 5 of our paper. It verifies the asymptotic behavior of the bound in section 12.

Compilation directions

• Install Lean using its version manager elan, following directions here.
• Clone the desired GitHub repository, e.g. add link.
• In the root of this directory, run leanpkg configure and leanpkg build. (Note: if you do not download precompiled mathlib binaries, this may take some time.)
• To inspect the files in VSCode, use File->Open Folder... to open the root of this directory.