Email Gateway (May 29 2026 at 16:02): Email Gateway (May 29 2026 at 16:02):From: Lawrence Paulson <lp15@cam.ac.uk>
We have yet another contribution from Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Abstract
We formalize the Erdős–Ginzburg–Ziv theorem for integer multisets: every multiset of at least 2n−1 integers contains a submultiset of cardinality n whose sum is divisible by n. The proof is split into a prime-modulus argument over residue multisets and a strong-induction argument for the general case, following the classical theorem of Erdős, Ginzburg, and Ziv [1]. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.
https://isa-afp.org/entries/Erdos_Ginzburg_Ziv.html
Last updated: Jun 12 2026 at 04:13 UTC