Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Khovanskii's Theorem

view this post on Zulip Email Gateway (Sep 07 2022 at 13:39):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m glad to announce that there is another new AFP entry today.

Best,
René

Khovanskii's Theorem
by Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Abstract:
We formalise the proof of an important theorem in additive combinatorics due to
Khovanskii, attesting that the cardinality of the set of all sums of n many
elements of A, where A is a finite subset of an abelian group, is a polynomial
in n for all sufficiently large n. We follow a proof due to Nathanson and Ruzsa
as presented in the notes "Introduction to Additive Combinatorics" by Timothy
Gowers for the University of Cambridge.

https://www.isa-afp.org/entries/Khovanskii_Theorem.html

Last updated: Jan 04 2025 at 20:18 UTC