Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Freiman’s 3k−4 Theorem

view this post on Zulip Email Gateway (Jul 07 2026 at 07:03):

From: Tobias Nipkow <nipkow@in.tum.de>

Freiman's 3k - 4 Theorem
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz

This entry formalizes Freiman's theorem for finite sets of integers: small
doubling, in the range , forces containment in a short arithmetic progression.
AI assistance was used for proof engineering. The final definitions, statements,
and proofs are checked by Isabelle.

https://isa-afp.org/entries/Freiman_3k_4.html

Enjoy!

PS The authors clearly reference the sources they used, an important practice:

"The formalization follows the standard presentation of Freiman’s theorem in
additive-combinatorics texts, especially Nathanson [1] and Tao and Vu [2]."

smime.p7s

Last updated: Jul 22 2026 at 14:00 UTC