Freiman's 3k - 4 Theorem

Arthur Freitas Ramos 📧, David Barros Hulak 📧 and Ruy Jose Guerra Barretto de Queiroz 📧

June 2, 2026

Abstract

This entry formalizes Freiman's \(3k - 4\) theorem for finite sets of integers: small doubling, in the range \(|A + A| \leq 3|A| - 4\), forces containment in a short arithmetic progression. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.

License

BSD License

Note

Codex with gpt 5.5 on extra high was used to help with proof engineering

Topics

Session Freiman_3k_4

Depends on

Cite

× 
@article{Freiman_3k_4-AFP,
  author  = {Arthur Freitas Ramos and David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz},
  title   = {Freiman's 3k - 4 Theorem},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Freiman_3k_4.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download