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.

The paper is still a draft and this page is under construction.

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.

Compilation directions