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
by Sander R. Dahmen,
Johannes Hölzl, and
Robert Y. Lewis.
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
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
It compiles with Lean version 3.4.2 and mathlib commit
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.
- Install Lean using its version manager elan, following directions
- 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