### Abstract

In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of 픽^{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 cap set problem. Ellenberg and Gijswijt’s proof was published in the 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 픽^{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.

Original language | English |
---|---|

Title of host publication | 10th International Conference on Interactive Theorem Proving (ITP 2019) |

Editors | John Harrison, John O'Leary, Andrew Tolmach |

Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |

Pages | 1-19 |

Number of pages | 19 |

ISBN (Print) | 9783959771221 |

DOIs | |

Publication status | Published - 2019 |

Event | 10th International Conference on Interactive Theorem Proving, ITP 2019 - Portland, United States Duration: 9 Sep 2019 → 12 Sep 2019 |

### Publication series

Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|

Volume | 141 |

ISSN (Print) | 1868-8969 |

### Conference

Conference | 10th International Conference on Interactive Theorem Proving, ITP 2019 |
---|---|

Country | United States |

City | Portland |

Period | 9/09/19 → 12/09/19 |

### Fingerprint

### Keywords

- Cap set problem
- Combinatorics
- Formal proof
- Lean

### Cite this

*10th International Conference on Interactive Theorem Proving (ITP 2019)*(pp. 1-19). [15] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 141). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ITP.2019.15