# 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.